awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
h :
  ∀ (a : Option α),
    Eq.{u_2 + 1} (α := M)
      (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) a :
        M)
      ((f : (a : Option α) → M) a : M)
⊢ optionElim ((f : (a : Option α) → M) none) f.some = f

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
a : Option α
h :
  Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) none :
      M)
    ((f : (a : Option α) → M) none : M)
h₁ :
  ∀ (val : α),
    Eq.{u_2 + 1} (α := M)
      (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M)
          (Option.some val) :
        M)
      ((f : (a : Option α) → M) (Option.some val) : M)
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) a : M)
    ((f : (a : Option α) → M) a : M)

Tactic:
cases a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
h h₁ : Eq.{u_2 + 1} (α := M) ((f : (a : Option α) → M) none : M) ((f : (a : Option α) → M) none : M)
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M) none :
      M)
    ((f : (a : Option α) → M) none : M)

Tactic:
rw [optionElim_apply_none]

Premises used: Finsupp.optionElim_apply_none
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : Finsupp.{u_1, u_2} (Option α) M
val : α
⊢ Eq.{u_2 + 1} (α := M)
    (((optionElim ((f : (a : Option α) → M) none) f.some : Finsupp.{u_1, u_2} (Option α) M) : (a : Option α) → M)
        (Option.some val) :
      M)
    ((f : (a : Option α) → M) (Option.some val) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
h :
  ∀ (a : Option α),
    Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) a : M) ((single none y : (a : Option α) → M) a : M)
⊢ Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim y 0) (single none y)

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
a : Option α
h :
  Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) none : M) ((single none y : (a : Option α) → M) none : M)
h₁ :
  ∀ (val : α),
    Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) (Option.some val) : M)
      ((single none y : (a : Option α) → M) (Option.some val) : M)
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) a : M) ((single none y : (a : Option α) → M) a : M)

Tactic:
cases a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) none : M) ((single none y : (a : Option α) → M) none : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
val : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y 0 : (a : Option α) → M) (Option.some val) : M)
    ((single none y : (a : Option α) → M) (Option.some val) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : y ≠ 0
contrapose : ∀ (c : optionElim y f = 0), y = 0
⊢ optionElim y f ≠ 0

Tactic:
contrapose h with c
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
rw rw₁ : Eq.{u_2 + 1} (α := M) ((0 : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)

Tactic:
rw [c]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)

Tactic:
have : f.optionElim y none = (0 : Option α →₀ M) none := by
    rw [c]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) none : M) ((0 : (a : Option α) → M) none : M)
⊢ y = 0

Tactic:
simp only [optionElim_apply_eq_elim, Option.elim_none, coe_zero, Pi.zero_apply] at this

Premises used: Option.elim_none, Pi.zero_apply, Finsupp.optionElim_apply_eq_elim, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : y = 0
⊢ y = 0

Tactic:
this
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
this : y = 0
⊢ y = 0

Tactic:
exact this
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0
contrapose : ∀ (c : optionElim y f = 0), f = 0
⊢ optionElim y f ≠ 0

Tactic:
contrapose h with c
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)
⊢ f = 0

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
rw rw₁ :
  Eq.{u_2 + 1} (α := M) ((0 : (a : Option α) → M) (Option.some a) : M) ((0 : (a : Option α) → M) (Option.some a) : M)
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some a) : M)
    ((0 : (a : Option α) → M) (Option.some a) : M)

Tactic:
rw [c]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
⊢ Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some a) : M)
    ((0 : (a : Option α) → M) (Option.some a) : M)

Tactic:
have : f.optionElim y (Option.some a) = (0 : Option α →₀ M) (Option.some a) := by
    rw [c]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this :
  Eq.{u_2 + 1} (α := M) ((optionElim y f : (a : Option α) → M) (Option.some a) : M)
    ((0 : (a : Option α) → M) (Option.some a) : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
simp only [optionElim_apply_eq_elim, Option.elim_some, coe_zero, Pi.zero_apply] at this

Premises used: Pi.zero_apply, Option.elim_some, Finsupp.optionElim_apply_eq_elim, Finsupp.coe_zero
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
this
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
c : optionElim y f = 0
a : α
this : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) ((0 : (a : α) → M) a : M)

Tactic:
exact this
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
mp : optionElim y f ≠ 0 → f ≠ 0 ∨ y ≠ 0
mpr : f ≠ 0 ∨ y ≠ 0 → optionElim y f ≠ 0
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0

Tactic:
constructor
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : optionElim y f ≠ 0
mp : ∀ (h : f = 0 ∧ y = 0), optionElim y f = 0
⊢ f ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f = 0 ∧ y = 0
mp : Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim 0 0) 0
⊢ optionElim y f = 0

Tactic:
rcases h with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
mp : Eq (α := Finsupp.{u_1, u_2} (Option α) M) (single none 0) 0
mp₁ mp₂ : Eq (α := Finsupp.{u_1, u_2} (Option α) M) 0 0
⊢ Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim 0 0) 0

