feat(BooleanSubalgebra): closure of supClosed+infClosed set containin…

…g bot+top (#20251)

Every element in the closure of such a set `s` can be written as a finite sup of elements of the form `a \ b` with `a`, `b` in `s`.

Mathlib/Order/BooleanSubalgebra.lean

@@ -361,6 +361,44 @@ lemma closure_bot_sup_induction {p : ∀ g ∈ closure s, Prop} (mem : ∀ x hx,
       compl_mem' := fun ⟨_, hb⟩ ↦ ⟨_, compl _ _ hb⟩ }
   closure_le (L := L).mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
 
+section sdiff_sup
+
+variable (sup : SupClosed s) (inf : InfClosed s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s)
+include sup inf bot_mem top_mem
+
+theorem mem_closure_iff_sup_sdiff {a : α} :
+    a ∈ closure s ↔ ∃ t : Finset (s × s), a = t.sup fun x ↦ x.1.1 \ x.2.1 := by
+  classical
+  refine ⟨closure_bot_sup_induction
+    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
+  · rintro ⟨t, rfl⟩
+    exact t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _
+      fun x hx ↦ sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2)
+  · rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩
+    exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩
+  rintro x - ⟨t, rfl⟩
+  refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_
+  simp_rw [Finset.sup_insert, compl_sup, eq]
+  refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_
+  simp_rw [Finset.sup_insert, inf_sup_left, eq]
+  refine ⟨{(z, ⟨_, sup x.2 w.2⟩), (⟨_, inf y.2 z.2⟩, w)} ∪ t, ?_⟩
+  simp_rw [Finset.sup_union, Finset.sup_insert, Finset.sup_singleton, sdiff_eq,
+    compl_sup, inf_left_comm z.1, compl_inf, compl_compl, inf_sup_right, inf_assoc]
+
+@[elab_as_elim] theorem closure_sdiff_sup_induction {p : ∀ g ∈ closure s, Prop}
+    (sdiff : ∀ x hx y hy, p (x \ y) (sdiff_mem (subset_closure hx) (subset_closure hy)))
+    (sup' : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (sup_mem hx hy))
+    {x} (hx : x ∈ closure s) : p x hx := by
+  obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff sup inf bot_mem top_mem).mp hx
+  revert hx
+  classical
+  refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
+  simp only [Finset.sup_insert] at hxt ⊢
+  exact sup' _ _ _ _ (sdiff _ x.1.2 _ x.2.2)
+    (ih <| (mem_closure_iff_sup_sdiff sup inf bot_mem top_mem).mpr ⟨_, rfl⟩)
+
+end sdiff_sup
+
 end BooleanAlgebra
 
 section CompleteBooleanAlgebra