case nil
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ prod []

case cons
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ prod (hd :: tl)
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ 1 ≤ prod l
induction' l with hd tl ih
case cons
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * prod tl
case cons
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ prod (hd :: tl)
rw [prod_cons]
no goals
case cons
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → 1 ≤ prod tl
hl₁ : ∀ (x : M), x ∈ hd :: tl → 1 ≤ x
⊢ 1 ≤ hd * prod tl
exact one_le_mul (hl₁ hd (mem_cons_self hd tl)) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))
no goals
case nil
ι : Type ?u.105808
α : Type ?u.105811
M : Type u_1
N : Type ?u.105817
P : Type ?u.105820
M₀ : Type ?u.105823
G : Type ?u.105826
R : Type ?u.105829
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝¹ : Preorder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List M
hl₁✝ : ∀ (x : M), x ∈ l → 1 ≤ x
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ 1 ≤ prod []
rfl