Tactic:
rw [optionElim_zero, single_zero]

Premises used: Finsupp.optionElim_zero, Finsupp.single_zero
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
optionElim_ne_zero_of_right y f h

Premises used: Finsupp.optionElim_ne_zero_of_right
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
exact optionElim_ne_zero_of_right y f h

Premises used: Finsupp.optionElim_ne_zero_of_right
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
optionElim_ne_zero_of_left y f h

Premises used: Finsupp.optionElim_ne_zero_of_left
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : y ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
exact optionElim_ne_zero_of_left y f h

Premises used: Finsupp.optionElim_ne_zero_of_left
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0 ∨ y ≠ 0
mpr : ∀ (h : f ≠ 0), optionElim y f ≠ 0
mpr₁ : ∀ (h : y ≠ 0), optionElim y f ≠ 0
⊢ optionElim y f ≠ 0

Tactic:
cases h with
    | inl h => exact optionElim_ne_zero_of_right y f h
    | inr h => exact optionElim_ne_zero_of_left y f h
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
n : Finsupp.{u_1, u_2} (Option α) M
m : α →₀ M
i : M
⊢ n = (embDomain Embedding.some m).update none i ↔ (n : (a : Option α) → M) none = i ∧ n.some = m

Tactic:
(optionEquiv.apply_eq_iff_eq_symm_apply (y := (_, _))).symm.trans Prod.ext_iff

Premises used: Finsupp.update, Prod.ext_iff, Finsupp.optionEquiv, Iff.trans, Iff.symm, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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 : (a : Option α) → M) none) * prod.{u_1, u_2, u_3} (M := M) (some 0) fun (a : α) ↦ b (Option.some a)

Tactic:
simp [some_zero, h_zero]

Premises used: Finsupp.some_zero
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)
add :
  (b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)) *
      (b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)) =
    b none ((f₁ + f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (f₁.some.prod fun (a : α) ↦ b (Option.some a)) (f₂.some.prod fun (a : α) ↦ b (Option.some a))
add₁ : ∀ a ∈ f₁.some.support ∪ f₂.some.support, b (Option.some a) 0 = 1
add₂ :
  ∀ 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₂
add₃ : ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1
add₄ : ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) 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]

Premises used: Finsupp.prod_add_index, Finsupp.some_add
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)
add :
  (b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)) *
      (b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)) =
    b none ((f₁ : (a : Option α) → M) none) * b none ((f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (f₁.some.prod fun (a : α) ↦ b (Option.some a)) (f₂.some.prod fun (a : α) ↦ b (Option.some a))
⊢ (b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)) *
      (b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)) =
    b none ((f₁ + f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (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]

Premises used: Pi.add_apply, Finsupp.coe_add
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)
add add₁ :
  b none ((f₁ : (a : Option α) → M) none) * b none ((f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (f₁.some.prod fun (a : α) ↦ b (Option.some a)) (f₂.some.prod fun (a : α) ↦ b (Option.some a)) =
    b none ((f₁ : (a : Option α) → M) none) * b none ((f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (f₁.some.prod fun (a : α) ↦ b (Option.some a)) (f₂.some.prod fun (a : α) ↦ b (Option.some a))
⊢ (b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)) *
      (b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)) =
    b none ((f₁ : (a : Option α) → M) none) * b none ((f₂ : (a : Option α) → M) none) *
      HMul.hMul (α := N) (f₁.some.prod fun (a : α) ↦ b (Option.some a)) (f₂.some.prod fun (a : α) ↦ b (Option.some a))

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.some.support ∪ f₂.some.support, b (Option.some a) 0 = 1

Tactic:
simp [h_zero, h_add]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) 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₂

Tactic:
simp [h_zero, h_add]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)
⊢ ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1

Tactic:
simp [h_zero, h_add]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂ : Finsupp.{u_1, u_2} (Option α) M
h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a)
h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) 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]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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 α
m : M
single :
  prod (Finsupp.single none m) b =
    b none ((Finsupp.single none m : (a : Option α) → M) none) *
      prod (some (Finsupp.single none m)) fun (a : α) ↦ b (Option.some a)
single₁ :
  ∀ (val : α),
    prod (Finsupp.single (Option.some val) m) b =
      b none ((Finsupp.single (Option.some val) m : (a : Option α) → M) none) *
        prod (some (Finsupp.single (Option.some val) m)) fun (a : α) ↦ b (Option.some a)
⊢ prod (Finsupp.single a m) b =
    b none ((Finsupp.single a m : (a : Option α) → M) none) *
      prod (some (Finsupp.single a m)) fun (a : α) ↦ b (Option.some a)

