-- 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) := by
Goals accomplished! 🐙
  rintro 
⟨a, ha⟩: ∃ a, p a
⟨
a: ℕ
a
⟨a, ha⟩: ∃ a, p a
, 
ha: p a
ha
⟨a, ha⟩: ∃ a, p a
⟩ 
⟨: ∃ b, p b
⟨
p: ℕ → Prop
(∃ b, p b) → (∃ b, p b) → ∃ c, p c
b: ℕ
b
Warning: unused variable `b`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p: ℕ → Prop
(∃ b, p b) → (∃ b, p b) → ∃ c, p c
, : ∃ b, p b
,
p: ℕ → Prop
(∃ b, p b) → (∃ b, p b) → ∃ c, p c
, : ∃ b, p b
 
hb: p b
hb
Warning: unused variable `hb`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p: ℕ → Prop
(∃ b, p b) → (∃ b, p b) → ∃ c, p c
⟩: ∃ b, p b
⟩
p: ℕ → Prop
a: ℕ
ha: p a
b: ℕ
hb: p b
intro.intro
∃ c, p c
  use 
a: ℕ
a
Goals accomplished! 🐙

-- break `rintro` into `intro`s and `obtain`s
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := by
Goals accomplished! 🐙
  intro 
h1: ∃ a, p a
h1
p: ℕ → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro 
h2: ∃ b, p b
h2
p: ℕ → 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
h1
p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro
∃ c, p c
  obtain 
⟨: ∃ b, p b
⟨
p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro
∃ c, p c
b: ℕ
b
Warning: unused variable `b`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro
∃ c, p c
, : ∃ b, p b
,
p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro
∃ c, p c
, : ∃ b, p b
 
hb: p b
hb
Warning: unused variable `hb`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p: ℕ → Prop
h2: ∃ b, p b
a: ℕ
ha: p a
intro
∃ c, p c
⟩: ∃ b, p b
⟩ := 
h2: ∃ b, p b
h2
p: ℕ → Prop
a: ℕ
ha: p a
b: ℕ
hb: p b
intro.intro
∃ c, p c
  use 
a: ℕ
a
Goals accomplished! 🐙

-- rewrite `obtain` to `cases'`
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := by
Goals accomplished! 🐙
  intro 
h1: ∃ a, p a
h1
p: ℕ → Prop
h1: ∃ a, p a
(∃ b, p b) → ∃ c, p c
  intro 
h2: ∃ b, p b
h2
p: ℕ → Prop
h1, h2: ∃ b, p b
∃ c, p c
  cases' 
h1: ∃ a, p a
h1 with 
a: ℕ
a 
ha: p a
ha
p: ℕ → 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
ha
p: ℕ → Prop
a✝: ℕ
ha✝: p a✝
a: ℕ
ha: p a
intro.intro
∃ c, p c
  use 
a: ℕ
a
Goals accomplished! 🐙

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

-- using `rintro`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
Goals 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: ℕ
a
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h
∃ d, p a d
  use 
b: ℕ
b
Goals accomplished! 🐙

-- break `rintro` into `intro`s and `cases'`s
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
Goals accomplished! 🐙
  intro 
h: ∃ a b, p a b
h
p: ℕ → ℕ → 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
ha
p: ℕ → ℕ → 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
hb
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro
∃ c d, p c d
  use 
a: ℕ
a
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h
∃ d, p a d
  use 
b: ℕ
b
Goals accomplished! 🐙

-- collapse `cases'`s into a single `rcases`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
Goals accomplished! 🐙
  intro 
h: ∃ a b, p a b
h
p: ℕ → ℕ → 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: ℕ
a
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h
∃ d, p a d
  use 
b: ℕ
b
Goals 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)) := by
Goals accomplished! 🐙
  intro 
h: ∃ a b, p a b
h
p: ℕ → ℕ → 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
h
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
intro.intro
∃ c d, p c d
  use 
a: ℕ
a
p: ℕ → ℕ → Prop
a, b: ℕ
hb: p a b
h
∃ d, p a d
  use 
b: ℕ
b
Goals accomplished! 🐙

namespace Foo

#check
eq_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 := by
Goals accomplished! 🐙
  obtain 
(hp | hq): p ∨ q
(
hp: p
hp
hp | hq: p ∨ q
 | 
hq: q
hq
(hp | hq): p ∨ q
) := 
h: p ∨ q
h
p, q, r: Prop
hp: p
inl
q ∨ p
p, q, r: Prop
hq: q
inr
q ∨ p
  .
p, q, r: Prop
hp: p
inl
q ∨ p exact 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr 
hp: p
hp
Goals accomplished! 🐙
  .
p, q, r: Prop
hq: q
inr
q ∨ p exact 
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 := by
Goals accomplished! 🐙
  obtain 
⟨hp, hq⟩: p ∧ q
⟨
hp: p
hp
⟨hp, hq⟩: p ∧ q
, 
hq: q
hq
⟨hp, hq⟩: p ∧ q
⟩ := 
h: p ∧ q
h
p, q, r: Prop
hp: p
hq: q
intro
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) := by
Goals accomplished! 🐙
  obtain 
⟨hp | hq, hr⟩: (p ∨ q) ∧ r
⟨
hp: p
hp
hp | 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
h
p, q, r: Prop
hr: r
hp: p
intro.inl
r ∧ (q ∨ p)
p, q, r: Prop
hr: r
hq: q
intro.inr
r ∧ (q ∨ p)
  .
p, q, r: Prop
hr: r
hp: p
intro.inl
r ∧ (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.inr
r ∧ (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 := by
Goals accomplished! 🐙
  cases 
h: p ∨ q
h with
p, q, r: Prop
h: p ∨ q
q ∨ p
  | 
inl: ∀ {a b : Prop}, a → a ∨ b
inl 
h: p
h =>
p, q, r: Prop
h: p
inl
q ∨ p exact 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr 
h: p
h
Goals accomplished! 🐙
  | 
inr: ∀ {a b : Prop}, b → a ∨ b
inr 
h: q
h =>
p, q, r: Prop
h: q
inr
q ∨ p exact 
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl 
h: q
h
Goals accomplished! 🐙