case mp
α : Type u
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⁻

case mpr
α : Type u
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
α : Type u
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⁻
constructor <;> intro h
case mp.left
α : Type u
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⁺

case mp.right
α : Type u
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⁻
case mp
α : Type u
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⁻
constructor
no goals
case mp.left
α : Type u
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⁺
exact sup_le (h.trans (m_le_pos b)) (one_le_pos b)
case mp.right
α : Type u
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⁻
case mp.right
α : Type u
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⁻
rw [← inv_le_inv_iff] at h
no goals
case mp.right
α : Type u
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⁻
exact sup_le (h.trans (inv_le_neg a)) (one_le_neg a)
case mpr
α : Type u
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⁻
case mpr
α : Type u
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
rw [← pos_div_neg a, ← pos_div_neg b]
no goals
case mpr
α : Type u
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⁻
exact div_le_div'' h.1 h.2