-- Mathlib/Data/Set/MemPartition.lean
@[simp]
lemma sUnion_memPartition (f : ℕ → Set α) (n : ℕ) : ⋃₀ memPartition f n = univ

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
⊢ ⋃₀ memPartition f 0 = univ

Tactic:
simp

Result:
no goals

Proof state:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : x ∈ ⋃₀ memPartition f n
⊢ x ∈ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} ↔ x ∈ univ

Tactic:
simp only [mem_sUnion, mem_iUnion, mem_insert_iff, mem_singleton_iff, exists_prop, mem_univ,
  iff_true] at this ⊢

Result:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : ∃ t ∈ memPartition f n, x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Proof state:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ x ∈ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} ↔ x ∈ univ

Tactic:
have : x ∈ ⋃₀ memPartition f n := by simp [ih]

Result:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : x ∈ ⋃₀ memPartition f n
⊢ x ∈ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} ↔ x ∈ univ

Proof state:
case pos
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
exact ⟨t ∩ f n, ⟨t, ht, Or.inl rfl⟩, hxt, hxf⟩

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ memPartition f (n + 1) = univ

Tactic:
rw [memPartition_succ]

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ

Proof state:
case neg
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
exact ⟨t \ f n, ⟨t, ht, Or.inr rfl⟩, hxt, hxf⟩

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ x ∈ ⋃₀ memPartition f n

Tactic:
simp [ih]

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
⊢ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} = univ

Tactic:
ext x

Result:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
⊢ x ∈ ⋃₀ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n} ↔ x ∈ univ

Proof state:
case succ.h.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
by_cases hxf : x ∈ f n

Result:
case pos
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∈ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

case neg
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
hxf : x ∉ f n
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Proof state:
case succ.h
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
this : ∃ t ∈ memPartition f n, x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t

Tactic:
obtain ⟨t, ht, hxt⟩ := this

Result:
case succ.h.intro.intro
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ⋃₀ memPartition f n = univ
x : α
t : Set α
ht : t ∈ memPartition f n
hxt : x ∈ t
⊢ ∃ t ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}, x ∈ t