awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : SubNegZeroMonoid G
g₁ g₂ : ι →₀ G
a : ι
⊢ (g₁ - g₂ : (a : ι) → G) a = HSub.hSub (α := G) (β := 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 : SubNegZeroMonoid G
inst_1 : SubNegZeroMonoid H
f : G → H
hf : f 0 = 0
hf' : ∀ (x y : G), f (x - y) = f x - f y
v₁ v₂ : ι →₀ G
x : ι
⊢ Eq.{u_7 + 1} (α := H) ((mapRange f hf (v₁ - v₂) : (a : ι) → H) x : H)
    ((mapRange f hf v₁ - mapRange f hf v₂ : (a : ι) → H) x : H)

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

Premises used: Finsupp.mapRange_apply, Finsupp.sub_apply
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
G : Type u_6
H : Type u_7
inst : AddGroup G
inst_1 : SubtractionMonoid H
inst_2 : FunLike F G H
inst_3 : AddMonoidHomClass F G H
f : F
v : ι →₀ G
⊢ Eq (α := ι →₀ H) (mapRange (⇑f : (a : G) → H) ⋯ (-v)) (-mapRange (⇑f : (a : G) → H) ⋯ v)

Tactic:
mapRange_neg (map_neg f) v

Premises used: Finsupp.mapRange_neg, map_neg
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
F : Type u_2
G : Type u_6
H : Type u_7
inst : AddGroup G
inst_1 : SubtractionMonoid H
inst_2 : FunLike F G H
inst_3 : AddMonoidHomClass F G H
f : F
v₁ v₂ : ι →₀ G
⊢ mapRange (⇑f : (a : G) → H) ⋯ (v₁ - v₂) =
    HSub.hSub (α := ι →₀ H) (mapRange (⇑f : (a : G) → H) ⋯ v₁) (mapRange (⇑f : (a : G) → H) ⋯ v₂)

Tactic:
mapRange_sub (map_sub f) v₁ v₂

Premises used: map_sub, Finsupp.mapRange_sub
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
⊢ (-f).support = f.support

Tactic:
Finset.Subset.antisymm support_mapRange
    (calc
      support f = support (- -f) := congr_arg support (neg_neg _).symm
      _ ⊆ support (-f) := support_mapRange)

Premises used: Trans.trans, Finsupp.support, neg_neg, Finsupp.support_mapRange, congr_arg, Eq.symm, Finset.Subset.antisymm
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
inst_1 : DecidableEq ι
f g : ι →₀ G
rw : (f + -g).support ⊆ f.support ∪ (-g).support
⊢ (f - g).support ⊆ f.support ∪ g.support

Tactic:
rw [sub_eq_add_neg, ← support_neg g]

Premises used: sub_eq_add_neg, Finsupp.support_neg
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
inst_1 : DecidableEq ι
f g : ι →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support

Tactic:
support_add

Premises used: Set.Mem, setOf, Finsupp.support_add
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
inst_1 : DecidableEq ι
f g : ι →₀ G
⊢ (f + -g).support ⊆ f.support ∪ (-g).support

Tactic:
exact support_add

Premises used: Finsupp.support_add
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a : ι
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)
⊢ erase a f = HSub.hSub (β := ι →₀ G) f (single a ((f : (a : ι) → G) a) : ι →₀ G)

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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
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:
simp
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
f : ι →₀ G
a a' : ι
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:
simp [h]
-- Module: Mathlib.Algebra.Group.Finsupp
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
rw₁ 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
⊢ f.update 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]

Premises used: Finsupp.erase_eq_sub_single, Finsupp.update_eq_erase_add_single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
a : ι
b : G
⊢ Eq (α := ι →₀ G) (single a (-b)) (-single a b)

Tactic:
(singleAddHom a : G →+ _).map_neg b

Premises used: AddMonoidHom.map_neg, Finsupp.singleAddHom, Finsupp.single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
a : ι
b₁ b₂ : G
⊢ single a (b₁ - b₂) = HSub.hSub (α := ι →₀ G) (single a b₁) (single a b₂)

