-- import Batteries.Tactic.Rcases
-- import Mathlib.Tactic.Cases
-- import Mathlib.Tactic.Use
import Mathlib.Logic.Basic
import Mathlib.Tactic.Cases
import Mathlib.Tactic.Use

-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rcases.20vs.20cases

-- ## Understanding `rintro` for 1 pattern

-- using `rintro`
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := byGoals accomplished! 🐙
  rintro ⟨a, ha⟩: ∃ a, p a
⟨a: ℕ
a⟨a, ha⟩: ∃ a, p a
, ha: p a
ha⟨a, ha⟩: ∃ a, p a
⟩ ⟨b, hb⟩: ∃ b, p b
⟨b: ℕ
b⟨b, hb⟩: ∃ b, p b
, hb: p b
hb⟨b, hb⟩: ∃ b, p b
⟩p: ℕ → Prop
a: ℕ
ha: p a
b: ℕ
hb: p b
intro.intro∃ c, p c
  use a: ℕ
aGoals accomplished! 🐙

-- break `rintro` into `intro`s and `obtain`s
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := byGoals accomplished! 🐙
  intro h1: ∃ a, p a
h1p: ℕ → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro h2: ∃ b, p b
h2p: ℕ → Prop
h1, h2: ∃ b, p b
∃ c, p c
  obtain ⟨a, ha⟩: ∃ a, p a
⟨a: ℕ
a⟨a, ha⟩: ∃ a, p a
, ha: p a
ha⟨a, ha⟩: ∃ a, p a
⟩ := h1: ∃ a, p a
h1p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro∃ c, p c
  obtain ⟨b, hb⟩: ∃ b, p b
⟨b: ℕ
b⟨b, hb⟩: ∃ b, p b
, hb: p b
hb⟨b, hb⟩: ∃ b, p b
⟩ := h2: ∃ b, p b
h2p: ℕ → Prop
a: ℕ
ha: p a
b: ℕ
hb: p b
intro.intro∃ c, p c
  use a: ℕ
aGoals accomplished! 🐙

-- rewrite `obtain` to `cases'`
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := byGoals accomplished! 🐙
  intro h1: ∃ a, p a
h1p: ℕ → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro h2: ∃ b, p b
h2p: ℕ → Prop
h1, h2: ∃ b, p b
∃ c, p c
  cases' h1: ∃ a, p a
h1 with a: ℕ
a ha: p a
hap: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro∃ c, p c
  cases' h2: ∃ b, p b
h2 with a: ℕ
a ha: p a
hap: ℕ → Prop
a✝: ℕ
ha✝: p a✝
a: ℕ
ha: p a
intro.intro∃ c, p c
  use a: ℕ
aGoals accomplished! 🐙

-- ## Understanding `rintro` for 1+ patterns

-- using `rintro`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := byGoals accomplished! 🐙
  rintro ⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟨a: ℕ
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: ℕ
b⟨b, hb⟩: ∃ b, p a b
, hb: p a b
hb⟨b, hb⟩: ∃ b, p a b
⟩⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟩p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro∃ c d, p c d
  use a: ℕ
ap: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h∃ d, p a d
  use b: ℕ
bGoals accomplished! 🐙

-- break `rintro` into `intro`s and `cases'`s
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := byGoals accomplished! 🐙
  intro h: ∃ a b, p a b
hp: ℕ → ℕ → Prop
h: ∃ a b, p a b
∃ c d, p c d
  cases' h: ∃ a b, p a b
h with a: ℕ
a ha: ∃ b, p a b
hap: ℕ → ℕ → Prop
a: ℕ
ha: ∃ b, p a b
intro∃ c d, p c d
  cases' ha: ∃ b, p a b
ha with b: ℕ
b hb: p a b
hbp: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro∃ c d, p c d
  use a: ℕ
ap: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h∃ d, p a d
  use b: ℕ
bGoals accomplished! 🐙

-- collapse `cases'`s into a single `rcases`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := byGoals accomplished! 🐙
  intro h: ∃ a b, p a b
hp: ℕ → ℕ → Prop
h: ∃ a b, p a b
∃ c d, p c d
  rcases h: ∃ a b, p a b
h with ⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟨a: ℕ
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: ℕ
b⟨b, hb⟩: ∃ b, p a b
, hb: p a b
hb⟨b, hb⟩: ∃ b, p a b
⟩⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟩p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro∃ c d, p c d
  use a: ℕ
ap: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h∃ d, p a d
  use b: ℕ
