R : Type ?u.554754
s : Multiset ℕ
⊢ Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)
R : Type ?u.554754
s : Multiset ℕ
h0 : Multiset.prod s ≠ 0
⊢ ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)
revert h0
case refine_1
R : Type ?u.554754
s : Multiset ℕ
⊢ Multiset.prod 0 ≠ 0 → ↑Ω (Multiset.prod 0) = Multiset.sum (Multiset.map (↑Ω) 0)

case refine_2
R : Type ?u.554754
s : Multiset ℕ
⊢ ∀ ⦃a : ℕ⦄ {s : Multiset ℕ},
    (Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)) →
      Multiset.prod (a ::ₘ s) ≠ 0 → ↑Ω (Multiset.prod (a ::ₘ s)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ s))
R : Type ?u.554754
s : Multiset ℕ
⊢ Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)
refine s.induction_on ?_ ?_
case refine_2
R : Type ?u.554754
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : Multiset.prod (a ::ₘ t) ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
case refine_2
R : Type ?u.554754
s : Multiset ℕ
⊢ ∀ ⦃a : ℕ⦄ {s : Multiset ℕ},
    (Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)) →
      Multiset.prod (a ::ₘ s) ≠ 0 → ↑Ω (Multiset.prod (a ::ₘ s)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ s))
intro a t h h0
case refine_2
R : Type ?u.554754
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : a ≠ 0 ∧ Multiset.prod t ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
case refine_2
R : Type ?u.554754
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : Multiset.prod (a ::ₘ t) ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
rw [Multiset.prod_cons, mul_ne_zero_iff] at h0
no goals
case refine_2
R : Type ?u.554754
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : a ≠ 0 ∧ Multiset.prod t ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
simp [h0, cardFactors_mul, h]
no goals
case refine_1
R : Type ?u.554754
s : Multiset ℕ
⊢ Multiset.prod 0 ≠ 0 → ↑Ω (Multiset.prod 0) = Multiset.sum (Multiset.map (↑Ω) 0)
simp