awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Finsupp
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₂}
refine_2 : support (single f₂ g₂) ⊆ {f₁, f₂}
⊢ (HAdd.hAdd (α := ι →₀ M) (single f₁ g₁) (single f₂ g₂)).support ⊆ {f₁, f₂}

Tactic:
refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, subset_trans, And.intro, Finsupp.support_add, Finset.union_subset_iff
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ Subset (α := Finset ι) {f₁} {f₁, f₂}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ support (single f₁ g₁) ⊆ {f₁, f₂}

Tactic:
exact subset_trans Finsupp.support_single_subset (by simp)

Premises used: subset_trans, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ Subset (α := Finset ι) {f₂} {f₁, f₂}

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
inst_1 : DecidableEq ι
f₁ f₂ : ι
g₁ g₂ : M
⊢ support (single f₂ g₂) ⊆ {f₁, f₂}

Tactic:
exact subset_trans Finsupp.support_single_subset (by simp)

Premises used: subset_trans, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
M : Type u_8
inst : AddZeroClass M
d : M
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)
⊢ Eq (α := Unit →₀ M) ((AddEquiv.symm AddEquiv.finsuppUnique : (a : M) → Unit →₀ M) d : Unit →₀ M)
    (single () d : Unit →₀ M)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
M : Type u_8
inst : AddZeroClass M
d : M
⊢ 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:
simp [AddEquiv.finsuppUnique]

Premises used: AddEquiv.finsuppUnique
-- Module: Mathlib.Algebra.Group.Finsupp
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)
h₁ : ∀ (x : ι), Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)
⊢ AddCommute f g

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Finsupp
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)
neg : ∀ (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)

Tactic:
by_cases hf : x ∈ f.support

Premises used: Finsupp.support
-- Module: Mathlib.Algebra.Group.Finsupp
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)
neg : ∀ (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)

Tactic:
by_cases hg : x ∈ g.support

Premises used: Finsupp.support
-- Module: Mathlib.Algebra.Group.Finsupp
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
hg : x ∈ g.support
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)

Tactic:
h _ (mem_inter_of_mem hf hg)

Premises used: AddSemiconjBy, AddCommute, Finset.mem_inter_of_mem
-- Module: Mathlib.Algebra.Group.Finsupp
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
hg : x ∈ g.support
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)

Tactic:
exact h _ (mem_inter_of_mem hf hg)

Premises used: Finset.mem_inter_of_mem
-- Module: Mathlib.Algebra.Group.Finsupp
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
hg : x ∉ g.support
⊢ Eq.{u_3 + 1} (α := M) ((f + g : (a : ι) → M) x : M) ((g + f : (a : ι) → M) x : M)

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

Tactic:
simp_all
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f g : ι →₀ M
h : Disjoint f.support g.support
⊢ AddCommute f g

Tactic:
simp_all [addCommute_iff_inter, Finset.disjoint_iff_inter_eq_empty]

Premises used: Finset.disjoint_iff_inter_eq_empty, Finsupp.addCommute_iff_inter
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f g : ι →₀ M
h : Disjoint f.support g.support
⊢ AddCommute f g

Tactic:
classical simp_all [addCommute_iff_inter, Finset.disjoint_iff_inter_eq_empty]

Premises used: Finset.disjoint_iff_inter_eq_empty, Finsupp.addCommute_iff_inter
-- Module: Mathlib.Algebra.Group.Finsupp
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

Tactic:
ext j
-- Module: Mathlib.Algebra.Group.Finsupp
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)
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)
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
b : M
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
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:
simp [h, erase_ne]

Premises used: Finsupp.erase_ne
-- Module: Mathlib.Algebra.Group.Finsupp
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)
h₂ 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)
⊢ f.update a b = single a b + erase a f

Tactic:
classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

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

Tactic:
ext j
-- Module: Mathlib.Algebra.Group.Finsupp
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)
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)
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
b : M
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
b : M
j : ι
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:
simp [h, erase_ne]

Premises used: Finsupp.erase_ne
-- Module: Mathlib.Algebra.Group.Finsupp
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)
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)
h₂ h₃ :
  ∀ (j : ι) (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)
⊢ f.update a b = erase a f + single a b

Tactic:
classical
    ext j
    rcases eq_or_ne j a with (rfl | h)
    · simp
    · simp [h, erase_ne]

Premises used: Finsupp.erase_ne, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
h : Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
b : M
⊢ a ∉ f.support

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
h : Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
b : M
rw : single a b + erase a f = single a b + f
rw₁ rw₂ : single a b + f = single a b + f
⊢ f.update a b = single a b + f

Tactic:
rw [update_eq_single_add_erase, erase_of_notMem_support (by simpa)]

Premises used: Finsupp.erase_of_notMem_support, Finsupp.update_eq_single_add_erase
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
f : ι →₀ M
a : ι
h : Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
b : M
rw : erase a f + single a b = f + single a b
rw₁ rw₂ : f + single a b = f + single a b
⊢ f.update a b = f + single a b

Tactic:
rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]

