LaTeX
$$$\\exists A: Set(\\text{Set}(\\text{Set} \\alpha)),\\ A\\text{ finite} \\land (\\forall a \\in A, a\\text{ finite}) \\land (\\forall a \\in A, \\forall t \\in a, t \\in 𝒜 \\lor t^{c} \\in 𝒜) \\land s = \\bigcup a \\in A, \\bigcap t \\in a, t$$$
Lean4
/-- If a set belongs to the algebra of sets generated by `𝒜` then it can be written as a finite
union of finite intersections of sets which are in `𝒜` or have their complement in `𝒜`. -/
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 :=
by
induction s_mem with
| base u
u_mem =>
refine
⟨{{ u }}, finite_singleton { u }, fun a ha ↦ eq_of_mem_singleton ha ▸ finite_singleton u, fun a ha t ht ↦ ?_, by
simp⟩
rw [eq_of_mem_singleton ha, ha, eq_of_mem_singleton ht, ht] at *
exact Or.inl u_mem
| empty =>
exact ⟨∅, finite_empty, fun _ h ↦ (notMem_empty _ h).elim, fun _ ha _ _ ↦ (notMem_empty _ ha).elim, by simp⟩
| compl u _ u_ind =>
rcases u_ind with ⟨A, A_fin, mem_A, hA, u_eq⟩
have := finite_coe_iff.2 A_fin
have := fun a : A ↦ finite_coe_iff.2 <| mem_A a.1 a.2
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 ↦ ?_, ?_⟩
· rcases ha with ⟨f, rfl⟩
rcases ht with ⟨a, rfl⟩
rw [compl_compl, or_comm]
exact hA a.1 a.2 (f a).1 (f a).2
· ext x
simp only [u_eq, compl_iUnion, compl_iInter, mem_iInter, mem_iUnion, mem_compl_iff, exists_prop, Subtype.exists,
mem_setOf_eq, iUnion_exists, iUnion_iUnion_eq', iInter_exists]
constructor <;> intro hx
· choose f hf using hx
exact ⟨fun ⟨a, ha⟩ ↦ ⟨f a ha, (hf a ha).1⟩, fun _ a ha h ↦ by rw [← h]; exact (hf a ha).2⟩
· rcases hx with ⟨f, hf⟩
exact fun a ha ↦ ⟨f ⟨a, ha⟩, (f ⟨a, ha⟩).2, hf (f ⟨a, ha⟩)ᶜ a ha rfl⟩
| union u v _ _ u_ind v_ind =>
rcases u_ind with ⟨Au, Au_fin, mem_Au, hAu, u_eq⟩
rcases v_ind with ⟨Av, Av_fin, mem_Av, hAv, v_eq⟩
refine ⟨Au ∪ Av, Au_fin.union Av_fin, ?_, ?_, by rw [u_eq, v_eq, ← biUnion_union]⟩
· rintro a (ha | ha)
· exact mem_Au a ha
· exact mem_Av a ha
· rintro a (ha | ha) t ht
· exact hAu a ha t ht
· exact hAv a ha t ht