Tactic:
cases a
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂
m : M
⊢ prod (single none m) b =
    b none ((single none m : (a : Option α) → M) none) * prod (some (single none m)) fun (a : α) ↦ b (Option.some a)

Tactic:
simp [h_zero]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
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₂
m : M
val : α
⊢ prod (single (Option.some val) m) b =
    b none ((single (Option.some val) m : (a : Option α) → M) none) *
      prod (some (single (Option.some val) m)) fun (a : α) ↦ b (Option.some a)

Tactic:
simp [h_zero]
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
f : Finsupp.{u_1, u_2} (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₂
zero :
  prod 0 b =
    b none ((0 : (a : Option α) → M) none) * prod.{u_1, u_2, u_3} (M := M) (some 0) fun (a : α) ↦ b (Option.some a)
add :
  ∀ (f₁ f₂ : Finsupp.{u_1, u_2} (Option α) M)
    (h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a))
    (h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)),
    (f₁ + f₂).prod b =
      b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
single :
  ∀ (a : Option α) (m : M),
    prod (Finsupp.single a m) b =
      b none ((Finsupp.single a m : (a : Option α) → M) none) *
        prod (some (Finsupp.single a m)) fun (a : α) ↦ b (Option.some a)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)

Tactic:
induction f using induction_linear with
    | zero => simp [some_zero, h_zero]
    | add f₁ f₂ h₁ h₂ =>
      rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
      · simp only [h_add, Pi.add_apply, Finsupp.coe_add]
        rw [mul_mul_mul_comm]
      all_goals simp [h_zero, h_add]
    | single a m => cases a <;> simp [h_zero]

Premises used: Finsupp.prod_add_index, mul_mul_mul_comm, Finsupp.some_zero, Finsupp.some_add, Pi.add_apply, Finsupp.coe_add, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : CommMonoid N
f : Finsupp.{u_1, u_2} (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₂
zero :
  prod 0 b =
    b none ((0 : (a : Option α) → M) none) * prod.{u_1, u_2, u_3} (M := M) (some 0) fun (a : α) ↦ b (Option.some a)
add :
  ∀ (f₁ f₂ : Finsupp.{u_1, u_2} (Option α) M)
    (h₁ : f₁.prod b = b none ((f₁ : (a : Option α) → M) none) * f₁.some.prod fun (a : α) ↦ b (Option.some a))
    (h₂ : f₂.prod b = b none ((f₂ : (a : Option α) → M) none) * f₂.some.prod fun (a : α) ↦ b (Option.some a)),
    (f₁ + f₂).prod b =
      b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
single :
  ∀ (a : Option α) (m : M),
    prod (Finsupp.single a m) b =
      b none ((Finsupp.single a m : (a : Option α) → M) none) *
        prod (some (Finsupp.single a m)) fun (a : α) ↦ b (Option.some a)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)

Tactic:
classical
    induction f using induction_linear with
    | zero => simp [some_zero, h_zero]
    | add f₁ f₂ h₁ h₂ =>
      rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
      · simp only [h_add, Pi.add_apply, Finsupp.coe_add]
        rw [mul_mul_mul_comm]
      all_goals simp [h_zero, h_add]
    | single a m => cases a <;> simp [h_zero]

Premises used: Finsupp.prod_add_index, mul_mul_mul_comm, Finsupp.some_zero, Finsupp.some_add, Pi.add_apply, Finsupp.coe_add, Finsupp.single
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
R : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Finsupp.{u_1, u_4} (Option α) R
b : Option α → M
⊢ (f.sum fun (o : Option α) (r : R) ↦ r • b o) =
    HSMul.hSMul.{u_4, u_2, u_2} (α := R) ((f : (a : Option α) → R) none : R) (b none) +
      f.some.sum fun (a : α) (r : R) ↦ r • b (Option.some a)

Tactic:
f.sum_option_index _ (fun _ => zero_smul _ _) fun _ _ _ => add_smul _ _ _

Premises used: zero_smul, add_smul, Finsupp.sum_option_index
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
h :
  ∀ (x : Option α),
    Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) x : M)
      ((optionElim i a + optionElim j b : (a : Option α) → M) x : M)
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b

Tactic:
ext x
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
x : Option α
h :
  Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) none : M)
    ((optionElim i a + optionElim j b : (a : Option α) → M) none : M)
h₁ :
  ∀ (val : α),
    Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) (Option.some val) : M)
      ((optionElim i a + optionElim j b : (a : Option α) → M) (Option.some val) : M)
⊢ Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) x : M)
    ((optionElim i a + optionElim j b : (a : Option α) → M) x : M)

Tactic:
cases x
-- Module: Mathlib.Data.Finsupp.Option
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
⊢ Eq.{u_2 + 1} (α := M) ((optionElim (i + j) (a + b) : (a : Option α) → M) none : M)
    ((optionElim i a + optionElim j b : (a : Option α) → M) none : M)

Tactic:
simp