[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
⊢ 1⁻ = 1
[PROOFSTEP]
rw [m_neg_part_def, inv_one, sup_idem]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁻ = (a ⊓ 1)⁻¹
[PROOFSTEP]
rw [m_neg_part_def, ← inv_inj, inv_sup_eq_inv_inf_inv, inv_inv, inv_inv, inv_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻¹ ⊔ a⁻¹⁻¹ = a ⊔ a⁻¹
[PROOFSTEP]
rw [inv_inv, sup_comm]
  -- 0 ≤ a⁺
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁺ ≤ 1 ↔ a ≤ 1
[PROOFSTEP]
rw [m_pos_part_def, sup_le_iff, and_iff_left le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻ ≤ 1 ↔ a⁻¹ ≤ 1
[PROOFSTEP]
rw [m_neg_part_def, sup_le_iff, and_iff_left le_rfl]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α Mul.mul LE.le
a : α
⊢ a⁻ = 1 ↔ 1 ≤ a
[PROOFSTEP]
rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁺ = a⁻¹⁻
[PROOFSTEP]
rw [neg_eq_pos_inv, inv_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) = c * a ⊓ c * b
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) ≤ c * a ⊓ c * b
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left]
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a ⊓ b ≤ a ∧ a ⊓ b ≤ b
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
[PROOFSTEP]
rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul, le_inf_iff, inv_mul_le_iff_le_mul,
  inv_mul_le_iff_le_mul]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * a ∧ c * a ⊓ c * b ≤ c * b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁺ / a⁻ = a
