awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
pos :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b)
    (h_1 : ∃ (a : α), (f : (a : α) → β) a = b),
    Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
      ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
neg :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b),
    (¬∃ (a : α), (f : (a : α) → β) a = b) →
      Eq.{u_4 + 1} (α := M)
        ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)
have pos₁ : (¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b) →
  ∀ (h : ∃ (a : α), (f : (a : α) → β) a = b),
    Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
b : β
pos :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b)
    (h_1 : ∃ (a : α), (f : (a : α) → β) a = b),
    Eq.{u_4 + 1} (α := M) ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M)
      ((v : (a : α) → M) (h_1.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
neg :
  ∀ (h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b),
    (¬∃ (a : α), (f : (a : α) → β) a = b) →
      Eq.{u_4 + 1} (α := M)
        ((v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯) : M) (0 : M)
pos₁ :
  (¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b) →
    ∀ (h : ∃ (a : α), (f : (a : α) → β) a = b),
      Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b)) : M)
⊢ Eq.{u_4 + 1} (α := M)
    (if h : ∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b then
      (v : (a : α) → M) (Finset.choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = b) v.support ⋯)
    else 0)
    (if h : ∃ (a : α), (f : (a : α) → β) a = b then
      (v : (a : α) → M) (h.choose (p := fun (a : α) ↦ (f : (a : α) → β) a = b))
    else 0)
have neg₁ : (¬∃ (a : α), Ne.{u_4 + 1} (α := M) ((v : (a : α) → M) a : M) (0 : M) ∧ (f : (a : α) → β) a = b) →
  (¬∃ (a : α), (f : (a : α) → β) a = b) → Eq.{u_4 + 1} (α := M) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have simp_rw : Eq.{u_4 + 1} (α := M)
  (if h : a ∈ v.support then
      (v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support sorry)
    else 0 :
    M)
  ((v : (a : α) → M) a : M)