bGoals accomplished! 🐙

-- rewrite `rcases` to `obtain` then look at `rintro` above again
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := byGoals accomplished! 🐙
  intro h: ∃ a b, p a b
hp: ℕ → ℕ → Prop
h: ∃ a b, p a b
∃ c d, p c d
  obtain ⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟨a: ℕ
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: ℕ
b⟨b, hb⟩: ∃ b, p a b
, hb: p a b
hb⟨b, hb⟩: ∃ b, p a b
⟩⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟩ := h: ∃ a b, p a b
hp: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro∃ c d, p c d
  use a: ℕ
ap: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h∃ d, p a d
  use b: ℕ
bGoals accomplished! 🐙

namespace Foo

#checkeq_or_ne.{u_1} {α : Sort u_1} (x y : α) : x = y ∨ x ≠ y eq_or_ne: ∀ {α : Sort u_1} (x y : α), x = y ∨ x ≠ y
eq_or_ne

variable (p: Prop
p q: Prop
q r: Prop
r: Prop: Type
Prop)

example: ∀ (p q : Prop), p ∨ q → q ∨ p
example (h: p ∨ q
h: p: Prop
p ∨ q: Prop
q) : q: Prop
q ∨ p: Prop
p := byGoals accomplished! 🐙
  obtain (hp | hq): p ∨ q
(hp: p
hphp | hq: p ∨ q
 | hq: q
hq(hp | hq): p ∨ q
) := h: p ∨ q
hp, q, r: Prop
hp: p
inlq ∨ p
p, q, r: Prop
hq: q
inrq ∨ p
  .p, q, r: Prop
hp: p
inlq ∨ p exact Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr hp: p
hpGoals accomplished! 🐙
  .p, q, r: Prop
hq: q
inrq ∨ p exact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hq: q
hqGoals accomplished! 🐙

example: ∀ (p q : Prop), p ∧ q → q ∧ p
example (h: p ∧ q
h: p: Prop
p ∧ q: Prop
q) : q: Prop
q ∧ p: Prop
p := byGoals accomplished! 🐙
  obtain ⟨hp, hq⟩: p ∧ q
⟨hp: p
hp⟨hp, hq⟩: p ∧ q
, hq: q
hq⟨hp, hq⟩: p ∧ q
⟩ := h: p ∧ q
hp, q, r: Prop
hp: p
hq: q
introq ∧ p
  exact ⟨hq: q
hq, hp: p
hp⟩Goals accomplished! 🐙

example: ∀ (p q r : Prop), (p ∨ q) ∧ r → r ∧ (q ∨ p)
example (h: (p ∨ q) ∧ r
h: (p: Prop
p ∨ q: Prop
q) ∧ r: Prop
r) : r: Prop
r ∧ (q: Prop
q ∨ p: Prop
p) := byGoals accomplished! 🐙
  obtain ⟨hp | hq, hr⟩: (p ∨ q) ∧ r
⟨hp: p
hphp | hq: p ∨ q
 | hq: q
hq⟨hp | hq, hr⟩: (p ∨ q) ∧ r
, hr: r
hr⟨hp | hq, hr⟩: (p ∨ q) ∧ r
⟩ := h: (p ∨ q) ∧ r
hp, q, r: Prop
hr: r
hp: p
intro.inlr ∧ (q ∨ p)
p, q, r: Prop
hr: r
hq: q
intro.inrr ∧ (q ∨ p)
  .p, q, r: Prop
hr: r
hp: p
intro.inlr ∧ (q ∨ p) exact ⟨hr: r
hr, Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr hp: p
hp⟩Goals accomplished! 🐙
  .p, q, r: Prop
hr: r
hq: q
intro.inrr ∧ (q ∨ p) exact ⟨hr: r
hr, Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl hq: q
hq⟩Goals accomplished! 🐙

example: ∀ (p q : Prop), p ∨ q → q ∨ p
example (h: p ∨ q
h: p: Prop
p ∨ q: Prop
q) : q: Prop
q ∨ p: Prop
p := byGoals accomplished! 🐙
  cases h: p ∨ q
h withp, q, r: Prop
h: p ∨ q
q ∨ p
  | inl: ∀ {a b : Prop}, a → a ∨ b
inl h: p
h =>Goals accomplished! 🐙 exact Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr h: p
hGoals accomplished! 🐙
  | inr: ∀ {a b : Prop}, b → a ∨ b
inr h: q
h =>Goals accomplished! 🐙 exact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl h: q
hGoals accomplished! 🐙