refactor(Topology/ContinuousFunction/Algebra): lattice ordered group …

…gives inf/sup formula (#6205)

Previously the following comment occured in `Topology.ContinuousFunction.Algebra`:

> -- TODO:
-- This lemma (and the next) could go all the way back in `Algebra.Order.Field`,
-- except that it is tedious to prove without tactics.
-- Rather than stranding it at some intermediate location,
-- it's here, immediately prior to the point of use.

Subsequently, the theory of lattice ordered groups has been developed in Mathlib (Algebra.Order.LatticeGroup). This now provides the natural "intermediate location" for these lemmas, they are an immediate consequence of `LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub` and `LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub`. In fact we can show that `C(α, β)` is itself a lattice ordered group and hence expressions for the `inf` and `sup` (`inf_eq` and `sup_eq`) can be deduced directly from `LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub` and `LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub`.

This was previously submitted to Mathlib leanprover-community/mathlib3#18780



Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -3,8 +3,9 @@ Copyright (c) 2021 Christopher Hoskin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 -/
-import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Algebra.Invertible
+import Mathlib.Algebra.Module.Basic
 import Mathlib.Order.Closure
 
 #align_import algebra.order.lattice_group from "leanprover-community/mathlib"@"5dc275ec639221ca4d5f56938eb966f6ad9bc89f"
@@ -59,12 +60,9 @@ lattices.
 lattice, ordered, group
 -/
 
+universe u v
 
--- Needed for squares
--- Needed for squares
-universe u
-
-variable {α : Type u} [Lattice α] [CommGroup α]
+variable {α : Type u} {β : Type v} [Lattice α] [CommGroup α]
 
 -- Special case of Bourbaki A.VI.9 (1)
 -- c + (a ⊔ b) = (c + a) ⊔ (c + b)
@@ -571,11 +569,11 @@ theorem mabs_mul_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |a
 
 -- |a - b| = |b - a|
 @[to_additive]
-theorem abs_inv_comm (a b : α) : |a / b| = |b / a| := by
+theorem abs_div_comm (a b : α) : |a / b| = |b / a| := by
   dsimp only [Abs.abs]
   rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
-#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_inv_comm
-#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_neg_comm
+#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_div_comm
+#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_sub_comm
 
 -- | |a| - |b| | ≤ |a - b|
 @[to_additive]
@@ -586,17 +584,51 @@ theorem abs_abs_div_abs_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : 
   · apply div_le_iff_le_mul.2
     convert mabs_mul_le (a / b) b
     rw [div_mul_cancel']
-  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, abs_inv_comm]
+  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, abs_div_comm]
     convert mabs_mul_le (b / a) a
     · rw [div_mul_cancel']
 #align lattice_ordered_comm_group.abs_abs_div_abs_le LatticeOrderedCommGroup.abs_abs_div_abs_le
 #align lattice_ordered_comm_group.abs_abs_sub_abs_le LatticeOrderedCommGroup.abs_abs_sub_abs_le
 
 end LatticeOrderedCommGroup
 
+section invertible
+
+variable (α)
+variable [Semiring α] [Invertible (2 : α)] [Lattice β] [AddCommGroup β] [Module α β]
+  [CovariantClass β β (· + ·) (· ≤ ·)]
+
+lemma inf_eq_half_smul_add_sub_abs_sub (x y : β) :
+  x ⊓ y = (⅟2 : α) • (x + y - |y - x|) :=
+by rw [←LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub x y, two_smul, ←two_smul α,
+    smul_smul, invOf_mul_self, one_smul]
+
+lemma sup_eq_half_smul_add_add_abs_sub (x y : β) :
+  x ⊔ y = (⅟2 : α) • (x + y + |y - x|) :=
+by rw [←LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub x y, two_smul, ←two_smul α,
+    smul_smul, invOf_mul_self, one_smul]
+
+end invertible
+
+section DivisionSemiring
+
+variable (α)
+variable [DivisionSemiring α] [NeZero (2 : α)] [Lattice β] [AddCommGroup β] [Module α β]
+  [CovariantClass β β (· + ·) (· ≤ ·)]
+
+lemma inf_eq_half_smul_add_sub_abs_sub' (x y : β) : x ⊓ y = (2⁻¹ : α) • (x + y - |y - x|) := by
+  letI := invertibleOfNonzero (two_ne_zero' α)
+  exact inf_eq_half_smul_add_sub_abs_sub α x y
+
+lemma sup_eq_half_smul_add_add_abs_sub' (x y : β) : x ⊔ y = (2⁻¹ : α) • (x + y + |y - x|) := by
+  letI := invertibleOfNonzero (two_ne_zero' α)
+  exact sup_eq_half_smul_add_add_abs_sub α x y
+
+end DivisionSemiring
+
 namespace LatticeOrderedAddCommGroup
 
-variable {β : Type u} [Lattice β] [AddCommGroup β]
+variable [Lattice β] [AddCommGroup β]
 
 section solid
 

Mathlib/Topology/ContinuousFunction/Algebra.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
 import Mathlib.Algebra.Algebra.Pi
+import Mathlib.Algebra.Order.LatticeGroup
 import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Star.StarAlgHom
@@ -900,45 +901,27 @@ We now provide formulas for `f ⊓ g` and `f ⊔ g`, where `f g : C(α, β)`,
 in terms of `ContinuousMap.abs`.
 -/
 
-
-section
-
-variable {R : Type _} [LinearOrderedField R]
-
--- TODO:
--- This lemma (and the next) could go all the way back in `Algebra.Order.Field`,
--- except that it is tedious to prove without tactics.
--- Rather than stranding it at some intermediate location,
--- it's here, immediately prior to the point of use.
-theorem min_eq_half_add_sub_abs_sub {x y : R} : min x y = 2⁻¹ * (x + y - |x - y|) := by
-  cases' le_total x y with h h <;> field_simp [h, abs_of_nonneg, abs_of_nonpos, mul_two]
-  abel
-#align min_eq_half_add_sub_abs_sub min_eq_half_add_sub_abs_sub
-
-theorem max_eq_half_add_add_abs_sub {x y : R} : max x y = 2⁻¹ * (x + y + |x - y|) := by
-  cases' le_total x y with h h <;> field_simp [h, abs_of_nonneg, abs_of_nonpos, mul_two]
-  abel
-#align max_eq_half_add_add_abs_sub max_eq_half_add_add_abs_sub
-
-end
-
 namespace ContinuousMap
 
 section Lattice
 
 variable {α : Type _} [TopologicalSpace α]
 
-variable {β : Type _} [LinearOrderedField β] [TopologicalSpace β] [OrderTopology β]
-  [TopologicalRing β]
+variable {β : Type _} [TopologicalSpace β]
+
+/-! `C(α, β)`is a lattice ordered group -/
 
-theorem inf_eq (f g : C(α, β)) : f ⊓ g = (2⁻¹ : β) • (f + g - |f - g|) :=
-  ext fun x => by simpa using min_eq_half_add_sub_abs_sub
-#align continuous_map.inf_eq ContinuousMap.inf_eq
+@[to_additive]
+instance covariant_class_mul_le_left [PartialOrder β] [Mul β] [ContinuousMul β]
+  [CovariantClass β β (· * ·) (· ≤ ·)] :
+  CovariantClass C(α, β) C(α, β) (· * ·) (· ≤ ·) :=
+⟨fun _ _ _ hg₁₂ x => mul_le_mul_left' (hg₁₂ x) _⟩
 
--- Not sure why this is grosser than `inf_eq`:
-theorem sup_eq (f g : C(α, β)) : f ⊔ g = (2⁻¹ : β) • (f + g + |f - g|) :=
-  ext fun x => by simpa [mul_add] using @max_eq_half_add_add_abs_sub _ _ (f x) (g x)
-#align continuous_map.sup_eq ContinuousMap.sup_eq
+@[to_additive]
+instance covariant_class_mul_le_right [PartialOrder β] [Mul β] [ContinuousMul β]
+  [CovariantClass β β (Function.swap (· * ·)) (· ≤ ·)] :
+  CovariantClass C(α, β) C(α, β) (Function.swap (· * ·)) (· ≤ ·) :=
+⟨fun _ _ _ hg₁₂ x => mul_le_mul_right' (hg₁₂ x) _⟩
 
 end Lattice
 

Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

@@ -118,7 +118,7 @@ theorem abs_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f : A) :
 
 theorem inf_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f g : A) :
     (f : C(X, ℝ)) ⊓ (g : C(X, ℝ)) ∈ A.topologicalClosure := by
-  rw [inf_eq]
+  rw [inf_eq_half_smul_add_sub_abs_sub' ℝ]
   refine'
     A.topologicalClosure.smul_mem
       (A.topologicalClosure.sub_mem
@@ -140,7 +140,7 @@ theorem inf_mem_closed_subalgebra (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed (
 
 theorem sup_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f g : A) :
     (f : C(X, ℝ)) ⊔ (g : C(X, ℝ)) ∈ A.topologicalClosure := by
-  rw [sup_eq]
+  rw [sup_eq_half_smul_add_add_abs_sub' ℝ]
   refine'
     A.topologicalClosure.smul_mem
       (A.topologicalClosure.add_mem