Tactic: simp_rw [embDomain, coe_mk, mem_map']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
have pos : ∀ (h : a ∈ v.support),
  Eq.{u_4 + 1} (α := M)
    ((v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
          sorry) :
      M)
    ((v : (a : α) → M) a : M)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
pos :
  ∀ (h : a ∈ v.support),
    Eq.{u_4 + 1} (α := M)
      ((v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯) :
        M)
      ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
have neg : ∀ (h : a ∉ v.support), Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∈ v.support
⊢ Eq.{u_4 + 1} (α := M)
    ((v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
          ⋯) :
      M)
    ((v : (a : α) → M) a : M)
have pos : f.toFun
    (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support sorry) =
  f.toFun a
Tactic: refine congr_arg (v : α → M) (f.inj' ?_)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have simp_rw : Eq.{u_4 + 1} (α := M)
  (({ support := map f v.support,
          toFun := fun (a₂ : β) ↦
            if h : a₂ ∈ map f v.support then
              (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support sorry)
            else 0,
          mem_support_toFun := sorry } :
        (a : β) → M)
      ((f : (a : α) → β) a : β) :
    M)
  ((v : (a : α) → M) a : M)
Tactic: classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (({ support := map f v.support,
            toFun := fun (a₂ : β) ↦
              if h : a₂ ∈ map f v.support then
                (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
              else 0,
            mem_support_toFun := ⋯ } :
          (a : β) → M)
        ((f : (a : α) → β) a : β) :
      M)
    ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have simp_rw₁ : Eq.{u_4 + 1} (α := M)
  (if h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β) then
      (v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support sorry)
    else 0 :
    M)
  ((v : (a : α) → M) a : M)
Tactic: classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (({ support := map f v.support,
            toFun := fun (a₂ : β) ↦
              if h : a₂ ∈ map f v.support then
                (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
              else 0,
            mem_support_toFun := ⋯ } :
          (a : β) → M)
        ((f : (a : α) → β) a : β) :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M)
    (if h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β) then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have simp_rw₂ : Eq.{u_4 + 1} (α := M)
  (if h : a ∈ v.support then
      (v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support sorry)
    else 0 :
    M)
  ((v : (a : α) → M) a : M)
Tactic: classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (({ support := map f v.support,
            toFun := fun (a₂ : β) ↦
              if h : a₂ ∈ map f v.support then
                (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
              else 0,
            mem_support_toFun := ⋯ } :
          (a : β) → M)
        ((f : (a : α) → β) a : β) :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M)
    (if h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β) then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have pos : ∀ (h : a ∈ v.support),
  Eq.{u_4 + 1} (α := M)
    ((v : (a : α) → M)
        (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
          sorry) :
      M)
    ((v : (a : α) → M) a : M)
Tactic: classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_4
inst : Zero M
f : α ↪ β
v : α →₀ M
a : α
simp_rw :
  Eq.{u_4 + 1} (α := M)
    (({ support := map f v.support,
            toFun := fun (a₂ : β) ↦
              if h : a₂ ∈ map f v.support then
                (v : (a : α) → M) (choose (fun (a₁ : α) ↦ (f : (a : α) → β) a₁ = a₂) v.support ⋯)
              else 0,
            mem_support_toFun := ⋯ } :
          (a : β) → M)
        ((f : (a : α) → β) a : β) :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₁ :
  Eq.{u_4 + 1} (α := M)
    (if h : Membership.mem (α := β) (map f v.support) ((f : (a : α) → β) a : β) then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M)
    (if h : a ∈ v.support then
        (v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯)
      else 0 :
      M)
    ((v : (a : α) → M) a : M)
pos :
  ∀ (h : a ∈ v.support),
    Eq.{u_4 + 1} (α := M)
      ((v : (a : α) → M)
          (choose (fun (a₁ : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a₁ : β) ((f : (a : α) → β) a : β)) v.support
            ⋯) :
        M)
      ((v : (a : α) → M) a : M)
⊢ Eq.{u_4 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
have neg : ∀ (h : a ∉ v.support), Eq.{u_4 + 1} (α := M) (0 : M) ((v : (a : α) → M) a : M)
Tactic: classical
    simp_rw [embDomain, coe_mk, mem_map']
    split_ifs with h
    · refine congr_arg (v : α → M) (f.inj' ?_)
      exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _
    · exact (notMem_support_iff.1 h).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Defs (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Zero M
⊢ Eq (α := (v : α →₀ M) → α →₀ M) (embDomain (Embedding.refl α)) id
have h : ∀ (x : α →₀ M) (a : α),
  Eq.{u_4 + 1} (α := M) ((embDomain (Embedding.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Ext (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : AddZeroClass N
f g : (α →₀ M) →+ N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N) ((f : (a : α →₀ M) → N) (single x y) : N) ((g : (a : α →₀ M) → N) (single x y) : N)
⊢ f = g
have refine : Set.EqOn (α := α →₀ M) (β := N) (⇑f : (a : α →₀ M) → N) (⇑g : (a : α →₀ M) → N)
  {f : α →₀ M | ∃ (a : α) (b : M), f = single a b}
Tactic: refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Ext (hypothesis)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
⊢ f = g
have this : Eq (α := (α →₀ M) →+ Additive N)
  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f : (α →₀ M) →+ Additive N)
  ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g : (α →₀ M) →+ Additive N)
Tactic: have := addHom_ext (f := f.toAdditiveRight) (g := g.toAdditiveRight) H
-- Lean 4 proof step from Mathlib.Data.Finsupp.Ext (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
this :
  Eq (α := (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
      (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
      (α →₀ M) →+ Additive N)
⊢ f = g
have h : ∀ (x : α) (x_1 : M),
  Eq.{u_3 + 1} (α := N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Ext (goal)
Goal:
α : Type u_1
M : Type u_2
N : Type u_3
inst : AddZeroClass M
inst_1 : MulOneClass N
f g : Multiplicative (α →₀ M) →* N
H :
  ∀ (x : α) (y : M),
    Eq.{u_3 + 1} (α := N)
      ((f : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
      ((g : (a : Multiplicative (α →₀ M)) → N)
          ((Multiplicative.ofAdd : (a : α →₀ M) → Multiplicative (α →₀ M)) (single x y) : Multiplicative (α →₀ M)) :
        N)
this :
  Eq (α := (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
      (α →₀ M) →+ Additive N)
    ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
      (α →₀ M) →+ Additive N)
x : α
x_1 : M
⊢ Eq.{u_3 + 1} (α := N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_1 :
          Additive N) :
      N)
have h : ∀
  (this :
    ∀ (x : α →₀ M),
      Eq.{u_3 + 1} (α := Additive N)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f :
                (α →₀ M) →+ Additive N) :
              (a : α →₀ M) → Additive N)
            x :
          Additive N)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g :
                (α →₀ M) →+ Additive N) :
              (a : α →₀ M) → Additive N)
            x :
          Additive N))
  (x : α) (x_2 : M),
  Eq.{u_3 + 1} (α := N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) f)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_2 :
          Additive N) :
      N)
    ((Additive.toMul : (a : Additive N) → N)
        ((AddMonoidHom.comp
                ((MonoidHom.toAdditiveRight : (a : Multiplicative (α →₀ M) →* N) → (α →₀ M) →+ Additive N) g)
                (singleAddHom x) :
              (a : M) → Additive N)
            x_2 :
          Additive N) :
      N)
Tactic: rw [DFunLike.ext_iff] at this
Cleared hypotheses: this, x, x_1
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
i : Fin n
M : Type u_1
inst : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update i.succ y).tail = t.tail.update i y
have h : ∀ (a : Fin n),
  Eq (α := M) (((t.update i.succ y).tail : (a : Fin n) → M) a : M) ((t.tail.update i y : (a : Fin n) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
⊢ cons ((t : (a : Fin (n + 1)) → M) 0) t.tail = t
have h : ∀ (a : Fin (n + 1)),
  Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have pos : ∀ (c_a : a = 0),
  Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
Tactic: by_cases c_a : a = 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
pos :
  ∀ (c_a : a = 0),
    Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
      ((t : (a : Fin (n + 1)) → M) a)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have neg : ∀ (c_a : ¬a = 0),
  Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
Tactic: by_cases c_a : a = 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have pos : Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) 0 : M)
  ((t : (a : Fin (n + 1)) → M) 0 : M)
Tactic: rw [c_a, cons_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : a = 0
pos :
  Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) 0 : M)
    ((t : (a : Fin (n + 1)) → M) 0 : M)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have pos₁ : Eq (α := M) ((t : (a : Fin (n + 1)) → M) 0 : M) ((t : (a : Fin (n + 1)) → M) 0 : M)
Tactic: rw [c_a, cons_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have neg : Eq (α := M)
  (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
  ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
Tactic: rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
neg :
  Eq (α := M)
    (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
    ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have neg₁ : Eq (α := M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M) ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
Tactic: rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
c_a : ¬a = 0
neg :
  Eq (α := M)
    (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
    ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
neg₁ : Eq (α := M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M) ((t : (a : Fin (n + 1)) → M) (a.pred c_a).succ : M)
⊢ Eq (α := M) (((cons ((t : (a : Fin (n + 1)) → M) 0) t.tail : Fin (n + 1) →₀ M) : (a : Fin (n + 1)) → M) a : M)
    ((t : (a : Fin (n + 1)) → M) a)
have neg₂ : Eq (α := M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M) ((t.tail : (a : Fin n) → M) (a.pred c_a) : M)
Tactic: rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Fin (goal)
Goal:
n : ℕ
M : Type u_1
inst : Zero M
y : M
⊢ Eq (α := Fin (n + 1) →₀ M) (cons y 0) (single 0 y)
have h : ∀ (j : Fin (n + 1)), Eq (α := M) ((cons y 0 : (a : Fin (n + 1)) → M) j : M) ((single 0 y : (a : Fin (n + 1)) → M) j)
Tactic: ext j