awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)
refine : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
h : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M), a ∉ a_2.support → a_1 ≠ 0 → motive a_2 → single a a_1 + a_2 = a_2 + single a a_1
⊢ motive f
have refine₁ : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M),
  a ∉ a_2.support → a_1 ≠ 0 → motive a_2 → Disjoint (support (single a a_1)) a_2.support
Tactic: classical
  refine f.induction zero ?_
  convert! add_single using 7
  apply (addCommute_of_disjoint _).eq
  simp_all
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f
have suffices : ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f
Tactic: suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f
have refine_1 : ∀ (s : Finset ι) (f : ι →₀ M) (h : f.support = ∅), motive f
Tactic: refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
refine_1 : ∀ (s : Finset ι) (f : ι →₀ M) (h : f.support = ∅), motive f
⊢ ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f
have refine_2 : ∀ (s : Finset ι) (a : ι) (s : Finset ι) (hm : ∀ x ∈ s, x < a) (hf : ∀ (f : ι →₀ M), f.support = s → motive f)
  (f : ι →₀ M) (hs : f.support = insert a s), motive f
Tactic: refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ (erase a f).support = s
have rw : f.support.erase a = s
Tactic: rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
rw : f.support.erase a = s
⊢ (erase a f).support = s
have rw₁ : (insert a s).erase a = s
Tactic: rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
rw : f.support.erase a = s
rw₁ : (insert a s).erase a = s
⊢ (erase a f).support = s
have rw₂ : s = s
Tactic: rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
⊢ motive f
have refine_2 : ∀ (hs' : (erase a f).support = s), motive f
Tactic: have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive f
have refine_2 : motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
Tactic: rw [← single_add_erase a f]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have refine_2 : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
Tactic: refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
have refine_2 : a ∈ insert a s
Tactic: rw [← mem_support_iff, hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
⊢ motive f
have refine : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
Tactic: refine f.induction_on_max zero ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
have h : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
  a_1 ≠ 0 → motive a_2 → single a a_1 + a_2 = a_2 + single a a_1
Tactic: convert! add_single using 7 with _ _ _ H
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
a : ι
a_1 : M
a_2 : ι →₀ M
H : ∀ c ∈ a_2.support, c < a
h : a_1 ≠ 0
h_1 : motive a_2
⊢ single a a_1 + a_2 = a_2 + single a a_1
have this : ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a
Tactic: have := fun c hc ↦ (H c hc).ne
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
a : ι
a_1 : M
a_2 : ι →₀ M
H : ∀ c ∈ a_2.support, c < a
h : a_1 ≠ 0
h_1 : motive a_2
this : ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a
⊢ single a a_1 + a_2 = a_2 + single a a_1
have apply : Disjoint (support (single a a_1)) a_2.support
Tactic: apply (addCommute_of_disjoint _).eq
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
⊢ motive f
have refine : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
Tactic: classical
  refine f.induction_on_max zero ?_
  convert! add_single using 7 with _ _ _ H
  have := fun c hc ↦ (H c hc).ne
  apply (addCommute_of_disjoint _).eq
  simp_all [not_imp_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
refine : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f
have h : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
  a_1 ≠ 0 → motive a_2 → single a a_1 + a_2 = a_2 + single a a_1
Tactic: classical
  refine f.induction_on_max zero ?_
  convert! add_single using 7 with _ _ _ H
  have := fun c hc ↦ (H c hc).ne
  apply (addCommute_of_disjoint _).eq
  simp_all [not_imp_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
refine : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
h :
  ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
    a_1 ≠ 0 → motive a_2 → single a a_1 + a_2 = a_2 + single a a_1
⊢ motive f
have h₁ : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
  a_1 ≠ 0 → motive a_2 → ∀ (this : ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a), single a a_1 + a_2 = a_2 + single a a_1
Tactic: classical
  refine f.induction_on_max zero ?_
  convert! add_single using 7 with _ _ _ H
  have := fun c hc ↦ (H c hc).ne
  apply (addCommute_of_disjoint _).eq
  simp_all [not_imp_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
refine : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
h :
  ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
    a_1 ≠ 0 → motive a_2 → single a a_1 + a_2 = a_2 + single a a_1
h₁ :
  ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
    a_1 ≠ 0 → motive a_2 → ∀ (this : ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a), single a a_1 + a_2 = a_2 + single a a_1
⊢ motive f
have refine₁ : ∀ (a : ι) (a_1 : M) (a_2 : ι →₀ M) (H : ∀ c ∈ a_2.support, c < a),
  a_1 ≠ 0 →
    motive a_2 → ∀ (this : ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a), Disjoint (support (single a a_1)) a_2.support
Tactic: classical
  refine f.induction_on_max zero ?_
  convert! add_single using 7 with _ _ _ H
  have := fun c hc ↦ (H c hc).ne
  apply (addCommute_of_disjoint _).eq
  simp_all [not_imp_not]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) = HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw : HAdd.hAdd (α := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) k u) (Pi.single (M := fun (j : ι) ↦ M) l v) =
    HAdd.hAdd (α := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) m u) (Pi.single (M := fun (j : ι) ↦ M) n v) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) = HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw : (∀ (x : ι),
    Eq.{u_3 + 1} (α := M) ((HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) : (a : ι) → M) x : M)
      ((HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) : (a : ι) → M) x : M)) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: classical
    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
    exact Pi.single_add_single_eq_single_add_single hu hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
