-- 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: Nat
a⟨a, ha⟩: ∃ a, p a
, ha: p a
ha⟨a, ha⟩: ∃ a, p a
⟩ ⟨b, hb⟩: ∃ b, p b
⟨b: Nat
b⟨b, hb⟩: ∃ b, p b
, hb: p b
hb⟨b, hb⟩: ∃ b, p b
⟩p: Nat → Prop
a: Nat
ha: p a
b: Nat
hb: p b
∃ c, p c
  use a: Nat
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
h1Warning: Try this: intro h1 h2
p: Nat → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro h2: ∃ b, p b
h2Warning: Try this: intro h1 h2
p: Nat → Prop
h1, h2: ∃ b, p b
∃ c, p c
  obtain ⟨a, ha⟩: ∃ a, p a
⟨a: Nat
a⟨a, ha⟩: ∃ a, p a
, ha: p a
ha⟨a, ha⟩: ∃ a, p a
⟩ := h1: ∃ a, p a
h1Warning: Try this: intro h1 h2
p: Nat → Prop
h2: ∃ b, p b
a: Nat
ha: p a
∃ c, p c
  obtain ⟨b, hb⟩: ∃ b, p b
⟨b: Nat
b⟨b, hb⟩: ∃ b, p b
, hb: p b
hb⟨b, hb⟩: ∃ b, p b
⟩ := h2: ∃ b, p b
h2p: Nat → Prop
a: Nat
ha: p a
b: Nat
hb: p b
∃ c, p c
  use a: Nat
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
h1Warning: Try this: intro h1 h2
p: Nat → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro h2: ∃ b, p b
h2Warning: Try this: intro h1 h2
p: Nat → Prop
h1, h2: ∃ b, p b
∃ c, p c
  cases' h1: ∃ a, p a
h1 with a: Nat
a ha: p a
haWarning: Try this: intro h1 h2
p: Nat → Prop
h2: ∃ b, p b
a: Nat
ha: p a
intro∃ c, p c
  cases' h2: ∃ b, p b
h2 with a: Nat
a ha: p a
hap: Nat → Prop
a✝: Nat
ha✝: p a✝
a: Nat
ha: p a
intro.intro∃ c, p c
  use a: Nat
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: Nat
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: Nat
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: Nat → Nat → Prop
a, b: Nat
hb: p a b
∃ c d, p c d
  use a: Nat
ap: Nat → Nat → Prop
a, b: Nat
hb: p a b
h∃ d, p a d
  use b: Nat
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: Nat → Nat → Prop
h: ∃ a b, p a b
∃ c d, p c d
  cases' h: ∃ a b, p a b
h with a: Nat
a ha: ∃ b, p a b
hap: Nat → Nat → Prop
a: Nat
ha: ∃ b, p a b
intro∃ c d, p c d
  cases' ha: ∃ b, p a b
ha with b: Nat
b hb: p a b
hbp: Nat → Nat → Prop
a, b: Nat
hb: p a b
intro.intro∃ c d, p c d
  use a: Nat
ap: Nat → Nat → Prop
a, b: Nat
hb: p a b
h∃ d, p a d
  use b: Nat
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: Nat → Nat → 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: Nat
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: Nat
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: Nat → Nat → Prop
a, b: Nat
hb: p a b
∃ c d, p c d
  use a: Nat
ap: Nat → Nat → Prop
a, b: Nat
hb: p a b
h∃ d, p a d
  use b: Nat
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: Nat → Nat → Prop
h: ∃ a b, p a b
∃ c d, p c d
  obtain ⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
⟨a: Nat
a⟨a, ⟨b, hb⟩⟩: ∃ a b, p a b
, ⟨b, hb⟩: ∃ b, p a b
⟨b: Nat
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: Nat → Nat → Prop
a, b: Nat
hb: p a b
∃ c d, p c d
  use a: Nat
ap: Nat → Nat → Prop
a, b: Nat
hb: p a b
h∃ d, p a d
  use b: Nat
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
q ∧ 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
inlr ∧ (q ∨ p)
p, q, r: Prop
hr: r
hq: q
inrr ∧ (q ∨ p)
  .p, q, r: Prop
hr: r
hp: p
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
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 withGoals accomplished! 🐙
  | 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! 🐙