awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
n : ℕ
⊢ Eq (α := (M → G) → M → G) (⇑(HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) n) : (a : M → G) → M → G)
    Δ_[h]^[n]
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
n : ℕ
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
have h₁ : (⇑(fwdDiffₗ M G h) : (a : M → G) → M → G)^[n] x x_1 = Δ_[h]^[n] x x_1
Tactic: rw [Module.End.pow_apply, coe_fwdDiffₗ]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) n : (a : M → G) → M → G) x x_1 = Δ_[h]^[n] x x_1
have h₂ : Δ_[h]^[n] x x_1 = Δ_[h]^[n] x x_1
Tactic: rw [Module.End.pow_apply, coe_fwdDiffₗ]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
k : ℕ
y : M
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y = f (y + k • h)
have 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)
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]
Cleared hypotheses: f, k
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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)
⊢ (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y = f (y + k • h)
have 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)
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]
Cleared hypotheses: f, k
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : Monoid R
inst_3 : DistribMulAction R G
r : R
f : M → G
n : ℕ
⊢ Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
have zero : ∀ (f : M → G), Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] 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]
Cleared hypotheses: f, n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
R : Type u_3
inst_2 : 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
⊢ Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f
have 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
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]
Cleared hypotheses: f, n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h)
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
⊢ Δ_[h]^[n] f y = ∑ k ∈ range (n + 1), (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h)
have 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)
Tactic: rw [← coe_fwdDiffₗ, this, ← Module.End.pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
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
⊢ 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)
have this₁ : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
Tactic: have : Commute (shiftₗ M G h) (-1) := (Commute.one_right _).neg_right
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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) ((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)
have h₁ : HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1 = HAdd.hAdd (α := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
Tactic: convert! congr_fun (LinearMap.congr_fun (this.add_pow n) f) y using 3
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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)
⊢ 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)
have 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)
Tactic: convert! congr_fun (LinearMap.congr_fun (this.add_pow n) f) y using 3
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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)
    (∑ 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)
have 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)
Tactic: rw [LinearMap.sum_apply, sum_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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) (∑ 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)
have 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
Tactic: congr 1 with k
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
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))
have 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))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
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 (α := ℤ) (-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
have this₁ : 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
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
⊢ (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
have h₁ : (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
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
h₁ :
  (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
⊢ (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
have h₂ : (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
  (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
    ((HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) : (a : M → G) → M → G)
        f :
      M → G)
    y
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
h₁ :
  (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
h₂ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) :
            (a : M → G) → M → G)
          f :
        M → G)
      y
⊢ (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
have h₃ : (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
  (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
    (((↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G)) : (a : M → G) → M → G) f :
      M → G)
    y
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
h₁ :
  (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
h₂ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) :
            (a : M → G) → M → G)
          f :
        M → G)
      y
h₃ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      (((↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G)) : (a : M → G) → M → G) f :
        M → G)
      y
⊢ (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
have h₄ : (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
  (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
    ((HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f) y
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
h₁ :
  (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
h₂ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) :
            (a : M → G) → M → G)
          f :
        M → G)
      y
h₃ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      (((↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G)) : (a : M → G) → M → G) f :
        M → G)
      y
h₄ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f) y
⊢ (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
have h₅ : (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
  HSMul.hSMul (β := M → G) (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ))
    ((HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f : M → G) y
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_1
G : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this_1 : fwdDiffₗ M G h = HSub.hSub (α := Module.End ℤ (M → G)) (shiftₗ M G h) 1
this_2 : Commute (S := Module.End ℤ (M → G)) (shiftₗ M G h) (-1)
k : ℕ
this :
  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))
h₁ :
  (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
h₂ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := Module.End ℤ (M → G)) (-1) (n - k) * (↑(n.choose k) : Module.End ℤ (M → G)) :
            (a : M → G) → M → G)
          f :
        M → G)
      y
h₃ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      (((↑(HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) : Module.End ℤ (M → G)) : (a : M → G) → M → G) f :
        M → G)
      y
h₄ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    (HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G)
      ((HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f) y
h₅ :
  (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
    HSMul.hSMul (β := M → G) (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ))
      ((HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f : M → G) y
⊢ (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
have h₆ : (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h) =
  HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ))
    ((HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) k : (a : M → G) → M → G) f y : G)
Tactic: rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]