awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (hypothesis)
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 : (a : α) → M) a : M)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0
have mp : optionElim y f ≠ 0 → f ≠ 0 ∨ y ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
mp : optionElim y f ≠ 0 → f ≠ 0 ∨ y ≠ 0
⊢ optionElim y f ≠ 0 ↔ f ≠ 0 ∨ y ≠ 0
have mpr : f ≠ 0 ∨ y ≠ 0 → optionElim y f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : optionElim y f ≠ 0
⊢ f ≠ 0 ∨ y ≠ 0
have mp : ∀ (h : f = 0 ∧ y = 0), optionElim y f = 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f = 0 ∧ y = 0
⊢ optionElim y f = 0
have mp : Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim 0 0) 0
Tactic: rcases h with ⟨rfl, rfl⟩
Cleared hypotheses: y, f, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
⊢ Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim 0 0) 0
have mp : Eq (α := Finsupp.{u_1, u_2} (Option α) M) (single none 0) 0
Tactic: rw [optionElim_zero, single_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
mp : Eq (α := Finsupp.{u_1, u_2} (Option α) M) (single none 0) 0
⊢ Eq (α := Finsupp.{u_1, u_2} (Option α) M) (optionElim 0 0) 0
have mp₁ : Eq (α := Finsupp.{u_1, u_2} (Option α) M) 0 0
Tactic: rw [optionElim_zero, single_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
y : M
f : α →₀ M
h : f ≠ 0 ∨ y ≠ 0
⊢ optionElim y f ≠ 0
have mpr : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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
⊢ optionElim y f ≠ 0
have mpr₁ : ∀ (h : y ≠ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
have 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))
Tactic: rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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))
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
have add₁ : ∀ a ∈ f₁.some.support ∪ f₂.some.support, b (Option.some a) 0 = 1
Tactic: rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
have 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₂
Tactic: rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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₂
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
have add₃ : ∀ a ∈ f₁.support ∪ f₂.support, b a 0 = 1
Tactic: rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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
⊢ (f₁ + f₂).prod b = b none ((f₁ + f₂ : (a : Option α) → M) none) * (f₁ + f₂).some.prod fun (a : α) ↦ b (Option.some a)
have add₄ : ∀ a ∈ f₁.support ∪ f₂.support, ∀ (b₁ b₂ : M), b a (b₁ + b₂) = b a b₁ * b a b₂
Tactic: rw [Finsupp.prod_add_index, h₁, h₂, some_add, Finsupp.prod_add_index]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ (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))
have 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))
Tactic: simp only [h_add, Pi.add_apply, Finsupp.coe_add]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ (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))
have 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))
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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
⊢ prod (single a m) b =
    b none ((single a m : (a : Option α) → M) none) * prod (some (single a m)) fun (a : α) ↦ b (Option.some a)
have single : 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: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ 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)
have 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)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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₂
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have single : ∀ (a : Option α) (m : M),
  prod (single a m) b =
    b none ((single a m : (a : Option α) → M) none) * prod (some (single a m)) 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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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₂
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have 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)
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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ f.prod b = b none ((f : (a : Option α) → M) none) * f.some.prod fun (a : α) ↦ b (Option.some a)
have single : ∀ (a : Option α) (m : M),
  prod (single a m) b =
    b none ((single a m : (a : Option α) → M) none) * prod (some (single a m)) 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]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
⊢ optionElim (i + j) (a + b) = optionElim i a + optionElim j b
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
Goal:
α : Type u_1
M : Type u_2
inst : AddZeroClass M
a b : α →₀ M
i j : M
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)
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Option (goal)
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)
⊢ 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)
have 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)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h
have rw : LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
  (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
Tactic: rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
    sum_of_support_subset _ Finset.subset_union_right _ hh₀]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Order (goal)
Goal:
ι : Type u_1
α : Type u_3
β : Type u_4
inst : Zero α
inst_1 : Preorder α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : IsOrderedAddMonoid β
inst_5 : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ LE.le.{u_4} (α := β) (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₁ : (a : ι) → α) x))
    (∑ x ∈ f₁.support ∪ f₂.support, h x ((f₂ : (a : ι) → α) x))
have h₁ : ∀ (i : ι) (hi : i ∈ f₁.support ∪ f₂.support), h i ((f₁ : (a : ι) → α) i) ≤ h i ((f₂ : (a : ι) → α) i)
Tactic: gcongr with i hi