case nil
ι : Type ?u.73927
α : Type ?u.73930
M : Type u_1
N : Type ?u.73936
P : Type ?u.73939
M₀ : Type ?u.73942
G : Type ?u.73945
R : Type ?u.73948
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
⊢ prod [] ≤ prod []

case cons
ι : Type ?u.73927
α : Type ?u.73930
M : Type u_1
N : Type ?u.73936
P : Type ?u.73939
M₀ : Type ?u.73942
G : Type ?u.73945
R : Type ?u.73948
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a✝ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
a b : M
la lb : List M
hab : a ≤ b
ih : Forall₂ (fun x x_1 => x ≤ x_1) la lb
ih' : prod la ≤ prod lb
⊢ prod (a :: la) ≤ prod (b :: lb)
ι : Type ?u.73927
α : Type ?u.73930
M : Type u_1
N : Type ?u.73936
P : Type ?u.73939
M₀ : Type ?u.73942
G : Type ?u.73945
R : Type ?u.73948
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
h : Forall₂ (fun x x_1 => x ≤ x_1) l₁ l₂
⊢ prod l₁ ≤ prod l₂
induction' h with a b la lb hab ih ih'
no goals
case nil
ι : Type ?u.73927
α : Type ?u.73930
M : Type u_1
N : Type ?u.73936
P : Type ?u.73939
M₀ : Type ?u.73942
G : Type ?u.73945
R : Type ?u.73948
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
⊢ prod [] ≤ prod []
rfl
no goals
case cons
ι : Type ?u.73927
α : Type ?u.73930
M : Type u_1
N : Type ?u.73936
P : Type ?u.73939
M₀ : Type ?u.73942
G : Type ?u.73945
R : Type ?u.73948
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l l₁✝ l₂✝ : List M
a✝ : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l₁ l₂ : List M
a b : M
la lb : List M
hab : a ≤ b
ih : Forall₂ (fun x x_1 => x ≤ x_1) la lb
ih' : prod la ≤ prod lb
⊢ prod (a :: la) ≤ prod (b :: lb)
simpa only [prod_cons] using mul_le_mul' hab ih'