case nil
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ prod []

case cons
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ prod (head✝ :: tail✝)
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
l : List M
hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x
⊢ ∀ (x : M), x ∈ l → x ≤ prod l
induction l
case cons
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝ ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
case cons
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ prod (head✝ :: tail✝)
simp_rw [prod_cons, forall_mem_cons] at hl₁⊢
case cons.left
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝

case cons.right
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
case cons
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝ ∧ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
constructor
case cons.right
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
case cons.left
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝

case cons.right
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
no goals
case cons.right
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ tail✝ → x ≤ head✝ * prod tail✝
case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)
no goals
case nil
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
hl₁ : ∀ (x : M), x ∈ [] → 1 ≤ x
⊢ ∀ (x : M), x ∈ [] → x ≤ prod []
simp
no goals
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ prod tail✝
hl₁ : 1 ≤ head✝ ∧ ∀ (x : M), x ∈ tail✝ → 1 ≤ x
⊢ head✝ ≤ head✝ * prod tail✝
exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
no goals
ι : Type ?u.137425
α : Type ?u.137428
M : Type u_1
N : Type ?u.137434
P : Type ?u.137437
M₀ : Type ?u.137440
G : Type ?u.137443
R : Type ?u.137446
inst✝ : OrderedCommMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ prod tl
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * prod tl
exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)