Theorem: OnCycleFactors.Multiset.prod_pos (Jordan/ConjClassCount.lean)

State before:
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
h : ∀ a ∈ m, 0 < a
⊢ 0 < Multiset.prod m
Tactic:
induction' m using Multiset.induction with a m ih
State after:
case empty
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
h : ∀ a ∈ 0, 0 < a
⊢ 0 < Multiset.prod 0

case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < Multiset.prod (a ::ₘ m)

State before:
case empty
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
h : ∀ a ∈ 0, 0 < a
⊢ 0 < Multiset.prod 0
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < Multiset.prod (a ::ₘ m)
Tactic:
rw [Multiset.prod_cons]
State after:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < a * Multiset.prod m

State before:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < a * Multiset.prod m
Tactic:
exact
  mul_pos (h _ <| Multiset.mem_cons_self _ _)
    (ih fun a ha => h a <| Multiset.mem_cons_of_mem ha)
State after:
no goals