-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_option_index [AddCommMonoid M] [CommMonoid N] (f : Option α →₀ M)
    (b : Option α → M → N) (h_zero : ∀ o, b o 0 = 1)
    (h_add : ∀ o m₁ m₂, b o (m₁ + m₂) = b o m₁ * b o m₂) :
    f.prod b = b none (f none) * f.some.prod fun a => b (Option.some a)

Proof state:
case hadd
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)) *
      (b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)) =
    b none ((f₁ + f₂) none) * ((f₁.some.prod fun a => b (Option.some a)) * f₂.some.prod fun a => b (Option.some a))

Tactic:
simp only [h_add, Pi.add_apply, Finsupp.coe_add]

Result:
case hadd
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)) *
      (b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)) =
    b none (f₁ none) * b none (f₂ none) *
      ((f₁.some.prod fun a => b (Option.some a)) * f₂.some.prod fun a => b (Option.some a))

Proof state:
case hadd
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a => b (Option.some a)

Tactic:
rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]

Result:
case hadd
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)) *
      (b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)) =
    b none ((f₁ + f₂) none) * ((f₁.some.prod fun a => b (Option.some a)) * f₂.some.prod fun a => b (Option.some a))

case hadd.h_zero
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ ∀ a ∈ f₁.some.support ∪ f₂.some.support, b (Option.some a) 0 = 1

case hadd.h_add
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ ∀ a ∈ f₁.some.support ∪ f₂.some.support,
    ∀ (b₁ b₂ : M), b (Option.some a) (b₁ + b₂) = b (Option.some a) b₁ * b (Option.some a) b₂

case hadd.h_zero
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

case hadd.h_add
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂

Proof state:
case hadd
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ (b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)) *
      (b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)) =
    b none (f₁ none) * b none (f₂ none) *
      ((f₁.some.prod fun a => b (Option.some a)) * f₂.some.prod fun a => b (Option.some a))

Tactic:
rw [mul_mul_mul_comm]

Result:
no goals

Proof state:
case hadd.h_add
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : Option α →₀ M
b : Option α → M → N
h_zero : ∀ (o : Option α), b o 0 = 1
h_add : ∀ (o : Option α) (m₁ m₂ : M), b o (m₁ + m₂) = b o m₁ * b o m₂
f₁ f₂ : Option α →₀ M
h₁ : f₁.prod b = b none (f₁ none) * f₁.some.prod fun a => b (Option.some a)
h₂ : f₂.prod b = b none (f₂ none) * f₂.some.prod fun a => b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂

Tactic:
simp [h_zero, h_add]

Result:
no goals