-- 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.refine_2.h
α : 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 : α
⊢ (∀ 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:
constructor <;> intro 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 : α
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

case compl.intro.intro.intro.intro.refine_2.h.mpr
α : 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, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1
⊢ ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2

Proof state:
case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : 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, a.Finite

Tactic:
rintro a (ha | ha)

Result:
case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.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
⊢ a.Finite

case union.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.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
⊢ a.Finite

Proof state:
case compl.intro.intro.intro.intro.refine_2.h.mpr.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
x : α
f : (a : ↑A) → ↑↑a
hf : ∀ (i : Set α) (i_1 : Set (Set α)) (i_2 : i_1 ∈ A), (↑(f ⟨i_1, ⋯⟩))ᶜ = i → x ∈ i
⊢ ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2

Tactic:
exact fun a ha ↦ ⟨f ⟨a, ha⟩, (f ⟨a, ha⟩).2, hf (f ⟨a, ha⟩)ᶜ a ha rfl⟩

Result:
no goals

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
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
refine ⟨{{(f a).1ᶜ | a : A} | f : (Π a : A, ↑a)}, finite_coe_iff.1 inferInstance,
  fun a ⟨f, hf⟩ ↦ hf ▸ finite_coe_iff.1 inferInstance, fun a ha t ht ↦ ?_, ?_⟩

Result:
case compl.intro.intro.intro.intro.refine_1
α : 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
a : Set (Set α)
ha : a ∈ {x | ∃ f, {x | ∃ a, (↑(f a))ᶜ = x} = x}
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

case compl.intro.intro.intro.intro.refine_2
α : 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
⊢ uᶜ = ⋃ a ∈ {x | ∃ f, {x | ∃ a, (↑(f a))ᶜ = x} = x}, ⋂ t ∈ a, t

Proof state:
case compl
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
u_ind : ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ 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:
rcases u_ind with ⟨A, A_fin, mem_A, hA, u_eq⟩

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
⊢ ∃ 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
α : 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
⊢ uᶜ = ⋃ a ∈ {x | ∃ f, {x | ∃ a, (↑(f a))ᶜ = x} = x}, ⋂ t ∈ a, t

Tactic:
ext x

Result:
case compl.intro.intro.intro.intro.refine_2.h
α : 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 : α
⊢ x ∈ uᶜ ↔ x ∈ ⋃ a ∈ {x | ∃ f, {x | ∃ a, (↑(f a))ᶜ = x} = x}, ⋂ 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 : α
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

Tactic:
exact ⟨fun ⟨a, ha⟩ ↦ ⟨f a ha, (hf a ha).1⟩, fun _ a ha h ↦ by rw [← h]; exact (hf a ha).2⟩

Result:
no goals

Proof state:
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ᶜ ∈ 𝒜

Tactic:
exact hAu 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 : {u} ∈ {{u}}
t : Set α
ht : u ∈ {u}
⊢ u ∈ 𝒜 ∨ uᶜ ∈ 𝒜

Tactic:
exact Or.inl u_mem

Result:
no goals