A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a = a0 ∧ b = b0
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
⊢ a = a0 ∧ b = b0
haveI := Mul.to_covariantClass_right A
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
⊢ a = a0 ∧ b = b0
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a = a0 ∧ b = b0
have ha' : ¬a0 * b0 < a * b → ¬a0 < a := mt fun h ↦ mul_lt_mul_of_lt_of_le h hb
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
hb' : ¬a0 * b0 < a * b → ¬b0 < b
⊢ a = a0 ∧ b = b0
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
⊢ a = a0 ∧ b = b0
have hb' : ¬a0 * b0 < a * b → ¬b0 < b := mt fun h ↦ mul_lt_mul_of_le_of_lt ha h
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : a * b ≤ a0 * b0 → a ≤ a0
hb' : a * b ≤ a0 * b0 → b ≤ b0
⊢ a = a0 ∧ b = b0
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
hb' : ¬a0 * b0 < a * b → ¬b0 < b
⊢ a = a0 ∧ b = b0
push_neg  at ha' hb'
no goals
A : Type u_1
inst✝⁴ : Mul A
inst✝³ : LinearOrder A
inst✝² : CovariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass A A (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : A
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass A A (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : a * b ≤ a0 * b0 → a ≤ a0
hb' : a * b ≤ a0 * b0 → b ≤ b0
⊢ a = a0 ∧ b = b0
exact ⟨ha.antisymm' (ha' ab), hb.antisymm' (hb' ab)⟩