Premises used: Finsupp.erase_of_notMem_support, Finsupp.update_eq_erase_add_single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
rw : f.update a ((f : (a : ι) → M) a) = f
rw₁ rw₂ : f = f
⊢ HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f) = f

Tactic:
rw [← update_eq_single_add_erase, update_self]

Premises used: Finsupp.update_self, Finsupp.update_eq_single_add_erase
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
rw : f.update a ((f : (a : ι) → M) a) = f
rw₁ rw₂ : f = f
⊢ HAdd.hAdd (β := ι →₀ M) (erase a f) (single a ((f : (a : ι) → M) a) : ι →₀ M) = f

Tactic:
rw [← update_eq_erase_add_single, update_self]

Premises used: Finsupp.update_self, Finsupp.update_eq_erase_add_single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
h :
  ∀ (s : ι),
    Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
⊢ erase a (f + f') = erase a f + erase a f'

Tactic:
ext s
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
pos :
  ∀ (hs : s = a),
    Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
neg :
  ∀ (hs : ¬s = a),
    Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)

Tactic:
by_cases hs : s = a
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : s = a
pos : Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) a : M) ((erase a f + erase a f' : (a : ι) → M) a : M)
pos₁ :
  (erase a (f + f') : (a : ι) → M) a =
    HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) a : M) ((erase a f' : (a : ι) → M) a : M)
pos₂ : 0 = HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) a : M) ((erase a f' : (a : ι) → M) a : M)
pos₃ : 0 = HAdd.hAdd (α := M) (β := M) (0 : M) ((erase a f' : (a : ι) → M) a : M)
pos₄ : 0 = HAdd.hAdd (α := M) 0 0
pos₅ pos₆ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)

Tactic:
rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]

Premises used: Finsupp.erase_same, Finsupp.add_apply, add_zero
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
hs : ¬s = a
neg :
  (erase a (f + f') : (a : ι) → M) s =
    HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) s : M) ((erase a f' : (a : ι) → M) s : M)
neg₁ :
  (f + f' : (a : ι) → M) s =
    HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) s : M) ((erase a f' : (a : ι) → M) s : M)
neg₂ :
  (f + f' : (a : ι) → M) s = HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((erase a f' : (a : ι) → M) s : M)
neg₃ : (f + f' : (a : ι) → M) s = HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((f' : (a : ι) → M) s : M)
neg₄ neg₅ :
  HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((f' : (a : ι) → M) s : M) =
    HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((f' : (a : ι) → M) s : M)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)

Tactic:
rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

Premises used: Finsupp.erase_ne, Finsupp.add_apply
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s : Finset ι
f : ι →₀ M
hf : f.support = ∅
rwa rwa₁ rwa₂ rwa₃ : motive 0
⊢ motive f

Tactic:
rwa [support_eq_empty.1 hf]

Premises used: Iff.mp, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
this : motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : motive f), motive f
⊢ motive f

Tactic:
rwa [single_add_erase] at this

Premises used: Finsupp.single_add_erase
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
suffices : motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
⊢ motive f

Tactic:
suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
a₁ : a ∉ (erase a f).support
a₂ : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
a₃ : motive (erase a f)
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))

Tactic:
apply single_add
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
a₁ : ¬(a ≠ a ∧ a ∈ f.support)
⊢ a ∉ (erase a f).support

Tactic:
rw [support_erase, mem_erase]

Premises used: Finsupp.support_erase, Finset.mem_erase
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
fun H => H.1 rfl

Premises used: And.left, Not, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
exact fun H => H.1 rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
a₁ : a ∈ cons a s has
⊢ Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)

Tactic:
rw [← mem_support_iff, hf]

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has

Tactic:
mem_cons_self _ _

Premises used: Finset.mem_cons_self
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has

Tactic:
exact mem_cons_self _ _

Premises used: Finset.mem_cons_self
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
apply : (erase a f).support = s
⊢ motive (erase a f)

Tactic:
apply ih _ _
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
rw : f.support.erase a = s
rw₁ : (cons a s has).erase a = s
rw₂ rw₃ : s = s
⊢ (erase a f).support = s

Tactic:
rw [support_erase, hf, Finset.erase_cons]

Premises used: Finset.erase_cons, Finsupp.support_erase
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
motive : (ι →₀ M) → Prop
f_1 : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hf : f.support = cons a s has
a₁ : a ∉ (erase a f).support
a₂ : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
a₃ : motive (erase a f)
a₄ : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
a₅ a₆ : motive (erase a f)
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))

Tactic:
classical
      apply single_add
      · rw [support_erase, mem_erase]
        exact fun H => H.1 rfl
      · rw [← mem_support_iff, hf]
        exact mem_cons_self _ _
      · apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

Premises used: Finsupp.mem_support_iff, Finset.erase_cons, Finsupp.support_erase, Finset.mem_erase, Finset.mem_cons_self
-- 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)
⊢ motive f

Tactic:
f.induction zero ?_

Premises used: Finsupp.induction
-- 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)
⊢ motive f

Tactic:
refine f.induction zero ?_
-- 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 : ι) (b : M) (f : ι →₀ M), a ∉ f.support → 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
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)
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
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
convert! add_single using 7
-- 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
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