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
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
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)
⊢ (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 (α := ℤ) (-1) (n - k) * (↑(n.choose k) : ℤ)) • f (y + k • h)
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
⊢ f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y
have h₁ : f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y
Tactic: convert!
    congr_fun (LinearMap.congr_fun ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1
-- 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
h₁ : f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y
⊢ f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y
have h₂ : Eq.{u_2 + 1} (α := G) (∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y : G)
  ((∑ m ∈ range (n + 1),
          HPow.hPow (α := Module.End ℤ (M → G)) (fwdDiffₗ 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 ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1
-- 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
⊢ f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y
have h₁ : Eq.{u_2 + 1} (α := G) ((HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) n : (a : M → G) → M → G) f y : G)
  ((HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
Tactic: rw [← shiftₗ_pow_apply h f, shiftₗ]
-- 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
h₁ :
  Eq.{u_2 + 1} (α := G) ((HPow.hPow (α := Module.End ℤ (M → G)) (shiftₗ M G h) n : (a : M → G) → M → G) f y : G)
    ((HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
⊢ f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y
have h₂ : Eq.{u_2 + 1} (α := G) ((HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
  ((HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y : G)
Tactic: rw [← shiftₗ_pow_apply h f, shiftₗ]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
j : ℕ
⊢ Eq (α := ℕ → ℤ) (Δ_[1] fun (x : ℕ) ↦ (↑(x.choose (j + 1)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
have h : ∀ (n : ℕ), Eq (α := ℤ) (Δ_[1] (fun (x : ℕ) ↦ (↑(x.choose (j + 1)) : ℤ)) n) (↑(n.choose j) : ℤ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
j k : ℕ
⊢ Eq (α := ℕ → ℤ) (Δ_[1]^[k] fun (x : ℕ) ↦ (↑(x.choose (k + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
have zero : ∀ (j : ℕ), Eq (α := ℕ → ℤ) (Δ_[1]^[0] fun (x : ℕ) ↦ (↑(x.choose (0 + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
Tactic: induction k generalizing j with
  | zero => simp only [zero_add, iterate_zero, id_eq]
  | succ k IH =>
    simp only [iterate_succ_apply', add_assoc, add_comm 1 j, IH, fwdDiff_choose]
Cleared hypotheses: j, k
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
j k : ℕ
zero : ∀ (j : ℕ), Eq (α := ℕ → ℤ) (Δ_[1]^[0] fun (x : ℕ) ↦ (↑(x.choose (0 + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
⊢ Eq (α := ℕ → ℤ) (Δ_[1]^[k] fun (x : ℕ) ↦ (↑(x.choose (k + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
have succ : ∀ (k : ℕ)
  (IH :
    ∀ (j : ℕ), Eq (α := ℕ → ℤ) (Δ_[1]^[k] fun (x : ℕ) ↦ (↑(x.choose (k + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ))
  (j : ℕ), Eq (α := ℕ → ℤ) (Δ_[1]^[k + 1] fun (x : ℕ) ↦ (↑(x.choose (k + 1 + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
Tactic: induction k generalizing j with
  | zero => simp only [zero_add, iterate_zero, id_eq]
  | succ k IH =>
    simp only [iterate_succ_apply', add_assoc, add_comm 1 j, IH, fwdDiff_choose]
Cleared hypotheses: j, k
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m n : ℕ
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
have inl : ∀ (hmn : m < n), Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
Tactic: rcases lt_trichotomy m n with hmn | rfl | hnm
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m n : ℕ
inl : ∀ (hmn : m < n), Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
have inr : Eq (α := ℤ) (Δ_[1]^[m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m = m then 1 else 0 : ℤ)
Tactic: rcases lt_trichotomy m n with hmn | rfl | hnm
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m n : ℕ
inl : ∀ (hmn : m < n), Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
inr : Eq (α := ℤ) (Δ_[1]^[m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m = m then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
have inr₁ : ∀ (hnm : n < m), Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
Tactic: rcases lt_trichotomy m n with hmn | rfl | hnm
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m n : ℕ
hmn : m < n
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
have inl : ∀ (k : ℕ) (hmn : m < m + k + 1),
  Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
Tactic: rcases Nat.exists_eq_add_of_lt hmn with ⟨k, rfl⟩
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₆ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₆ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₇ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ 1) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₆ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₇ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ 1) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₈ : Eq (α := ℤ) (Δ_[1]^[k] (fun (x : ℕ) ↦ 0) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₆ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₇ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ 1) 0 : ℤ) (0 : ℤ)
inl₈ : Eq (α := ℤ) (Δ_[1]^[k] (fun (x : ℕ) ↦ 0) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₉ : Eq (α := ℤ) (∑ k_1 ∈ range (k + 1), HSMul.hSMul (β := ℤ) (HPow.hPow (α := ℤ) (-1) (k - k_1) * (↑(k.choose k_1) : ℤ)) 0)
  0
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m k : ℕ
hmn : m < m + k + 1
inl : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inl₁ : Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₂ : Eq (α := ℤ) (Δ_[1]^[k + 1 + m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₃ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] (Δ_[1]^[m] fun (x : ℕ) ↦ (↑(x.choose m) : ℤ))) 0 : ℤ) (0 : ℤ)
inl₄ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑(x.choose 0) : ℤ)) 0 : ℤ) (0 : ℤ)
inl₅ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1]^[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₆ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ (↑1 : ℤ)) 0 : ℤ) (0 : ℤ)
inl₇ : Eq (α := ℤ) (Δ_[1]^[k] (Δ_[1] fun (x : ℕ) ↦ 1) 0 : ℤ) (0 : ℤ)
inl₈ : Eq (α := ℤ) (Δ_[1]^[k] (fun (x : ℕ) ↦ 0) 0 : ℤ) (0 : ℤ)
inl₉ :
  Eq (α := ℤ)
    (∑ k_1 ∈ range (k + 1), HSMul.hSMul (β := ℤ) (HPow.hPow (α := ℤ) (-1) (k - k_1) * (↑(k.choose k_1) : ℤ)) 0) 0
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m then 1 else 0 : ℤ)
have inl₁₀ : Eq (α := ℤ) (∑ x ∈ range (k + 1), 0) 0
Tactic: simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
      add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
      fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
m n : ℕ
hnm : n < m
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)
have inr : ∀ (k : ℕ) (hnm : n < n + k + 1),
  Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
Tactic: rcases Nat.exists_eq_add_of_lt hnm with ⟨k, rfl⟩
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
n k : ℕ
hnm : n < n + k + 1
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
have inr : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
Tactic: simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
n k : ℕ
hnm : n < n + k + 1
inr : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
have inr₁ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
n k : ℕ
hnm : n < n + k + 1
inr : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inr₁ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
have inr₂ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + (k + 1))) : ℤ)) 0 : ℤ) (0 : ℤ)
Tactic: simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
n k : ℕ
hnm : n < n + k + 1
inr : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inr₁ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (0 : ℤ)
inr₂ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + (k + 1))) : ℤ)) 0 : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
have inr₃ : Eq (α := ℤ) (↑(Nat.choose 0 (k + 1)) : ℤ) 0
Tactic: simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
n k : ℕ
hnm : n < n + k + 1
inr : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if False then 1 else 0 : ℤ)
inr₁ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (0 : ℤ)
inr₂ : Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + (k + 1))) : ℤ)) 0 : ℤ) (0 : ℤ)
inr₃ : Eq (α := ℤ) (↑(Nat.choose 0 (k + 1)) : ℤ) 0
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)
have inr₄ : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
M : Type u_3
R : Type u_4
inst : AddCommMonoid M
inst_1 : Ring R
φ : AddChar M R
h : M
n : ℕ
IH :
  ∀ (x : M),
    Δ_[h]^[n] (⇑φ : (a : M) → R) x =
      HMul.hMul (β := R) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R) ^ n) ((φ : (a : M) → R) x : R)
x : M
⊢ Δ_[h]^[n + 1] (⇑φ : (a : M) → R) x =
    HMul.hMul (β := R) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R) ^ (n + 1))
      ((φ : (a : M) → R) x : R)
have succ : HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R) ^ n *
    HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) (x + h) : R) ((φ : (a : M) → R) x : R) =
  HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R) ^ n *
    HMul.hMul (β := R) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R)) ((φ : (a : M) → R) x : R)
Tactic: simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]