feat(order/complete_boolean_algebra): A frame is distributive (#15340)

`frame α`/`coframe α` imply `distrib_lattice α`.

Author: YaelDillies

src/order/complete_boolean_algebra.lean

@@ -142,6 +142,11 @@ instance pi.frame {ι : Type*} {π : ι → Type*} [Π i, frame (π i)] : frame
       ← supr_subtype''],
   ..pi.complete_lattice }
 
+@[priority 100] -- see Note [lower instance priority]
+instance frame.to_distrib_lattice : distrib_lattice α :=
+distrib_lattice.of_inf_sup_le $ λ a b c,
+  by rw [←Sup_pair, ←Sup_pair, inf_Sup_eq, ←Sup_image, image_pair]
+
 end frame
 
 section coframe
@@ -189,6 +194,11 @@ instance pi.coframe {ι : Type*} {π : ι → Type*} [Π i, coframe (π i)] : co
     by simp only [←sup_infi_eq, Inf_apply, ←infi_subtype'', infi_apply, pi.sup_apply],
   ..pi.complete_lattice }
 
+@[priority 100] -- see Note [lower instance priority]
+instance coframe.to_distrib_lattice : distrib_lattice α :=
+{ le_sup_inf := λ a b c, by rw [←Inf_pair, ←Inf_pair, sup_Inf_eq, ←Inf_image, image_pair],
+  ..‹coframe α› }
+
 end coframe
 
 section complete_distrib_lattice
@@ -202,12 +212,6 @@ instance pi.complete_distrib_lattice {ι : Type*} {π : ι → Type*}
 
 end complete_distrib_lattice
 
-@[priority 100] -- see Note [lower instance priority]
-instance complete_distrib_lattice.to_distrib_lattice [d : complete_distrib_lattice α] :
-  distrib_lattice α :=
-{ le_sup_inf := λ x y z, by rw [← Inf_pair, ← Inf_pair, sup_Inf_eq, ← Inf_image, set.image_pair],
-  ..d }
-
 /-- A complete Boolean algebra is a completely distributive Boolean algebra. -/
 class complete_boolean_algebra α extends boolean_algebra α, complete_distrib_lattice α
 

src/order/lattice.lean

@@ -553,7 +553,8 @@ end lattice
 equivalent distributive properties (of `sup` over `inf` or `inf` over `sup`,
 on the left or right).
 
-The definition here chooses `le_sup_inf`: `(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)`.
+The definition here chooses `le_sup_inf`: `(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)`. To prove distributivity
+from the dual law, use `distrib_lattice.of_inf_sup_le`.
 
 A classic example of a distributive lattice
 is the lattice of subsets of a set, and in fact this example is
@@ -562,9 +563,6 @@ as a sublattice of a powerset lattice. -/
 class distrib_lattice α extends lattice α :=
 (le_sup_inf : ∀x y z : α, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z))
 
-/- TODO: alternative constructors from the other distributive properties,
-and perhaps a `tfae` statement -/
-
 section distrib_lattice
 variables [distrib_lattice α] {x y z : α}
 
@@ -608,6 +606,13 @@ le_antisymm
 
 end distrib_lattice
 
+/-- Prove distributivity of an existing lattice from the dual distributive law. -/
+@[reducible] -- See note [reducible non-instances]
+def distrib_lattice.of_inf_sup_le [lattice α]
+  (inf_sup_le : ∀ a b c : α, a ⊓ (b ⊔ c) ≤ (a ⊓ b) ⊔ (a ⊓ c)) : distrib_lattice α :=
+{ ..‹lattice α›,
+  ..@order_dual.distrib_lattice αᵒᵈ { le_sup_inf := inf_sup_le, ..order_dual.lattice _ } }
+
 /-!
 ### Lattices derived from linear orders
 -/