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
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)
⊢ f.update a b = erase a f + single a b
have 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)
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 : ι
h : Eq.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
b : M
⊢ f.update a b = single a b + f
have rw : single a b + erase a f = single a b + f
Tactic: rw [update_eq_single_add_erase, erase_of_notMem_support (by simpa)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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
⊢ f.update a b = single a b + f
have rw₁ : single a b + f = single a b + f
Tactic: rw [update_eq_single_add_erase, erase_of_notMem_support (by simpa)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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
⊢ f.update a b = f + single a b
have rw : erase a f + single a b = f + single a b
Tactic: rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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
⊢ f.update a b = f + single a b
have rw₁ : f + single a b = f + single a b
Tactic: rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
⊢ HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f) = f
have rw : f.update a ((f : (a : ι) → M) a) = f
Tactic: rw [← update_eq_single_add_erase, update_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
rw : f.update a ((f : (a : ι) → M) a) = f
⊢ HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f) = f
have rw₁ : f = f
Tactic: rw [← update_eq_single_add_erase, update_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
⊢ HAdd.hAdd (β := ι →₀ M) (erase a f) (single a ((f : (a : ι) → M) a) : ι →₀ M) = f
have rw : f.update a ((f : (a : ι) → M) a) = f
Tactic: rw [← update_eq_erase_add_single, update_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f : ι →₀ M
rw : f.update a ((f : (a : ι) → M) a) = f
⊢ HAdd.hAdd (β := ι →₀ M) (erase a f) (single a ((f : (a : ι) → M) a) : ι →₀ M) = f
have rw₁ : f = f
Tactic: rw [← update_eq_erase_add_single, update_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
⊢ erase a (f + f') = erase a f + erase a f'
have 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)
Tactic: ext s
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have 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)
Tactic: by_cases hs : s = a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have 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)
Tactic: by_cases hs : s = a
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
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)
have pos : Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) a : M) ((erase a f + erase a f' : (a : ι) → M) a : M)
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have 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)
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have pos₂ : 0 = HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) a : M) ((erase a f' : (a : ι) → M) a : M)
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have pos₃ : 0 = HAdd.hAdd (α := M) (β := M) (0 : M) ((erase a f' : (a : ι) → M) a : M)
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have pos₄ : 0 = HAdd.hAdd (α := M) 0 0
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have pos₅ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : AddZeroClass M
a : ι
f f' : ι →₀ M
s : ι
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)
have 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)
Tactic: rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have neg₁ : (f + f' : (a : ι) → M) s =
  HAdd.hAdd (α := M) (β := M) ((erase a f : (a : ι) → M) s : M) ((erase a f' : (a : ι) → M) s : M)
Tactic: rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have neg₂ : (f + f' : (a : ι) → M) s = HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((erase a f' : (a : ι) → M) s : M)
Tactic: rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have neg₃ : (f + f' : (a : ι) → M) s = HAdd.hAdd (α := M) (β := M) ((f : (a : ι) → M) s : M) ((f' : (a : ι) → M) s : M)
Tactic: rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Finsupp (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((erase a (f + f') : (a : ι) → M) s : M) ((erase a f + erase a f' : (a : ι) → M) s : M)
have 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)
Tactic: rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
-- 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_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))
⊢ motive f
have rwa : ∀ (this : motive f), motive f
Tactic: rwa [single_add_erase] at this
Cleared hypotheses: this
-- 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_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
⊢ motive f
have suffices : motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
Tactic: suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
-- 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_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
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₁ : a ∉ (erase a f).support
Tactic: apply single_add
-- 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_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
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₂ : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
Tactic: apply single_add
-- 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_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)
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₃ : motive (erase a f)
Tactic: apply single_add
-- 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_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 ∉ (erase a f).support
have a₁ : ¬(a ≠ a ∧ a ∈ f.support)
Tactic: rw [support_erase, mem_erase]
-- 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_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
⊢ Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
have a₁ : a ∈ cons a s has
Tactic: rw [← mem_support_iff, hf]
-- 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_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
⊢ motive (erase a f)
have apply : (erase a f).support = s
Tactic: apply ih _ _
-- 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_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
⊢ (erase a f).support = s
have rw : f.support.erase a = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- 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_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
⊢ (erase a f).support = s
have rw₁ : (cons a s has).erase a = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- 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_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
⊢ (erase a f).support = s
have rw₂ : s = s
Tactic: rw [support_erase, hf, Finset.erase_cons]
-- 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_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
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₁ : a ∉ (erase a f).support
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]
-- 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_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
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₂ : Ne.{u_3 + 1} (α := M) ((f : (a : ι) → M) a : M) (0 : M)
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]
-- 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_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)
⊢ motive (HAdd.hAdd (α := ι →₀ M) (single a ((f : (a : ι) → M) a) : ι →₀ M) (erase a f))
have a₃ : motive (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]
-- 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)
⊢ motive f
have refine : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
Tactic: refine f.induction zero ?_
-- 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)
⊢ ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
have 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
Tactic: convert! add_single using 7
-- 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)
a : ι
a_1 : M
a_2 : ι →₀ M
h : a ∉ a_2.support
h_1 : a_1 ≠ 0
h_2 : motive a_2
⊢ 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
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
have refine : ∀ (a : ι) (b : M) (f : ι →₀ M), a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)
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
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
have 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
Tactic: classical
  refine f.induction zero ?_
  convert! add_single using 7
  apply (addCommute_of_disjoint _).eq
  simp_all