awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
have h : (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
M : Type u_2
n : ℕ
inst : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
h : (x • vecCons y v) 0 = vecCons (x • y) (x • v) 0
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
have h₁ : ∀ (i : Fin n), (x • vecCons y v) i.succ = vecCons (x • y) (x • v) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)
have h : ∀ (i : Fin n.succ), (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
have h : (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
h : (vecCons x v + w) 0 = vecCons (x + vecHead w) (v + vecTail w) 0
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
have h₁ : ∀ (i : Fin n), (vecCons x v + w) i.succ = vecCons (x + vecHead w) (v + vecTail w) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)
have h : ∀ (i : Fin n.succ), (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
have h : (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
h : (v + vecCons y w) 0 = vecCons (vecHead v + y) (vecTail v + w) 0
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
have h₁ : ∀ (i : Fin n), (v + vecCons y w) i.succ = vecCons (vecHead v + y) (vecTail v + w) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)
have h : ∀ (i : Fin n.succ), (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
have h : (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
h : (vecCons x v - w) 0 = vecCons (x - vecHead w) (v - vecTail w) 0
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
have h₁ : ∀ (i : Fin n), (vecCons x v - w) i.succ = vecCons (x - vecHead w) (v - vecTail w) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
⊢ v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)
have h : ∀ (i : Fin n.succ), (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
have h : (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
h : (v - vecCons y w) 0 = vecCons (vecHead v - y) (vecTail v - w) 0
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
have h₁ : ∀ (i : Fin n), (v - vecCons y w) i.succ = vecCons (vecHead v - y) (vecTail v - w) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Zero α
⊢ Eq.{u_1 + 1} (α := Fin n.succ → α) (vecCons 0 0) 0
have h : ∀ (i : Fin n.succ), Eq.{u_1 + 1} (α := α) (vecCons 0 0 i) (0 i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
⊢ -vecCons x v = vecCons (-x) (-v)
have h : ∀ (i : Fin n.succ), (-vecCons x v) i = vecCons (-x) (-v) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
have h : (-vecCons x v) 0 = vecCons (-x) (-v) 0
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Fin.Tuple (goal)
Goal:
α : Type u_1
n : ℕ
inst : Neg α
x : α
v : Fin n → α
i : Fin n.succ
h : (-vecCons x v) 0 = vecCons (-x) (-v) 0
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
have h₁ : ∀ (i : Fin n), (-vecCons x v) i.succ = vecCons (-x) (-v) i.succ
Tactic: refine i.cases ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Zero M
⊢ Eq (α := ZeroHom (ι →₀ M) (ι →₀ M)) (zeroHom (ZeroHom.id M)) (ZeroHom.id (ι →₀ M))
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_3 + 1} (α := M) ((((zeroHom (ZeroHom.id M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((ZeroHom.id (ι →₀ M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst : Zero M
inst_1 : Zero N
inst_2 : Zero O
f : ZeroHom N O
f₂ : ZeroHom M N
⊢ Eq (α := ZeroHom (ι →₀ M) (ι →₀ O)) (zeroHom (f.comp f₂)) (ZeroHom.comp (zeroHom f) (zeroHom f₂))
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_5 + 1} (α := O) ((((zeroHom (f.comp f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((ZeroHom.comp (zeroHom f) (zeroHom f₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
⊢ a ∈ (g₁ + g₂).support
have inl : a ∈ g₁.support ∧ a ∉ g₂.support → a ∈ (g₁ + g₂).support
Tactic: cases (Finset.mem_union_of_disjoint h).mp ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
g₁ g₂ : ι →₀ M
inst_1 : DecidableEq ι
h : Disjoint g₁.support g₂.support
a : ι
ha : a ∈ g₁.support ∪ g₂.support
inl : a ∈ g₁.support ∧ a ∉ g₂.support → a ∈ (g₁ + g₂).support
⊢ a ∈ (g₁ + g₂).support
have inr : a ∈ g₂.support ∧ a ∉ g₁.support → a ∈ (g₁ + g₂).support
Tactic: cases (Finset.mem_union_of_disjoint h).mp ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
⊢ embDomain f (v + w) = embDomain f v + embDomain f w
have h : ∀ (b : F),
  Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
have pos : ∀ (h : Membership.mem (γ := Set F) (Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)) b),
  Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
Tactic: by_cases h : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
pos :
  ∀ (h : Membership.mem (γ := Set F) (Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)) b),
    Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
      ((embDomain f v + embDomain f w : (a : F) → M) b : M)
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
have neg : ∀ (h : b ∉ Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)),
  Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
Tactic: by_cases h : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
F : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
H : Type u_7
inst : AddZeroClass M
inst_1 : AddZeroClass N
f_1 : M → N
g₁ g₂ : ι →₀ M
f : ι ↪ F
v w : ι →₀ M
b : F
h : Membership.mem (γ := Set F) (Set.range.{u_2, u_1 + 1} (ι := ι) (⇑f : (a : ι) → F)) b
⊢ Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) b : M)
    ((embDomain f v + embDomain f w : (a : F) → M) b : M)
have pos : ∀ (a : ι),
  Eq.{u_3 + 1} (α := M) ((embDomain f (v + w) : (a : F) → M) ((f : (a : ι) → F) a : F) : M)
    ((embDomain f v + embDomain f w : (a : F) → M) ((f : (a : ι) → F) a : F) : M)
Tactic: rcases h with ⟨a, rfl⟩
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (single a b + f).support = cons a f.support ha
have H : support (single a b) = {a}
Tactic: have H := support_single a hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
⊢ (single a b + f).support = cons a f.support ha
have rw : Disjoint (support (single a b)) f.support
Tactic: rw [support_add_eq, H, cons_eq_insert, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
⊢ Disjoint (support (single a b)) f.support
have rwa : Disjoint {a} f.support
Tactic: rwa [H, disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (single a b + f).support = cons a f.support ha
have have : ∀ (H : support (single a b) = {a}), (single a b + f).support = cons a f.support ha
Tactic: classical
  have H := support_single a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
have have₁ have₂ : ∀ (H : support (single a b) = {a}), (single a b + f).support = cons a f.support ha
⊢ (single a b + f).support = cons a f.support ha
have have₃ : ∀ (H : support (single a b) = {a}), Disjoint (support (single a b)) f.support
Tactic: classical
  have H := support_single a hb
  rw [support_add_eq, H, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha
have H : support (single a b) = {a}
Tactic: have H := support_single a hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
⊢ (f + single a b).support = cons a f.support ha
have rw : Disjoint f.support (support (single a b))
Tactic: rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : support (single a b) = {a}
⊢ Disjoint f.support (support (single a b))
have rwa : Disjoint f.support {a}
Tactic: rwa [H, disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
⊢ (f + single a b).support = cons a f.support ha
have have : ∀ (H : support (single a b) = {a}), (f + single a b).support = cons a f.support ha
Tactic: classical
  have H := support_single a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
have have₁ have₂ : ∀ (H : support (single a b) = {a}), (f + single a b).support = cons a f.support ha
⊢ (f + single a b).support = cons a f.support ha
have have₃ : ∀ (H : support (single a b) = {a}), Disjoint f.support (support (single a b))
Tactic: classical
  have H := support_single a hb
  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
  rwa [H, disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support = {f₁, f₂}
have rw : Eq (α := Finset ι) ({f₁} ∪ {f₂}) {f₁, f₂}
Tactic: rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
H : f₁ ≠ f₂
hg₁ : g₁ ≠ 0
hg₂ : g₂ ≠ 0
rw : Eq (α := Finset ι) ({f₁} ∪ {f₂}) {f₁, f₂}
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support = {f₁, f₂}
have rw₁ : Disjoint (support (single f₁ g₁)) (support (single f₂ g₂))
Tactic: rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support ⊆ {f₁, f₂}
have refine_1 : support (single f₁ g₁) ⊆ {f₁, f₂}
Tactic: refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
refine_1 : support (single f₁ g₁) ⊆ {f₁, f₂}
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support ⊆ {f₁, f₂}
have refine_2 : support (single f₂ g₂) ⊆ {f₁, f₂}
Tactic: refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
M : Type u_8
inst : AddZeroClass M
d : M
⊢ Eq (α := Unit →₀ M) ((AddEquiv.symm AddEquiv.finsuppUnique : (a : M) → Unit →₀ M) d : Unit →₀ M)
    (single () d : Unit →₀ M)
have h : Eq (α := M)
  ((((AddEquiv.symm AddEquiv.finsuppUnique : (a : M) → Unit →₀ M) d : Unit →₀ M) : (a : Unit) → M) default : M)
  ((single () d : (a : Unit) → M) default : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute.{u_3} (S := M) ((f : (a : ι) → M) x : M) ((g : (a : ι) → M) x : M)
⊢ AddCommute f g
have h₁ : ∀ (x : ι), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute.{u_3} (S := M) ((f : (a : ι) → M) x : M) ((g : (a : ι) → M) x : M)
x : ι
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
have pos : ∀ (hf : x ∈ f.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
Tactic: by_cases hf : x ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute.{u_3} (S := M) ((f : (a : ι) → M) x : M) ((g : (a : ι) → M) x : M)
x : ι
pos : ∀ (hf : x ∈ f.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
have neg : ∀ (hf : x ∉ f.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
Tactic: by_cases hf : x ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute.{u_3} (S := M) ((f : (a : ι) → M) x : M) ((g : (a : ι) → M) x : M)
x : ι
hf : x ∈ f.support
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
have pos : ∀ (hg : x ∈ g.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
Tactic: by_cases hg : x ∈ g.support
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f g : ι →₀ M
h : ∀ x ∈ f.support ∩ g.support, AddCommute.{u_3} (S := M) ((f : (a : ι) → M) x : M) ((g : (a : ι) → M) x : M)
x : ι
hf : x ∈ f.support
pos : ∀ (hg : x ∈ g.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
have neg : ∀ (hg : x ∉ g.support), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
Tactic: by_cases hg : x ∈ g.support
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = single a b + erase a f
have h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
⊢ Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
have h : Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((single j b + erase j f : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne j a with (rfl | h)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
h : Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((single j b + erase j f : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
have h₁ : ∀ (h : j ≠ a), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne j a with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = single a b + erase a f
have h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
Tactic: classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
⊢ f.update a b = single a b + erase a f
have h₁ : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((single j b + erase j f : (a : ι) → M) j : M)
Tactic: classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
h₁ :
  ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((single j b + erase j f : (a : ι) → M) j : M)
⊢ f.update a b = single a b + erase a f
have h₂ : ∀ (j : ι) (h : j ≠ a),
  Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((single a b + erase a f : (a : ι) → M) j : M)
Tactic: classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = erase a f + single a b
have h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
⊢ Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
have h : Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((erase j f + single j b : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne j a with (rfl | h)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
h : Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((erase j f + single j b : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
have h₁ : ∀ (h : j ≠ a), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
Tactic: rcases eq_or_ne j a with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
⊢ f.update a b = erase a f + single a b
have h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
Tactic: classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
h : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update a b : (a : ι) → M) j : M) ((erase a f + single a b : (a : ι) → M) j : M)
⊢ f.update a b = erase a f + single a b
have h₁ : ∀ (j : ι), Eq.{u_3 + 1} (α := M) ((f.update j b : (a : ι) → M) j : M) ((erase j f + single j b : (a : ι) → M) j : M)
Tactic: classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]
Cleared hypotheses: a