case slnil
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []

case cons
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)

case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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 : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ prod l₁ ≤ prod l₂
induction h
case cons
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)

case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
case slnil
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []

case cons
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)

case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
case slnil => rfl
case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
case cons
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod l₁✝ ≤ prod (a✝¹ :: l₂✝)

case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
case cons l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁⊢
  exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
no goals
case cons₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂ l₁✝ l₂✝ : List M
a✝¹ : M
a✝ : l₁✝ <+ l₂✝
a_ih✝ : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → prod l₁✝ ≤ prod l₂✝
h₁ : ∀ (a : M), a ∈ a✝¹ :: l₂✝ → 1 ≤ a
⊢ prod (a✝¹ :: l₁✝) ≤ prod (a✝¹ :: l₂✝)
case cons₂ l₁ l₂ a _ ih' =>
  simp only [prod_cons, forall_mem_cons] at h₁⊢
  exact mul_le_mul_left' (ih' h₁.2) _
no goals
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ prod [] ≤ prod []
rfl
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ prod l₁ ≤ a * prod l₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod l₁ ≤ prod (a :: l₂)
simp only [prod_cons, forall_mem_cons] at h₁⊢
no goals
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ prod l₁ ≤ a * prod l₂
exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ a * prod l₁ ≤ a * prod l₂
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂ → 1 ≤ a_1
⊢ prod (a :: l₁) ≤ prod (a :: l₂)
simp only [prod_cons, forall_mem_cons] at h₁⊢
no goals
ι : Type ?u.76473
α : Type ?u.76476
M : Type u_1
N : Type ?u.76482
P : Type ?u.76485
M₀ : Type ?u.76488
G : Type ?u.76491
R : Type ?u.76494
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₂✝ l₁ l₂ : List M
a : M
a✝ : l₁ <+ l₂
ih' : (∀ (a : M), a ∈ l₂ → 1 ≤ a) → prod l₁ ≤ prod l₂
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂ → 1 ≤ x
⊢ a * prod l₁ ≤ a * prod l₂
exact mul_le_mul_left' (ih' h₁.2) _