chore: Golf algebra.order.lattice_group (#2478)

Match leanprover-community/mathlib#18046

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 
 ! This file was ported from Lean 3 source module algebra.order.lattice_group
-! leanprover-community/mathlib commit 10b4e499f43088dd3bb7b5796184ad5216648ab1
+! leanprover-community/mathlib commit 474656fdf40ae1741dfffcdd7c685a0f198da61a
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -81,57 +81,42 @@ variable {α : Type u} [Lattice α] [CommGroup α]
 -- Special case of Bourbaki A.VI.9 (1)
 -- c + (a ⊔ b) = (c + a) ⊔ (c + b)
 @[to_additive]
-theorem mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b := by
-  refine' le_antisymm _ _
-  rw [← mul_le_mul_iff_left (c⁻¹), ← mul_assoc, inv_mul_self, one_mul]
-  apply sup_le
-  rw [le_inv_mul_iff_mul_le]
-  exact le_sup_left'
-  rw [le_inv_mul_iff_mul_le]
-  exact le_sup_right
-  rw [sup_le_iff, mul_le_mul_iff_left, mul_le_mul_iff_left, and_iff_left le_sup_right]
-  exact le_sup_left
+theorem mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : c * (a ⊔ b) = c * a ⊔ c * b :=
+  (OrderIso.mulLeft _).map_sup _ _
 #align mul_sup mul_sup
 #align add_sup add_sup
 
 @[to_additive]
-theorem mul_inf [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : c * (a ⊓ b) = c * a ⊓ c * b := by
-  refine' le_antisymm _ _
-  rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left, and_iff_left inf_le_right]
-  exact inf_le_left
-  rw [← mul_le_mul_iff_left (c⁻¹), ← mul_assoc, inv_mul_self, one_mul]
-  apply le_inf
-  rw [inv_mul_le_iff_le_mul]
-  exact inf_le_left
-  rw [inv_mul_le_iff_le_mul]
-  exact inf_le_right
+theorem sup_mul [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : (a ⊔ b) * c = a * c ⊔ b * c :=
+  (OrderIso.mulRight _).map_sup _ _
+#align sup_mul sup_mul
+#align sup_add sup_add
+
+@[to_additive]
+theorem mul_inf [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : c * (a ⊓ b) = c * a ⊓ c * b :=
+  (OrderIso.mulLeft _).map_inf _ _
 #align mul_inf mul_inf
 #align add_inf add_inf
 
+@[to_additive]
+theorem inf_mul [CovariantClass α α (· * ·) (· ≤ ·)] (a b c : α) : (a ⊓ b) * c = a * c ⊓ b * c :=
+  (OrderIso.mulRight _).map_inf _ _
+#align inf_mul inf_mul
+#align inf_add inf_add
+
 -- Special case of Bourbaki A.VI.9 (2)
 -- -(a ⊔ b)=(-a) ⊓ (-b)
 @[to_additive]
 theorem inv_sup_eq_inv_inf_inv [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) :
-    (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹ := by
-  apply le_antisymm
-  · refine' le_inf _ _
-    · rw [inv_le_inv_iff]
-      exact le_sup_left
-    · rw [inv_le_inv_iff]
-      exact le_sup_right
-  · rw [← inv_le_inv_iff, inv_inv]
-    refine' sup_le _ _
-    · rw [← inv_le_inv_iff]
-      simp
-    · rw [← inv_le_inv_iff]
-      simp
+    (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹ :=
+  (OrderIso.inv α).map_sup _ _
 #align inv_sup_eq_inv_inf_inv inv_sup_eq_inv_inf_inv
 #align neg_sup_eq_neg_inf_neg neg_sup_eq_neg_inf_neg
 
 -- -(a ⊓ b) = -a ⊔ -b
 @[to_additive]
 theorem inv_inf_eq_sup_inv [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹ :=
-  by rw [← inv_inv (a⁻¹ ⊔ b⁻¹), inv_sup_eq_inv_inf_inv a⁻¹ b⁻¹, inv_inv, inv_inv]
+  (OrderIso.inv α).map_inf _ _
 #align inv_inf_eq_sup_inv inv_inf_eq_sup_inv
 #align neg_inf_eq_sup_neg neg_inf_eq_sup_neg
 
@@ -140,10 +125,8 @@ theorem inv_inf_eq_sup_inv [CovariantClass α α (· * ·) (· ≤ ·)] (a b : 
 @[to_additive]
 theorem inf_mul_sup [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b :=
   calc
-    (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) :=
-    by
-      rw [mul_sup b⁻¹ a⁻¹ (a * b)]
-      simp
+    (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) := by
+      rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
     _ = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) := by rw [inv_inf_eq_sup_inv, sup_comm]
     _ = a * b := by rw [mul_comm, inv_mul_cancel_right]
 
@@ -238,40 +221,32 @@ theorem one_le_neg (a : α) : 1 ≤ a⁻ :=
 -- pos_nonpos_iff
 @[to_additive]
 theorem pos_le_one_iff {a : α} : a⁺ ≤ 1 ↔ a ≤ 1 := by
-  rw [m_pos_part_def, sup_le_iff]
-  simp
+  rw [m_pos_part_def, sup_le_iff, and_iff_left le_rfl]
 #align lattice_ordered_comm_group.pos_le_one_iff LatticeOrderedCommGroup.pos_le_one_iff
 #align lattice_ordered_comm_group.pos_nonpos_iff LatticeOrderedCommGroup.pos_nonpos_iff
 
 -- neg_nonpos_iff
 @[to_additive]
 theorem neg_le_one_iff {a : α} : a⁻ ≤ 1 ↔ a⁻¹ ≤ 1 := by
-  rw [m_neg_part_def, sup_le_iff]
-  simp
+  rw [m_neg_part_def, sup_le_iff, and_iff_left le_rfl]
 #align lattice_ordered_comm_group.neg_le_one_iff LatticeOrderedCommGroup.neg_le_one_iff
 #align lattice_ordered_comm_group.neg_nonpos_iff LatticeOrderedCommGroup.neg_nonpos_iff
 
 @[to_additive]
-theorem pos_eq_one_iff {a : α} : a⁺ = 1 ↔ a ≤ 1 := by
-  rw [le_antisymm_iff]
-  simp only [one_le_pos, and_true_iff]
-  exact pos_le_one_iff
+theorem pos_eq_one_iff {a : α} : a⁺ = 1 ↔ a ≤ 1 :=
+  sup_eq_right
 #align lattice_ordered_comm_group.pos_eq_one_iff LatticeOrderedCommGroup.pos_eq_one_iff
 #align lattice_ordered_comm_group.pos_eq_zero_iff LatticeOrderedCommGroup.pos_eq_zero_iff
 
 @[to_additive]
-theorem neg_eq_one_iff' {a : α} : a⁻ = 1 ↔ a⁻¹ ≤ 1 := by
-  rw [le_antisymm_iff]
-  simp only [one_le_neg, and_true_iff]
-  rw [neg_le_one_iff]
+theorem neg_eq_one_iff' {a : α} : a⁻ = 1 ↔ a⁻¹ ≤ 1 :=
+  sup_eq_right
 #align lattice_ordered_comm_group.neg_eq_one_iff' LatticeOrderedCommGroup.neg_eq_one_iff'
 #align lattice_ordered_comm_group.neg_eq_zero_iff' LatticeOrderedCommGroup.neg_eq_zero_iff'
 
 @[to_additive]
 theorem neg_eq_one_iff [CovariantClass α α Mul.mul LE.le] {a : α} : a⁻ = 1 ↔ 1 ≤ a := by
-  rw [le_antisymm_iff]
-  simp only [one_le_neg, and_true_iff]
-  rw [neg_le_one_iff, inv_le_one']
+  rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]
 #align lattice_ordered_comm_group.neg_eq_one_iff LatticeOrderedCommGroup.neg_eq_one_iff
 #align lattice_ordered_comm_group.neg_eq_zero_iff LatticeOrderedCommGroup.neg_eq_zero_iff
 
@@ -298,7 +273,7 @@ theorem neg_eq_pos_inv (a : α) : a⁻ = a⁻¹⁺ :=
 
 -- a⁺ = (-a)⁻
 @[to_additive]
-theorem pos_eq_neg_inv (a : α) : a⁺ = a⁻¹⁻ := by simp [neg_eq_pos_inv]
+theorem pos_eq_neg_inv (a : α) : a⁺ = a⁻¹⁻ := by rw [neg_eq_pos_inv, inv_inv]
 #align lattice_ordered_comm_group.pos_eq_neg_inv LatticeOrderedCommGroup.pos_eq_neg_inv
 #align lattice_ordered_comm_group.pos_eq_neg_neg LatticeOrderedCommGroup.pos_eq_neg_neg
 
@@ -331,8 +306,8 @@ theorem pos_div_neg [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : a⁺
 -- a⁺ ⊓ a⁻ = 0 (`a⁺` and `a⁻` are co-prime, and, since they are positive, disjoint)
 @[to_additive]
 theorem pos_inf_neg_eq_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : a⁺ ⊓ a⁻ = 1 := by
-  rw [← mul_right_inj (a⁻)⁻¹, mul_inf_eq_mul_inf_mul, mul_one, mul_left_inv, mul_comm, ←
-    div_eq_mul_inv, pos_div_neg, neg_eq_inv_inf_one, inv_inv]
+  rw [← mul_right_inj (a⁻)⁻¹, mul_inf, mul_one, mul_left_inv, mul_comm, ← div_eq_mul_inv,
+    pos_div_neg, neg_eq_inv_inf_one, inv_inv]
 #align lattice_ordered_comm_group.pos_inf_neg_eq_one LatticeOrderedCommGroup.pos_inf_neg_eq_one
 #align lattice_ordered_comm_group.pos_inf_neg_eq_zero LatticeOrderedCommGroup.pos_inf_neg_eq_zero
 
@@ -355,7 +330,7 @@ theorem inf_eq_div_pos_div [CovariantClass α α (· * ·) (· ≤ ·)] (a b : 
   calc
     a ⊓ b = a * 1 ⊓ a * (b / a) :=
       by rw [mul_one a, div_eq_mul_inv, mul_comm b, mul_inv_cancel_left]
-    _ = a * (1 ⊓ b / a) := by rw [← mul_inf_eq_mul_inf_mul 1 (b / a) a]
+    _ = a * (1 ⊓ b / a) := by rw [← mul_inf 1 (b / a) a]
     _ = a * (b / a ⊓ 1) := by rw [inf_comm]
     _ = a * ((a / b)⁻¹ ⊓ 1) :=
       by
@@ -415,17 +390,9 @@ theorem one_le_abs [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : 1 ≤
 -- |a| = a⁺ - a⁻
 @[to_additive]
 theorem pos_mul_neg [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) : |a| = a⁺ * a⁻ := by
-  refine' le_antisymm _ _
-  · refine' sup_le _ _
-    · nth_rw 1 [← mul_one a]
-      exact mul_le_mul' (m_le_pos a) (one_le_neg a)
-    · nth_rw 1 [← one_mul a⁻¹]
-      exact mul_le_mul' (one_le_pos a) (inv_le_neg a)
-  · rw [← inf_mul_sup, pos_inf_neg_eq_one, one_mul, ← m_pos_abs a]
-    apply sup_le
-    · exact ((m_le_iff_pos_le_neg_ge _ _).mp (le_mabs a)).left
-    · rw [neg_eq_pos_inv]
-      exact ((m_le_iff_pos_le_neg_ge _ _).mp (inv_le_abs a)).left
+  rw [m_pos_part_def, sup_mul, one_mul, m_neg_part_def, mul_sup, mul_one, mul_inv_self, sup_assoc,
+    ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
+  exact (sup_eq_left.2 <| one_le_abs a).symm
 #align lattice_ordered_comm_group.pos_mul_neg LatticeOrderedCommGroup.pos_mul_neg
 #align lattice_ordered_comm_group.pos_add_neg LatticeOrderedCommGroup.pos_add_neg
 
@@ -494,10 +461,9 @@ theorem abs_div_sup_mul_abs_div_inf [CovariantClass α α (· * ·) (· ≤ ·)]
       by rw [sup_div_inf_eq_abs_div]
     _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) :=
       by rw [sup_div_inf_eq_abs_div (b ⊓ c) (a ⊓ c)]
-    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) :=
-      by
-        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, @sup_comm _ _ c (a⊔c), sup_right_idem,
-          sup_assoc, inf_assoc, @inf_comm _ _ c (a⊓c), inf_right_idem, inf_assoc]
+    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
+      rw [← sup_inf_right, ← inf_sup_right, sup_assoc, @sup_comm _ _ c (a ⊔ c), sup_right_idem,
+        sup_assoc, inf_assoc, @inf_comm _ _ c (a ⊓ c), inf_right_idem, inf_assoc]
     _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
     _ = (b ⊔ a) * c / ((b ⊓ a) * c) :=
       by rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
@@ -551,10 +517,8 @@ theorem neg_of_inv_le_one (a : α) (h : a⁻¹ ≤ 1) : a⁻ = 1 :=
 
 -- neg_of_nonpos
 @[to_additive]
-theorem neg_of_le_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : a ≤ 1) : a⁻ = a⁻¹ := by
-  refine' neg_of_one_le_inv _ _
-  rw [one_le_inv']
-  exact h
+theorem neg_of_le_one [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : a ≤ 1) : a⁻ = a⁻¹ :=
+  sup_eq_left.2 <| one_le_inv'.2 h
 #align lattice_ordered_comm_group.neg_of_le_one LatticeOrderedCommGroup.neg_of_le_one
 #align lattice_ordered_comm_group.neg_of_nonpos LatticeOrderedCommGroup.neg_of_nonpos
 
@@ -567,11 +531,8 @@ theorem neg_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h :
 
 -- 0 ≤ a implies |a| = a
 @[to_additive abs_of_nonneg]
-theorem mabs_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : 1 ≤ a) : |a| = a := by
-  rw [abs_eq_sup_inv, sup_eq_mul_pos_div, div_eq_mul_inv, inv_inv, ← pow_two, inv_mul_eq_iff_eq_mul,
-    ← pow_two, pos_of_one_le]
-  rw [pow_two]
-  apply one_le_mul h h
+theorem mabs_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)] (a : α) (h : 1 ≤ a) : |a| = a :=
+  sup_eq_left.2 <| Left.inv_le_self h
 #align lattice_ordered_comm_group.mabs_of_one_le LatticeOrderedCommGroup.mabs_of_one_le
 #align lattice_ordered_comm_group.abs_of_nonneg LatticeOrderedCommGroup.abs_of_nonneg
 
@@ -641,9 +602,8 @@ theorem abs_abs_div_abs_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : 
   constructor
   · 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_mul_cancel']
+  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, abs_inv_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