Tactic:
(singleAddHom a : G →+ _).map_sub b₁ b₂

Premises used: Finsupp.singleAddHom, AddMonoidHom.map_sub, Finsupp.single
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
a : ι
f : ι →₀ G
⊢ erase a (-f) = -erase a f

Tactic:
(eraseAddHom a : (_ →₀ G) →+ _).map_neg f

Premises used: Finsupp.erase, AddMonoidHom.map_neg, Finsupp.eraseAddHom
-- Module: Mathlib.Algebra.Group.Finsupp
Goal:
ι : Type u_1
G : Type u_6
inst : AddGroup G
a : ι
f₁ f₂ : ι →₀ G
⊢ erase a (f₁ - f₂) = erase a f₁ - erase a f₂

Tactic:
(eraseAddHom a : (_ →₀ G) →+ _).map_sub f₁ f₂

Premises used: Finsupp.erase, AddMonoidHom.map_sub, Finsupp.eraseAddHom
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f g : M → G
⊢ Δ_[h] (f + g) = Δ_[h] f + Δ_[h] g

Tactic:
add_sub_add_comm ..

Premises used: fwdDiff, add_sub_add_comm
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
g : G
⊢ Eq (α := M → G) (Δ_[h] fun (x : M) ↦ g) fun (x : M) ↦ 0

Tactic:
funext fun _ ↦ sub_self g

Premises used: sub_self, funext
-- Module: Mathlib.Algebra.Group.ForwardDiff
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₁ : ∀ (y : M), Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y
⊢ Δ_[h] (f • g) = Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g

Tactic:
ext y
-- Module: Mathlib.Algebra.Group.ForwardDiff
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 (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))
⊢ Δ_[h] (f • g) y = (Δ_[h] f • g + f • Δ_[h] g + Δ_[h] f • Δ_[h] g) y

Tactic:
simp only [fwdDiff, Pi.smul_apply', Pi.add_apply, smul_sub, sub_smul]

Premises used: sub_smul, Pi.smul_apply', fwdDiff, Pi.add_apply, smul_sub
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
⊢ 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:
abel
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Monoid R
inst_3 : DistribMulAction R G
r : R
f : M → G
⊢ Δ_[h] (r • f) = r • Δ_[h] f

Tactic:
funext fun _ ↦ (smul_sub ..).symm

Premises used: funext, smul_sub, HAdd.hAdd, Eq.symm
-- Module: Mathlib.Algebra.Group.ForwardDiff
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₁ : ∀ (y : M), Δ_[h] (fun (y : M) ↦ f y • g) y = HSMul.hSMul (β := M → G) (Δ_[h] f) (fun (x : M) ↦ g) y
⊢ (Δ_[h] fun (y : M) ↦ f y • g) = HSMul.hSMul (β := M → G) (Δ_[h] f) fun (x : M) ↦ g

Tactic:
ext y
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
y : M
⊢ Δ_[h] (fun (y : M) ↦ f y • g) y = HSMul.hSMul (β := M → G) (Δ_[h] f) (fun (x : M) ↦ g) y

Tactic:
simp only [fwdDiff, Pi.smul_apply', sub_smul]

Premises used: sub_smul, Pi.smul_apply', fwdDiff
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
⊢ Eq (α := (f : M → G) → M → G) (⇑(fwdDiffₗ M G h) : (a : M → G) → M → G) Δ_[h]

Tactic:
rfl

Premises used: fwdDiff, rfl
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
n : ℕ
h₁ :
  ∀ (x : M → G) (x_1 : M),
    (HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) n : (a : M → G) → M → G) x x_1 = Δ_[h]^[n] x x_1
⊢ Eq (α := (M → G) → M → G) (⇑(HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) n) : (a : M → G) → M → G)
    Δ_[h]^[n]

