β : Type ?u.146910
A : Type ?u.146913
G : Type ?u.146916
M : Type u_1
R : Type ?u.146922
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : M
h : a * b < c * d
⊢ min a b * min a b < max c d * max c d
β : Type ?u.146910
A : Type ?u.146913
G : Type ?u.146916
M : Type u_1
R : Type ?u.146922
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : M
h : a * b < c * d
⊢ min a b ^ 2 < max c d ^ 2
simp_rw [pow_two]
no goals
β : Type ?u.146910
A : Type ?u.146913
G : Type ?u.146916
M : Type u_1
R : Type ?u.146922
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : M
h : a * b < c * d
⊢ min a b * min a b < max c d * max c d
exact
  (mul_le_mul' inf_le_left inf_le_right).trans_lt
    (h.trans_le <| mul_le_mul' le_sup_left le_sup_right)