-- 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 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

Tactic:
exact mem_Av a ha

Result:
no goals

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

Tactic:
refine ⟨{{u}}, finite_singleton {u},
  fun a ha ↦ eq_of_mem_singleton ha ▸ finite_singleton u,
  fun a ha t ht ↦ ?_, by simp⟩

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

Proof state:
α : 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
x✝ : Set α
a : Set (Set α)
ha : a ∈ A
h :
  (↑((fun x_1 =>
            match x_1 with
            | ⟨a, ha⟩ => ⟨f a ha, ⋯⟩)
          ⟨a, ⋯⟩))ᶜ =
    x✝
⊢ x ∈ x✝

Tactic:
rw [← h]

Result:
α : 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
x✝ : Set α
a : Set (Set α)
ha : a ∈ A
h :
  (↑((fun x_1 =>
            match x_1 with
            | ⟨a, ha⟩ => ⟨f a ha, ⋯⟩)
          ⟨a, ⋯⟩))ᶜ =
    x✝
⊢ x ∈
    (↑((fun x_1 =>
            match x_1 with
            | ⟨a, ha⟩ => ⟨f a ha, ⋯⟩)
          ⟨a, ⋯⟩))ᶜ

Proof state:
case union.intro.intro.intro.intro
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
v_ind : ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ v = ⋃ a ∈ A, ⋂ t ∈ a, t
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
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
rcases v_ind with ⟨Av, Av_fin, mem_Av, hAv, v_eq⟩

Result:
case union.intro.intro.intro.intro.intro.intro.intro.intro
α : 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, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u ∪ v = ⋃ a ∈ A, ⋂ t ∈ a, t