-- Mathlib/Data/Set/MemPartition.lean
lemma finite_memPartition (f : ℕ → Set α) (n : ℕ) : Set.Finite (memPartition f n)

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ (memPartition f (n + 1)).Finite

Tactic:
rw [memPartition_succ]

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑{s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Tactic:
simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i ∈ memPartition f n, {a | a = i ∩ f n} ∪ {a | a = i \ f n})

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
⊢ (memPartition f 0).Finite

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑(⋃ i ∈ memPartition f n, {a | a = i ∩ f n} ∪ {a | a = i \ f n})

Tactic:
refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ Finite ↑({a | a = u ∩ f n} ∪ {a | a = u \ f n})

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ Finite ↑({a | a = u ∩ f n} ∪ {a | a = u \ f n})

Tactic:
rw [Set.finite_coe_iff]

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ ({a | a = u ∩ f n} ∪ {a | a = u \ f n}).Finite

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
u : Set α
x✝ : u ∈ memPartition f n
⊢ ({a | a = u ∩ f n} ∪ {a | a = u \ f n}).Finite

Tactic:
simp

Result:
no goals

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

Tactic:
have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}.Finite

Tactic:
rw [← Set.finite_coe_iff]

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : (memPartition f n).Finite
this : Finite ↑(memPartition f n)
⊢ Finite ↑{s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
⊢ (memPartition f n).Finite

Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [memPartition_succ]
  have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
  rw [← Set.finite_coe_iff]
  simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
  refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
  rw [Set.finite_coe_iff]
  simp

Result:
no goals