case nil
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l : List R
h✝ : ∀ (a : R), a ∈ l → 0 < a
h : ∀ (a : R), a ∈ [] → 0 < a
⊢ 0 < prod []

case cons
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < prod (a :: l)
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l : List R
h : ∀ (a : R), a ∈ l → 0 < a
⊢ 0 < prod l
induction' l with a l ih
no goals
case nil
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l : List R
h✝ : ∀ (a : R), a ∈ l → 0 < a
h : ∀ (a : R), a ∈ [] → 0 < a
⊢ 0 < prod []
simp
case cons
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < a * prod l
case cons
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < prod (a :: l)
rw [prod_cons]
no goals
case cons
ι : Type ?u.157247
α : Type ?u.157250
M : Type ?u.157253
N : Type ?u.157256
P : Type ?u.157259
M₀ : Type ?u.157262
G : Type ?u.157265
R : Type u_1
inst✝ : StrictOrderedSemiring R
l✝ : List R
h✝ : ∀ (a : R), a ∈ l✝ → 0 < a
a : R
l : List R
ih : (∀ (a : R), a ∈ l → 0 < a) → 0 < prod l
h : ∀ (a_1 : R), a_1 ∈ a :: l → 0 < a_1
⊢ 0 < a * prod l
exact mul_pos (h _ <| mem_cons_self _ _) (ih fun a ha => h a <| mem_cons_of_mem _ ha)