[PROOFSTEP]
symm
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a = a⁺ / a⁻
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a = a⁺ * a⁻⁻¹
[PROOFSTEP]
apply eq_mul_inv_of_mul_eq
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a * a⁻ = a⁺
[PROOFSTEP]
rw [m_neg_part_def, mul_sup, mul_one, mul_right_inv, sup_comm, m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a
⊢ a⁺ = a
[PROOFSTEP]
rw [m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a
⊢ a ⊔ 1 = a
[PROOFSTEP]
exact sup_of_le_left h
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻ = a⁻¹
[PROOFSTEP]
rw [neg_eq_pos_inv]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a : α
h : 1 ≤ a⁻¹
⊢ a⁻¹⁺ = a⁻¹
[PROOFSTEP]
exact pos_of_one_le _ h
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x⁺
⊢ x⁺ = x
[PROOFSTEP]
rw [m_pos_part_def, right_lt_sup, not_le] at hx 
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ x⁺ = x
[PROOFSTEP]
rw [m_pos_part_def, sup_eq_left]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : Group α✝
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : CommGroup α
x : α
hx : 1 < x
⊢ 1 ≤ x
[PROOFSTEP]
exact hx.le
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ |a / b| = |b / a|
[PROOFSTEP]
dsimp only [Abs.abs]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Lattice α
inst✝ : Group α
a b : α
⊢ a / b ⊔ (a / b)⁻¹ = b / a ⊔ (b / a)⁻¹
[PROOFSTEP]
rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ a ^ 2 → 1 ≤ a
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
⊢ 1 ≤ a
[PROOFSTEP]
have e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 := by
  rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm, inf_assoc, (inf_of_le_left h)]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
[PROOFSTEP]
rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm, inf_assoc, (inf_of_le_left h)]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ 1 ≤ a
[PROOFSTEP]
rw [← inf_eq_right]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
h : 1 ≤ a ^ 2
e1 : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ a ⊓ 1 = 1
[PROOFSTEP]
exact mul_right_eq_self.mp e1
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply pow_two_semiclosed _ _
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a| ^ 2
[PROOFSTEP]
rw [abs_eq_sup_inv, pow_two, mul_sup, sup_mul, ← pow_two, mul_left_inv, sup_comm, ← sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ a ^ 2 ⊔ 1
[PROOFSTEP]
apply le_sup_right
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| = a⁺ * a⁻
[PROOFSTEP]
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]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| = a ⊔ a⁻¹ ⊔ 1
[PROOFSTEP]
exact (sup_eq_left.2 <| one_le_abs a).symm
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁺ = |a|
[PROOFSTEP]
rw [m_pos_part_def]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a| ⊔ 1 = |a|
[PROOFSTEP]
apply sup_of_le_left
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply one_le_abs
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻ = 1
[PROOFSTEP]
rw [m_neg_part_def]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻¹ ⊔ 1 = 1
[PROOFSTEP]
apply sup_of_le_right
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ |a|⁻¹ ≤ 1
[PROOFSTEP]
rw [Left.inv_le_one_iff]
[GOAL]
case a
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ 1 ≤ |a|
[PROOFSTEP]
apply one_le_abs
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = (a ⊔ b) * (a⁻¹ ⊔ b⁻¹)
[PROOFSTEP]
rw [div_eq_mul_inv, ← inv_inf_eq_sup_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) * (a⁻¹ ⊔ b⁻¹) = a * a⁻¹ ⊔ b * a⁻¹ ⊔ (a * b⁻¹ ⊔ b * b⁻¹)
[PROOFSTEP]
rw [mul_sup, sup_mul, sup_mul]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * a⁻¹ ⊔ b * a⁻¹ ⊔ (a * b⁻¹ ⊔ b * b⁻¹) = 1 ⊔ b / a ⊔ (a / b ⊔ 1)
[PROOFSTEP]
rw [mul_right_inv, mul_right_inv, ← div_eq_mul_inv, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ (a / b ⊔ 1) = 1 ⊔ b / a ⊔ (1 / (b / a) ⊔ 1)
[PROOFSTEP]
rw [one_div_div]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ (1 / (b / a) ⊔ 1) = 1 ⊔ b / a ⊔ ((b / a)⁻¹ ⊔ 1)
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ b / a ⊔ ((b / a)⁻¹ ⊔ 1) = 1 ⊔ (b / a ⊔ (b / a)⁻¹ ⊔ 1)
[PROOFSTEP]
rw [sup_assoc, sup_assoc]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ (b / a ⊔ (b / a)⁻¹ ⊔ 1) = 1 ⊔ (|b / a| ⊔ 1)
[PROOFSTEP]
rw [abs_eq_sup_inv]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ (|b / a| ⊔ 1) = 1 ⊔ |b / a|
[PROOFSTEP]
rw [← m_pos_part_def, m_pos_abs]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ 1 ⊔ |b / a| = |b / a| ⊔ 1
[PROOFSTEP]
rw [sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |b / a| ⊔ 1 = |b / a|
[PROOFSTEP]
rw [← m_pos_part_def, m_pos_abs]
[GOAL]
α : Type u
β : Type v
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ a⁺ ⊓ a⁻ = 1
[PROOFSTEP]
rw [← mul_left_inj (a⁻)⁻¹, inf_mul, one_mul, mul_right_inv, ← div_eq_mul_inv, pos_div_neg, neg_eq_inv_inf_one, inv_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
[PROOFSTEP]
rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)
[PROOFSTEP]
rw [inv_inf_eq_sup_inv, sup_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b
[PROOFSTEP]
rw [mul_comm, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊔ b = b * (a / b) ⊔ b * 1
[PROOFSTEP]
rw [mul_one b, div_eq_mul_inv, mul_comm a, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ b * (a / b) ⊔ b * 1 = b * (a / b ⊔ 1)
[PROOFSTEP]
rw [← mul_sup (a / b) 1 b]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊓ b = a * 1 ⊓ a * (b / a)
[PROOFSTEP]
rw [mul_one a, div_eq_mul_inv, mul_comm b, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * 1 ⊓ a * (b / a) = a * (1 ⊓ b / a)
[PROOFSTEP]
rw [← mul_inf 1 (b / a) a]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (1 ⊓ b / a) = a * (b / a ⊓ 1)
[PROOFSTEP]
rw [inf_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b / a ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
nth_rw 1 [← inv_inv b]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b⁻¹⁻¹ * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
[PROOFSTEP]
rw [← mul_inv, mul_comm b⁻¹, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1⁻¹)
[PROOFSTEP]
rw [inv_one]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1⁻¹) = a / (a / b ⊔ 1)
[PROOFSTEP]
rw [← inv_sup_eq_inv_inf_inv, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ≤ b → a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻ → a ≤ b
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
[PROOFSTEP]
constructor
[GOAL]
case mp.left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a⁺ ≤ b⁺
[PROOFSTEP]
exact sup_le (h.trans (m_le_pos b)) (one_le_pos b)
[GOAL]
case mp.right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ b⁻ ≤ a⁻
[PROOFSTEP]
rw [← inv_le_inv_iff] at h 
[GOAL]
case mp.right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h✝ : a ≤ b
h : b⁻¹ ≤ a⁻¹
⊢ b⁻ ≤ a⁻
[PROOFSTEP]
exact sup_le (h.trans (inv_le_neg a)) (one_le_neg a)
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
⊢ a ≤ b
[PROOFSTEP]
rw [← pos_div_neg a, ← pos_div_neg b]
[GOAL]
case mpr
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
h : a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻
⊢ a⁺ / a⁻ ≤ b⁺ / b⁻
[PROOFSTEP]
exact div_le_div'' h.1 h.2
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊔ b) ^ 2 = a * b * |b / a|
[PROOFSTEP]
rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, ← mul_assoc, mul_comm, mul_assoc, ← pow_two,
  inv_mul_cancel_left]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a ⊓ b) ^ 2 = a * b / |b / a|
[PROOFSTEP]
rw [← inf_mul_sup a b, ← sup_div_inf_eq_abs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv, mul_assoc,
  mul_inv_cancel_comm_assoc, ← pow_two]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
intros x y z
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
[PROOFSTEP]
rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul, le_inf_iff]
[GOAL]
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
[PROOFSTEP]
constructor
[GOAL]
case left
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
[PROOFSTEP]
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
[GOAL]
case left
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
[PROOFSTEP]
apply mul_le_mul'
[GOAL]
case left.h₁
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x ⊓ (y ⊓ z) ≤ x ⊓ y
[PROOFSTEP]
apply inf_le_inf_left
[GOAL]
case left.h₁.h
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ y ⊓ z ≤ y
[PROOFSTEP]
apply inf_le_left
[GOAL]
case left.h₂
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y
[PROOFSTEP]
apply inf_le_left
[GOAL]
case right
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
[PROOFSTEP]
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
[GOAL]
case right
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
[PROOFSTEP]
apply mul_le_mul'
[GOAL]
case right.h₁
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ x ⊓ (y ⊓ z) ≤ x ⊓ z
[PROOFSTEP]
apply inf_le_inf_left
[GOAL]
case right.h₁.h
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ y ⊓ z ≤ z
[PROOFSTEP]
apply inf_le_right
[GOAL]
case right.h₂
α✝ : Type u
β : Type v
inst✝³ : Lattice α✝
inst✝² : CommGroup α✝
α : Type u
s : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ z
[PROOFSTEP]
apply inf_le_right
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b|
[PROOFSTEP]
letI : DistribLattice α := LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice α
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b|
[PROOFSTEP]
calc
  |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)| := 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 [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]
  _ = (b ⊔ a) / (b ⊓ a) := by rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
  _ = |a / b| := by rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ |(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)| =
    (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c)))
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div (b ⊓ c) (a ⊓ c)]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c))
[PROOFSTEP]
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]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c))
[PROOFSTEP]
rw [div_mul_div_comm]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) = (b ⊔ a) * c / ((b ⊓ a) * c)
[PROOFSTEP]
rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a) * c / ((b ⊓ a) * c) = (b ⊔ a) / (b ⊓ a)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
this : DistribLattice α := latticeOrderedCommGroupToDistribLattice α
⊢ (b ⊔ a) / (b ⊓ a) = |a / b|
[PROOFSTEP]
rw [sup_div_inf_eq_abs_div]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| ≤ |a / b|
[PROOFSTEP]
apply le_of_mul_le_of_one_le_left
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)| * ?b ≤ |a / b|
[PROOFSTEP]
rw [abs_div_sup_mul_abs_div_inf]
[GOAL]
case hle
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ |(a ⊓ c) / (b ⊓ c)|
[PROOFSTEP]
exact one_le_abs _
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ |(a ⊓ c) / (b ⊓ c)| ≤ |a / b|
[PROOFSTEP]
apply le_of_mul_le_of_one_le_right
[GOAL]
case h
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ ?a * |(a ⊓ c) / (b ⊓ c)| ≤ |a / b|
[PROOFSTEP]
rw [abs_div_sup_mul_abs_div_inf]
[GOAL]
case hle
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ 1 ≤ |(a ⊔ c) / (b ⊔ c)|
[PROOFSTEP]
exact one_le_abs _
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a * b| ≤ |a| * |b|
[PROOFSTEP]
apply sup_le
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * b ≤ |a| * |b|
[PROOFSTEP]
exact mul_le_mul' (le_mabs a) (le_mabs b)
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (a * b)⁻¹ ≤ |a| * |b|
[PROOFSTEP]
rw [mul_inv]
[GOAL]
case a
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a| * |b|
[PROOFSTEP]
exact mul_le_mul' (inv_le_abs _) (inv_le_abs _)
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ ||a| / |b|| ≤ |a / b|
[PROOFSTEP]
rw [abs_eq_sup_inv, sup_le_iff]
[GOAL]
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| / |b| ≤ |a / b| ∧ (|a| / |b|)⁻¹ ≤ |a / b|
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| / |b| ≤ |a / b|
[PROOFSTEP]
apply div_le_iff_le_mul.2
[GOAL]
case left
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |a| ≤ |a / b| * |b|
[PROOFSTEP]
convert mabs_mul_le (a / b) b
[GOAL]
case h.e'_3.h.e'_3
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a = a / b * b
[PROOFSTEP]
rw [div_mul_cancel']
[GOAL]
case right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ (|a| / |b|)⁻¹ ≤ |a / b|
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, abs_div_comm]
[GOAL]
case right
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ |b| ≤ |b / a| * |a|
[PROOFSTEP]
convert mabs_mul_le (b / a) a
[GOAL]
case h.e'_3.h.e'_3
α : Type u
β : Type v
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ b = b / a * a
[PROOFSTEP]
rw [div_mul_cancel']
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊓ y = ⅟2 • (x + y - |y - x|)
[PROOFSTEP]
rw [← LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub x y, two_smul, ← two_smul α, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : Semiring α
inst✝⁴ : Invertible 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)
[PROOFSTEP]
rw [← LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul α, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)
[PROOFSTEP]
letI := invertibleOfNonzero (two_ne_zero' α)
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
this : Invertible 2 := invertibleOfNonzero (_ : 2 ≠ 0)
⊢ x ⊓ y = 2⁻¹ • (x + y - |y - x|)
[PROOFSTEP]
exact inf_eq_half_smul_add_sub_abs_sub α x y
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)
[PROOFSTEP]
letI := invertibleOfNonzero (two_ne_zero' α)
[GOAL]
α : Type u
β : Type v
inst✝⁷ : Lattice α
inst✝⁶ : CommGroup α
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
x y : β
this : Invertible 2 := invertibleOfNonzero (_ : 2 ≠ 0)
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)
[PROOFSTEP]
exact sup_eq_half_smul_add_add_abs_sub α x y