Tactic:
ext
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
n : ℕ
x : M → G
x_1 : M
h₁ : (⇑(fwdDiffₗ M G h) : (a : M → G) → M → G)^[n] x x_1 = Δ_[h]^[n] x x_1
h₂ h₃ : Δ_[h]^[n] x x_1 = Δ_[h]^[n] x x_1
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) n : (a : M → G) → M → G) x x_1 = Δ_[h]^[n] x x_1

Tactic:
rw [Module.End.pow_apply, coe_fwdDiffₗ]

Premises used: Module.End.pow_apply, fwdDiff_aux.coe_fwdDiffₗ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
y : M
⊢ (shiftₗ M G h : (a : M → G) → M → G) f y = f (y + h)

Tactic:
simp [shiftₗ, fwdDiff]

Premises used: fwdDiff_aux.shiftₗ, fwdDiff
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h y : M
f : M → G
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (β := ℕ) (shiftₗ M G h) 0 : (a : M → G) → M → G) f y =
    f (y + HSMul.hSMul (α := ℕ) 0 h)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h y : M
k : ℕ
IH : ∀ (f : M → G), (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y = f (y + k • h)
f : M → G
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) (k + 1) : (a : M → G) → M → G) f y = f (y + (k + 1) • h)

Tactic:
simp [pow_add, IH (shiftₗ M G h f), shiftₗ_apply, add_assoc, add_nsmul]

Premises used: add_assoc, fwdDiff_aux.shiftₗ, pow_add, fwdDiff_aux.shiftₗ_apply, DFunLike.coe, add_nsmul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
k : ℕ
y : M
zero :
  ∀ (f : M → G),
    (HPow.hPow (α := Module.End ℤ (M → G)) (β := ℕ) (shiftₗ M G h) 0 : (a : M → G) → M → G) f y =
      f (y + HSMul.hSMul (α := ℕ) 0 h)
succ :
  ∀ (k : ℕ)
    (IH :
      ∀ (f : M → G), (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y = f (y + k • h))
    (f : M → G),
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) (k + 1) : (a : M → G) → M → G) f y = f (y + (k + 1) • h)
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y = f (y + k • h)

Tactic:
induction k generalizing f with
  | zero => simp
  | succ k IH => simp [pow_add, IH (shiftₗ M G h f), shiftₗ_apply, add_assoc, add_nsmul]

Premises used: add_assoc, pow_add, fwdDiff_aux.shiftₗ_apply, Nat.zero, Nat.succ, add_nsmul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
α : Type u_3
s : Finset α
f : α → M → G
⊢ Eq (α := M → G) (Δ_[h] (∑ k ∈ s, f k)) (∑ k ∈ s, Δ_[h] (f k))

Tactic:
map_sum (fwdDiffₗ M G h) f s

Premises used: fwdDiff, map_sum, fwdDiff_aux.fwdDiffₗ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f g : M → G
n : ℕ
⊢ Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g

Tactic:
simpa only [coe_fwdDiffₗ_pow] using map_add (fwdDiffₗ M G h ^ n) f g

Premises used: map_add, fwdDiff_aux.fwdDiffₗ, HPow.hPow, fwdDiff_aux.coe_fwdDiffₗ_pow
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Monoid R
inst_3 : DistribMulAction R G
r : R
f : M → G
⊢ Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f

Tactic:
simp only [iterate_zero, id_eq]

Premises used: Function.iterate_zero, id_eq
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Monoid R
inst_3 : DistribMulAction R G
r : R
n : ℕ
IH : ∀ (f : M → G), Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
f : M → G
⊢ Δ_[h]^[n + 1] (r • f) = r • Δ_[h]^[n + 1] f

Tactic:
simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

Premises used: fwdDiff_const_smul, Function.iterate_succ_apply
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Monoid R
inst_3 : DistribMulAction R G
r : R
f : M → G
n : ℕ
zero : ∀ (f : M → G), Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f
succ :
  ∀ (n : ℕ) (IH : ∀ (f : M → G), Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f) (f : M → G),
    Δ_[h]^[n + 1] (r • f) = r • Δ_[h]^[n + 1] f
