-- 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.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₂

Tactic:
all_goals simp [h_zero, h_add]

Result:
no goals

Proof state:
α : 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.prod b = b none (f none) * f.some.prod fun a => b (Option.some a)

Tactic:
apply induction_linear f

Result:
case h0
α : 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₂
⊢ prod 0 b = b none (0 none) * (some 0).prod fun a => b (Option.some a)

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 g : Option α →₀ M),
    (f.prod b = b none (f none) * f.some.prod fun a => b (Option.some a)) →
      (g.prod b = b none (g none) * g.some.prod fun a => b (Option.some a)) →
        (f + g).prod b = b none ((f + g) none) * (f + g).some.prod fun a => b (Option.some a)

case hsingle
α : 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₂
⊢ ∀ (a : Option α) (b_1 : M),
    (single a b_1).prod b = b none ((single a b_1) none) * (single a b_1).some.prod fun a => b (Option.some a)

Proof state:
case h0
α : 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₂
⊢ prod 0 b = b none (0 none) * (some 0).prod fun a => b (Option.some a)

Tactic:
simp [some_zero, h_zero]

Result:
no goals

Proof state:
case hsingle
α : 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₂
⊢ ∀ (a : Option α) (b_1 : M),
    (single a b_1).prod b = b none ((single a b_1) none) * (single a b_1).some.prod fun a => b (Option.some a)

Tactic:
rintro (_ | a) m <;> simp [h_zero, h_add]

Result:
no goals

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 g : Option α →₀ M),
    (f.prod b = b none (f none) * f.some.prod fun a => b (Option.some a)) →
      (g.prod b = b none (g none) * g.some.prod fun a => b (Option.some a)) →
        (f + g).prod b = b none ((f + g) none) * (f + g).some.prod fun a => b (Option.some a)

Tactic:
intro f₁ f₂ h₁ h₂

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)
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂) none) * (f₁ + f₂).some.prod fun a => b (Option.some a)