feat(order/boolean_algebra): A bounded generalized boolean algebra is…

… a boolean algebra (#15606)

Abstract the construction of `boolean_algebra (finset α)`.

src/data/fintype/basic.lean

@@ -125,14 +125,7 @@ instance : order_top (finset α) :=
 section boolean_algebra
 variables [decidable_eq α] {a : α}
 
-instance : boolean_algebra (finset α) :=
-{ compl := λ s, univ \ s,
-  inf_compl_le_bot := λ s x hx, by simpa using hx,
-  top_le_sup_compl := λ s x hx, by simp,
-  sdiff_eq := λ s t, by simp [generalized_boolean_algebra.sdiff, ext_iff, compl],
-  ..finset.order_top,
-  ..finset.order_bot,
-  ..finset.generalized_boolean_algebra }
+instance : boolean_algebra (finset α) :=  generalized_boolean_algebra.to_boolean_algebra
 
 lemma compl_eq_univ_sdiff (s : finset α) : sᶜ = univ \ s := rfl
 

src/order/boolean_algebra.lean

@@ -618,6 +618,16 @@ class boolean_algebra (α : Type u) extends distrib_lattice α, has_compl α, ha
 instance boolean_algebra.to_bounded_order [h : boolean_algebra α] : bounded_order α :=
 { ..h }
 
+/-- A bounded generalized boolean algebra is a boolean algebra. -/
+@[reducible] -- See note [reducible non instances]
+def generalized_boolean_algebra.to_boolean_algebra [generalized_boolean_algebra α] [order_top α] :
+  boolean_algebra α :=
+{ compl := λ a, ⊤ \ a,
+  inf_compl_le_bot := λ _, disjoint_sdiff_self_right,
+  top_le_sup_compl := λ _, le_sup_sdiff,
+  sdiff_eq := λ _ _, by { rw [←inf_sdiff_assoc, inf_top_eq], refl },
+  ..‹generalized_boolean_algebra α›, ..generalized_boolean_algebra.to_order_bot, ..‹order_top α› }
+
 section boolean_algebra
 variables [boolean_algebra α]