-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem mem_generateSetAlgebra_elim (s_mem : s ∈ generateSetAlgebra 𝒜) :
    ∃ A : Set (Set (Set α)), A.Finite ∧ (∀ a ∈ A, a.Finite) ∧
    (∀ᵉ (a ∈ A) (t ∈ a), t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ s = ⋃ a ∈ A, ⋂ t ∈ a, t

Proof state:
case compl.intro.intro.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
have := finite_coe_iff.2 A_fin

Result:
case compl.intro.intro.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this : Finite ↑A
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t

Proof state:
case compl.intro.intro.intro.intro.refine_2.h.mp
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
hx : ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2
⊢ ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1

Tactic:
choose f hf using hx

Result:
case compl.intro.intro.intro.intro.refine_2.h.mp
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
f : (i : Set (Set α)) → i ∈ A → Set α
hf : ∀ (i : Set (Set α)) (i_1 : i ∈ A), f i i_1 ∈ i ∧ x ∉ f i i_1
⊢ ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1

Proof state:
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ ∅ = ⋃ a ∈ ∅, ⋂ t ∈ a, t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ u ∪ v = ⋃ a ∈ Au ∪ Av, ⋂ t ∈ a, t

Tactic:
rw [u_eq, v_eq, ← biUnion_union]

Result:
no goals

Proof state:
case compl.intro.intro.intro.intro.refine_1.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ ↑(f a) ∈ 𝒜 ∨ (↑(f a))ᶜ ∈ 𝒜

Tactic:
exact hA a.1 a.2 (f a).1 (f a).2

Result:
no goals

Proof state:
case empty
α : Type u_1
𝒜 : Set (Set α)
s : Set α
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ ∅ = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
exact ⟨∅, finite_empty, fun _ h ↦ (not_mem_empty _ h).elim,
fun _ ha _ _ ↦ (not_mem_empty _ ha).elim, by simp⟩

Result:
no goals

Proof state:
case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
exact hAv a ha t ht

Result:
no goals

Proof state:
case base
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
a : Set (Set α)
ha : a ∈ {{u}}
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *

Result:
case base
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
u_mem : u ∈ 𝒜
a : Set (Set α)
ha : {u} ∈ {{u}}
t : Set α
ht : u ∈ {u}
⊢ u ∈ 𝒜 ∨ uᶜ ∈ 𝒜

Proof state:
case compl.intro.intro.intro.intro.refine_1.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ (↑(f a))ᶜ ∈ 𝒜 ∨ (↑(f a))ᶜᶜ ∈ 𝒜

Tactic:
rw [compl_compl, or_comm]

Result:
case compl.intro.intro.intro.intro.refine_1.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ ↑(f a) ∈ 𝒜 ∨ (↑(f a))ᶜ ∈ 𝒜

Proof state:
case compl.intro.intro.intro.intro.refine_1.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
t : Set α
f : (a : ↑A) → ↑↑a
ht : t ∈ {x | ∃ a, (↑(f a))ᶜ = x}
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
rcases ht with ⟨a, rfl⟩

Result:
case compl.intro.intro.intro.intro.refine_1.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
f : (a : ↑A) → ↑↑a
a : ↑A
⊢ (↑(f a))ᶜ ∈ 𝒜 ∨ (↑(f a))ᶜᶜ ∈ 𝒜

Proof state:
case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
rintro a (ha | ha) t ht

Result:
case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