simp_rw :
  (∀ (x : ι),
      Eq.{u_3 + 1} (α := M) ((HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) : (a : ι) → M) x : M)
        ((HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) : (a : ι) → M) x : M)) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
⊢ HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) = HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw₁ : (∀ (x : ι),
    HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single k u) : (a : ι) → M) (⇑(single l v) : (a : ι) → M) x =
      HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single m u) : (a : ι) → M) (⇑(single n v) : (a : ι) → M) x) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: classical
    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
    exact Pi.single_add_single_eq_single_add_single hu hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
simp_rw :
  (∀ (x : ι),
      Eq.{u_3 + 1} (α := M) ((HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) : (a : ι) → M) x : M)
        ((HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) : (a : ι) → M) x : M)) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
simp_rw₁ :
  (∀ (x : ι),
      HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single k u) : (a : ι) → M) (⇑(single l v) : (a : ι) → M) x =
        HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single m u) : (a : ι) → M) (⇑(single n v) : (a : ι) → M) x) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
⊢ HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) = HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw₂ : (∀ (x : ι),
    HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) k u)
        (Pi.single (M := fun (j : ι) ↦ M) l v) x =
      HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) m u)
        (Pi.single (M := fun (j : ι) ↦ M) n v) x) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: classical
    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
    exact Pi.single_add_single_eq_single_add_single hu hv
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
k l m n : ι
u v : M
hu : u ≠ 0
hv : v ≠ 0
simp_rw :
  (∀ (x : ι),
      Eq.{u_3 + 1} (α := M) ((HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) : (a : ι) → M) x : M)
        ((HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) : (a : ι) → M) x : M)) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
simp_rw₁ :
  (∀ (x : ι),
      HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single k u) : (a : ι) → M) (⇑(single l v) : (a : ι) → M) x =
        HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (⇑(single m u) : (a : ι) → M) (⇑(single n v) : (a : ι) → M) x) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
simp_rw₂ :
  (∀ (x : ι),
      HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) k u)
          (Pi.single (M := fun (j : ι) ↦ M) l v) x =
        HAdd.hAdd (α := (a : ι) → M) (β := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) m u)
          (Pi.single (M := fun (j : ι) ↦ M) n v) x) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
⊢ HAdd.hAdd (α := ι →₀ M) (single k u) (single l v) = HAdd.hAdd (α := ι →₀ M) (single m u) (single n v) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw₃ : HAdd.hAdd (α := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) k u) (Pi.single (M := fun (j : ι) ↦ M) l v) =
    HAdd.hAdd (α := (a : ι) → M) (Pi.single (M := fun (j : ι) ↦ M) m u) (Pi.single (M := fun (j : ι) ↦ M) n v) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: classical
    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
    exact Pi.single_add_single_eq_single_add_single hu hv
-- 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 : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid O
f : N →+ O
g : M →+ N
⊢ Eq (α := (ι →₀ M) →+ ι →₀ O) (addMonoidHom (f.comp g)) (AddMonoidHom.comp (addMonoidHom f) (addMonoidHom g))
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_5 + 1} (α := O) ((((addMonoidHom (f.comp g) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((AddMonoidHom.comp (addMonoidHom f) (addMonoidHom g) : (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 : AddCommMonoid M
⊢ Eq (α := (ι →₀ M) ≃+ (ι →₀ M)) (addEquiv (AddEquiv.refl M)) (AddEquiv.refl (ι →₀ M))
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_3 + 1} (α := M) ((((addEquiv (AddEquiv.refl M) : (a : ι →₀ M) → ι →₀ M) x : ι →₀ M) : (a : ι) → M) a : M)
    ((((AddEquiv.refl (ι →₀ 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 : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid O
e₁ : M ≃+ N
e₂ : N ≃+ O
⊢ Eq (α := (ι →₀ M) ≃+ (ι →₀ O)) (addEquiv (e₁.trans e₂)) (AddEquiv.trans (addEquiv e₁) (addEquiv e₂))
have h : ∀ (x : ι →₀ M) (a : ι),
  Eq.{u_5 + 1} (α := O) ((((addEquiv (e₁.trans e₂) : (a : ι →₀ M) → ι →₀ O) x : ι →₀ O) : (a : ι) → O) a : O)
    ((((AddEquiv.trans (addEquiv e₁) (addEquiv e₂) : (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
G : Type u_6
inst : AddGroup G
inst_1 : DecidableEq ι
f g : ι →₀ G
⊢ (f - g).support ⊆ f.support ∪ g.support
have rw : (f + -g).support ⊆ f.support ∪ (-g).support
Tactic: rw [sub_eq_add_neg, ← support_neg g]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a : ι
⊢ erase a f = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G)
have h : ∀ (a' : ι),
  Eq.{u_6 + 1} (α := G) ((erase a f : (a : ι) → G) a' : G)
    ((HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) : (a : ι) → G) a' : G)
Tactic: ext a'
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a a' : ι
⊢ Eq.{u_6 + 1} (α := G) ((erase a f : (a : ι) → G) a' : G)
    ((HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) : (a : ι) → G) a' : G)
have h : Eq.{u_6 + 1} (α := G) ((erase a' f : (a : ι) → G) a' : G)
  ((HSub.hSub (β := ι →₀ G) f (single a' ((f : (a : ι) → G) a') : ι →₀ G) : (a : ι) → G) a' : G)
Tactic: rcases eq_or_ne a' a with (rfl | h)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a a' : ι
h :
  Eq.{u_6 + 1} (α := G) ((erase a' f : (a : ι) → G) a' : G)
    ((HSub.hSub (β := ι →₀ G) f (single a' ((f : (a : ι) → G) a') : ι →₀ G) : (a : ι) → G) a' : G)
⊢ Eq.{u_6 + 1} (α := G) ((erase a f : (a : ι) → G) a' : G)
    ((HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) : (a : ι) → G) a' : G)
have h₁ : ∀ (h : a' ≠ a),
  Eq.{u_6 + 1} (α := G) ((erase a f : (a : ι) → G) a' : G)
    ((HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) : (a : ι) → G) a' : G)
Tactic: rcases eq_or_ne a' a with (rfl | h)
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a : ι
b : G
⊢ f.update a b = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b
have rw : erase a f + single a b = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b
Tactic: rw [update_eq_erase_add_single, erase_eq_sub_single]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a : ι
b : G
rw : erase a f + single a b = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b
⊢ f.update a b = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b
have rw₁ : HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b =
  HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G) + single a b
Tactic: rw [update_eq_erase_add_single, erase_eq_sub_single]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Ring R
inst_3 : Module R G
f : M → R
g : M → G
⊢ Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g
have h₁ : ∀ (y : M), Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Ring R
inst_3 : Module R G
f : M → R
g : M → G
y : M
⊢ Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y
have h₁ : f (y + h) • g (y + h) - f y • g y =
  f (y + h) • g y - f y • g y + (f y • g (y + h) - f y • g y) +
    (f (y + h) • g (y + h) - f y • g (y + h) - (f (y + h) • g y - f y • g y))
Tactic: simp only [fwdDiff, Pi.smul_apply', Pi.add_apply, smul_sub, sub_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Ring R
inst_3 : Module R G
f : M → R
g : G
⊢ (Δ_[h] fun (y : M) ↦ f y • g) = HSMul.hSMul (β := M → G) (Δ_[h] f) fun (x : M) ↦ g
have h₁ : ∀ (y : M), Δ_[h] (fun (y : M) ↦ f y • g) y = HSMul.hSMul (β := M → G) (Δ_[h] f) (fun (x : M) ↦ g) y
Tactic: ext y