-- Mathlib/Data/Set/MemPartition.lean
lemma disjoint_memPartition (f : ℕ → Set α) (n : ℕ) {u v : Set α}
    (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v) :
    Disjoint u v

Proof state:
case succ.intro.intro.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
⊢ Disjoint u v

Tactic:
rcases hu'_eq with rfl | rfl <;> rcases hv'_eq with rfl | rfl

Result:
case succ.intro.intro.intro.intro.inl.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)

case succ.intro.intro.intro.intro.inl.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

case succ.intro.intro.intro.intro.inr.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

case succ.intro.intro.intro.intro.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ Disjoint (u' \ f n) (v' \ f n)

Proof state:
case succ.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
⊢ Disjoint u v

Tactic:
obtain ⟨v', hv', hv'_eq⟩ := hv

Result:
case succ.intro.intro.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
v' : Set α
hv' : v' ∈ memPartition f n
hv'_eq : v = v' ∩ f n ∨ v = v' \ f n
⊢ Disjoint u v

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
⊢ ∀ {u v : Set α}, u ∈ memPartition f (n + 1) → v ∈ memPartition f (n + 1) → u ≠ v → Disjoint u v

Tactic:
intro u v hu hv huv

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Disjoint u v

Proof state:
case succ.intro.intro.intro.intro.inl.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' \ f n
⊢ Disjoint (u' ∩ f n) (v' \ f n)

Tactic:
exact Disjoint.mono_left inter_subset_right Set.disjoint_sdiff_right

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ Disjoint (u' \ f n) (v' \ f n)

Tactic:
refine Disjoint.mono diff_subset diff_subset (ih hu' hv' ?_)

Result:
case succ.intro.intro.intro.intro.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ u' ≠ v'

Proof state:
case succ.intro.intro.intro.intro.inl.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ Disjoint (u' ∩ f n) (v' ∩ f n)

Tactic:
refine Disjoint.mono inter_subset_left inter_subset_left (ih hu' hv' ?_)

Result:
case succ.intro.intro.intro.intro.inl.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ u' ≠ v'

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
⊢ Disjoint u v

Tactic:
simp only [memPartition_zero, mem_insert_iff, mem_singleton_iff] at hu hv

Result:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
⊢ Disjoint u v

Tactic:
obtain ⟨u', hu', hu'_eq⟩ := hu

Result:
case succ.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
u' : Set α
hu' : u' ∈ memPartition f n
hu'_eq : u = u' ∩ f n ∨ u = u' \ f n
⊢ Disjoint u v

Proof state:
case succ.intro.intro.intro.intro.inr.inr
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' \ f n
⊢ u' ≠ v'

Tactic:
exact fun huv' ↦ huv (huv' ▸ rfl)

Result:
no goals

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
exact absurd rfl huv

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.inr.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' \ f n ≠ v' ∩ f n
⊢ Disjoint (u' \ f n) (v' ∩ f n)

Tactic:
exact Disjoint.mono_right inter_subset_right Set.disjoint_sdiff_left

Result:
no goals

Proof state:
case succ.intro.intro.intro.intro.inl.inl
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u' : Set α
hu' : u' ∈ memPartition f n
v' : Set α
hv' : v' ∈ memPartition f n
huv : u' ∩ f n ≠ v' ∩ f n
⊢ u' ≠ v'

Tactic:
exact fun huv' ↦ huv (huv' ▸ rfl)

Result:
no goals

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
⊢ ∀ {u v : Set α}, u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
intro u v hu hv huv

Result:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
hv : v ∈ memPartition f 0
huv : u ≠ v
⊢ Disjoint u v

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
u v : Set α
hu : u ∈ memPartition f n
hv : v ∈ memPartition f n
huv : u ≠ v
⊢ Disjoint u v

Tactic:
revert u v

Result:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v