⊢ Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f

Tactic:
induction n generalizing f with
  | zero => simp only [iterate_zero, id_eq]
  | succ n IH => simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

Premises used: Function.iterate_zero, fwdDiff_const_smul, Function.iterate_succ_apply, Nat.zero, Nat.succ, id_eq
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
α : Type u_3
s : Finset α
f : α → M → G
n : ℕ
⊢ Eq (α := M → G) (Δ_[h]^[n] (∑ k ∈ s, f k)) (∑ k ∈ s, Δ_[h]^[n] (f k))

Tactic:
simpa only [coe_fwdDiffₗ_pow] using map_sum (fwdDiffₗ M G h ^ n) f s

Premises used: map_sum, fwdDiff_aux.fwdDiffₗ, HPow.hPow, fwdDiff_aux.coe_fwdDiffₗ_pow
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1

Tactic:
simp only [shiftₗ, add_sub_cancel_right]

Premises used: fwdDiff_aux.shiftₗ, add_sub_cancel_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1

Tactic:
have : fwdDiffₗ M G h = shiftₗ M G h - 1 := by simp only [shiftₗ, add_sub_cancel_right]
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
rw :
  Eq.{u_2 + 1} (α := G) ((HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
    (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) : G)
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h)

Tactic:
rw [← coe_fwdDiffₗ, this, ← Module.End.pow_apply]

Premises used: Module.End.pow_apply, fwdDiff_aux.coe_fwdDiffₗ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
⊢ Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)

Tactic:
have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
⊢ Eq.{u_2 + 1} (α := G) ((HAdd.hAdd (α := Module.End ℤ (M → G)) (shiftₗ M G h) (-1) ^ n : (a : M → G) → M → G) f y : G)
    ((∑ m ∈ range (n + 1),
            HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) m *
                HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - m) *
              (↑(n.choose m) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y :
      G)

Tactic:
congr_fun (LinearMap.congr_fun (this.add_pow n) f) y

Premises used: Commute.add_pow, LinearMap.congr_fun, congr_fun
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
h₁ : HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1 = HAdd.hAdd (α := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
h₂ :
  Eq.{u_2 + 1} (α := G)
    (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) : G)
    ((∑ m ∈ range (n + 1),
            HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) m *
                HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - m) *
              (↑(n.choose m) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y :
      G)
⊢ Eq.{u_2 + 1} (α := G) ((HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
    (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) : G)

Tactic:
convert! congr_fun (LinearMap.congr_fun (this.add_pow n) f) y using 3

Premises used: Commute.add_pow, LinearMap.congr_fun, congr_fun
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
⊢ HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1 = HAdd.hAdd (α := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)

Tactic:
simp only [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
h₁ :
  Eq.{u_2 + 1} (α := G) (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h))
    (∑ c ∈ range (n + 1),
      (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) c * HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - c) *
            (↑(n.choose c) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y)
⊢ Eq.{u_2 + 1} (α := G)
    (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) : G)
    ((∑ m ∈ range (n + 1),
            HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) m *
                HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - m) *
              (↑(n.choose m) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y :
      G)

Tactic:
rw [LinearMap.sum_apply, sum_apply]

Premises used: Finset.sum_apply, LinearMap.sum_apply
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
h₁ :
  ∀ (k : ℕ),
    (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
      (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k * HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) *
            (↑(n.choose k) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y
⊢ Eq.{u_2 + 1} (α := G) (∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h))
    (∑ c ∈ range (n + 1),
      (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) c * HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - c) *
            (↑(n.choose c) : Module.End ℤ (M → G)) :
          (a : M → G) → M → G)
        f y)

Tactic:
congr 1 with k
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := Module.End ℤ (M → G)) (↑(Int.negSucc 0 ^ (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G))
    (↑(Int.negSucc 0 ^ (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G))
⊢ HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) =
    (↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G))

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
⊢ HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) =
    (↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G))

Tactic:
have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G))
              = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast