awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Finsupp
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)
a : ι
a_1 : M
a_2 : ι →₀ M
h : a ∉ a_2.support
h_1 : a_1 ≠ 0
h_2 : motive a_2
⊢ Disjoint (support (single a a_1)) a_2.support

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Finsupp
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
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
⊢ motive f

Tactic:
classical
  refine f.induction zero ?_
  convert! add_single using 7
  apply (addCommute_of_disjoint _).eq
  simp_all

Premises used: Finsupp.addCommute_of_disjoint, AddCommute.eq
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add : ∀ (f g : ι →₀ M), motive f → motive g → motive (f + g)
single : ∀ (a : ι) (b : M), motive (Finsupp.single a b)
⊢ motive f

Tactic:
induction₂ f zero fun _a _b _f _ _ w => add _ _ w (single _ _)

Premises used: Finsupp.induction₂
-- Module: Mathlib.Algebra.Group.Finsupp
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)
suffices : ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f
⊢ motive f

Tactic:
suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
-- Module: Mathlib.Algebra.Group.Finsupp
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

Tactic:
fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)

Premises used: Finset.induction_on_max
-- Module: Mathlib.Algebra.Group.Finsupp
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
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
⊢ ∀ (s : Finset ι) (f : ι →₀ M), f.support = s → motive f

Tactic:
refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
-- Module: Mathlib.Algebra.Group.Finsupp
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 : Finset ι
f : ι →₀ M
h : f.support = ∅
refine_1 refine_1₁ refine_1₂ refine_1₃ : motive 0
⊢ motive f

Tactic:
rwa [support_eq_empty.1 h]

Premises used: Iff.mp, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.Group.Finsupp
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
rw₂ rw₃ : s = s
⊢ (erase a f).support = s

Tactic:
rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]

Premises used: Finsupp.support_erase, Finset.erase_insert, LT.lt.false
-- Module: Mathlib.Algebra.Group.Finsupp
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
refine_2 : ∀ (hs' : (erase a f).support = s), motive f
⊢ motive f

Tactic:
have hs' : (erase a f).support = s := by
      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
-- Module: Mathlib.Algebra.Group.Finsupp
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
refine_2 : motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
⊢ motive f

Tactic:
rw [← single_add_erase a f]

Premises used: Finsupp.single_add_erase
-- Module: Mathlib.Algebra.Group.Finsupp
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))

Tactic:
single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Group.Finsupp
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
refine_2 : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))

Tactic:
refine single_add _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Group.Finsupp
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
refine_2 : a ∈ insert a s
⊢ Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)

Tactic:
rw [← mem_support_iff, hs]

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.Group.Finsupp
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
⊢ a ∈ insert a s

Tactic:
mem_insert_self a s

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Algebra.Group.Finsupp
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
⊢ a ∈ insert a s

Tactic:
exact mem_insert_self a s

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Algebra.Group.Finsupp
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, a < c) → b ≠ 0 → motive f → motive (single a b + f)
⊢ motive f

Tactic:
induction_on_max (ι := ιᵒᵈ) f zero single_add

Premises used: Finsupp.induction_on_max
-- Module: Mathlib.Algebra.Group.Finsupp
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

Tactic:
f.induction_on_max zero ?_

Premises used: Finsupp.induction_on_max
-- Module: Mathlib.Algebra.Group.Finsupp
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

Tactic:
refine f.induction_on_max zero ?_

Premises used: Finsupp.induction_on_max
-- Module: Mathlib.Algebra.Group.Finsupp
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 (f + single a b)

Tactic:
add_single
-- Module: Mathlib.Algebra.Group.Finsupp
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)
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
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
convert! add_single using 7 with _ _ _ H
-- Module: Mathlib.Algebra.Group.Finsupp
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
⊢ ∀ (c : ι) (hc : c ∈ a_2.support), c ≠ a

Tactic:
have := fun c hc ↦ (H c hc).ne
-- Module: Mathlib.Algebra.Group.Finsupp
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
apply : Disjoint (support (single a a_1)) a_2.support
⊢ single a a_1 + a_2 = a_2 + single a a_1

Tactic:
apply (addCommute_of_disjoint _).eq

Premises used: Finsupp.addCommute_of_disjoint, AddCommute.eq
-- Module: Mathlib.Algebra.Group.Finsupp
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
⊢ Disjoint (support (single a a_1)) a_2.support

Tactic:
simp_all [not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.Algebra.Group.Finsupp
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
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
⊢ motive 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]

Premises used: Finsupp.addCommute_of_disjoint, Finsupp.induction_on_max, AddCommute.eq, not_imp_not
-- Module: Mathlib.Algebra.Group.Finsupp
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, a < c) → b ≠ 0 → motive f → motive (f + single a b)
⊢ motive f

Tactic:
induction_on_max₂ (ι := ιᵒᵈ) f zero add_single

Premises used: Finsupp.induction_on_max₂
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddMonoid M
n : ℕ
f : ι →₀ M
⊢ (⇑(n • f) : (a : ι) → M) = HSMul.hSMul (β := (a : ι) → M) n (⇑f : (a : ι) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddMonoid M
n : ℕ
f : ι →₀ M
x : ι
⊢ (n • f : (a : ι) → M) x = HSMul.hSMul (β := M) n ((f : (a : ι) → M) x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
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 : AddMonoid M
inst_1 : IsAddTorsionFree M
⊢ IsAddTorsionFree (ι →₀ M)

Tactic:
DFunLike.coe_injective.isAddTorsionFree coeFnAddHom

Premises used: Finsupp.coeFnAddHom, DFunLike.coe_injective, Function.Injective.isAddTorsionFree
-- Module: Mathlib.Algebra.Group.Finsupp
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 :
  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
⊢ 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

Tactic:
simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]

Premises used: funext_iff, DFunLike.ext_iff, Finsupp.coe_add, Finsupp.single_eq_pi_single
-- Module: Mathlib.Algebra.Group.Finsupp
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 (α := (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:
Pi.single_add_single_eq_single_add_single hu hv

Premises used: Pi.single_add_single_eq_single_add_single
-- Module: Mathlib.Algebra.Group.Finsupp
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 (α := (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:
exact Pi.single_add_single_eq_single_add_single hu hv

Premises used: Pi.single_add_single_eq_single_add_single
-- Module: Mathlib.Algebra.Group.Finsupp
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
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
⊢ 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

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

Premises used: funext_iff, DFunLike.ext_iff, Finsupp.coe_add, Pi.single_add_single_eq_single_add_single, Finsupp.single_eq_pi_single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
⊢ Eq (α := (ι →₀ M) →+ ι →₀ M) (addMonoidHom (AddMonoidHom.id M)) (AddMonoidHom.id (ι →₀ M))

Tactic:
AddMonoidHom.ext mapRange_id

Premises used: AddMonoidHom.ext, Finsupp.mapRange_id
-- Module: Mathlib.Algebra.Group.Finsupp
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
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)
⊢ Eq (α := (ι →₀ M) →+ ι →₀ O) (addMonoidHom (f.comp g)) (AddMonoidHom.comp (addMonoidHom f) (addMonoidHom g))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
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
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : M →+ N
⊢ Eq (α := ZeroHom (ι →₀ M) (ι →₀ N)) (↑(addMonoidHom f) : ZeroHom (ι →₀ M) (ι →₀ N)) (zeroHom (↑f : ZeroHom M N))

Tactic:
rfl

Premises used: Finsupp.mapRange.zeroHom, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
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)
⊢ Eq (α := (ι →₀ M) ≃+ (ι →₀ M)) (addEquiv (AddEquiv.refl M)) (AddEquiv.refl (ι →₀ M))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddCommMonoid M
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
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
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)
⊢ Eq (α := (ι →₀ M) ≃+ (ι →₀ O)) (addEquiv (e₁.trans e₂)) (AddEquiv.trans (addEquiv e₁) (addEquiv e₂))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
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
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
e : M ≃+ N
⊢ Eq (α := (ι →₀ N) ≃+ (ι →₀ M)) (AddEquiv.symm (addEquiv e)) (addEquiv e.symm)

Tactic:
rfl

Premises used: Finsupp.mapRange.equiv, Finsupp.onFinset, Finsupp.mapRange.addEquiv, Equiv.symm, Finsupp.mapRange, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
e : M ≃+ N
⊢ (↑(addEquiv e) : (ι →₀ M) →+ ι →₀ N) = addMonoidHom e.toAddMonoidHom

Tactic:
rfl

Premises used: Finsupp.mapRange.addMonoidHom, AddMonoidHomClass.toAddMonoidHom, Finsupp.onFinset, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
e : M ≃+ N
⊢ (↑(addEquiv e) : (ι →₀ M) ≃ (ι →₀ N)) = equiv (↑e : M ≃ N) ⋯

Tactic:
rfl

Premises used: Finsupp.mapRange.equiv, Finsupp.onFinset, Finsupp.mapRange, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : NegZeroClass G
g : ι →₀ G
⊢ Eq (α := (a : ι) → G) (⇑(-g) : (a : ι) → G) (-(⇑g : (a : ι) → G))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : NegZeroClass G
g : ι →₀ G
a : ι
⊢ Eq.{u_6 + 1} (α := G) ((-g : (a : ι) → G) a : G) (-(g : (a : ι) → G) a : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
H : Type u_7
inst : NegZeroClass G
inst_1 : NegZeroClass H
f : G → H
hf : f 0 = 0
hf' : ∀ (x : G), f (-x) = -f x
v : ι →₀ G
x : ι
⊢ Eq.{u_7 + 1} (α := H) ((mapRange f hf (-v) : (a : ι) → H) x : H) ((-mapRange f hf v : (a : ι) → H) x : H)

Tactic:
simp only [hf', neg_apply, mapRange_apply]

Premises used: Finsupp.mapRange_apply, Finsupp.neg_apply
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : SubNegZeroMonoid G
g₁ g₂ : ι →₀ G
⊢ (⇑(g₁ - g₂) : (a : ι) → G) = HSub.hSub (α := (a : ι) → G) (⇑g₁ : (a : ι) → G) (⇑g₂ : (a : ι) → G)

Tactic:
rfl

Premises used: rfl