case refine'_1
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) 0) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal 0))

case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s)) →
      prod (map (fun a => f a + g a) (a ::ₘ s)) =
        sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
refine' s.induction_on _ _
no goals
case refine'_1
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ prod (map (fun a => f a + g a) 0) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal 0))
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ prod (map (fun a => f a + g a) (a ::ₘ s)) =
    sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s : Multiset α
f g : α → β
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s)) →
      prod (map (fun a => f a + g a) (a ::ₘ s)) =
        sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
intro a s ih
case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (g a * prod (map g i.snd))) (antidiagonal s)) =
    sum (map (fun x => prod (map f x.fst) * (g a * prod (map g x.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s))
case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ prod (map (fun a => f a + g a) (a ::ₘ s)) =
    sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal (a ::ₘ s)))
simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
  mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod_map, id_eq, map_add, map_map,
  Function.comp_apply, mul_assoc, sum_add]
no goals
case refine'_2
α : Type u_2
β : Type u_1
inst✝ : CommSemiring β
s✝ : Multiset α
f g : α → β
a : α
s : Multiset α
ih : prod (map (fun a => f a + g a) s) = sum (map (fun p => prod (map f p.fst) * prod (map g p.snd)) (antidiagonal s))
⊢ sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (g a * prod (map g i.snd))) (antidiagonal s)) =
    sum (map (fun x => prod (map f x.fst) * (g a * prod (map g x.snd))) (antidiagonal s)) +
      sum (map (fun i => prod (map f i.fst) * (f a * prod (map g i.snd))) (antidiagonal s))
exact add_comm _ _