awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
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) (β := R) ((φ : (a : M) → R) h : R) ((φ : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
Tactic: rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
-- 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
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) (β := R) ((φ : (a : M) → R) h : R) ((φ : (a : M) → R) x : R) -
        HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
⊢ 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)
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 *
    HSub.hSub (α := R) ((φ : (a : M) → R) (h + x) : R) (HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
Tactic: rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
-- 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
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) (β := R) ((φ : (a : M) → R) h : R) ((φ : (a : M) → R) x : R) -
        HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
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 *
      HSub.hSub (α := R) ((φ : (a : M) → R) (h + x) : R) (HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
⊢ 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)
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 *
    HSub.hSub (α := R) ((φ : (a : M) → R) (x + h) : R) (HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
Tactic: rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
-- 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
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) (β := R) ((φ : (a : M) → R) h : R) ((φ : (a : M) → R) x : R) -
        HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
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 *
      HSub.hSub (α := R) ((φ : (a : M) → R) (h + x) : R) (HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
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 *
      HSub.hSub (α := R) ((φ : (a : M) → R) (x + h) : R) (HMul.hMul (α := R) (β := R) (1 : R) ((φ : (a : M) → R) x : R))
⊢ 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)
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 *
    HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) (x + h) : R) ((φ : (a : M) → R) x : R)
Tactic: rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
-- 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
x h : M
n : ℕ
⊢ Δ_[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)
have zero : ∀ (x : M),
  Δ_[h]^[0] (⇑φ : (a : M) → R) x =
    HMul.hMul (β := R) (HPow.hPow (β := ℕ) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R)) 0)
      ((φ : (a : M) → R) x : R)
Tactic: induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]
    rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
Cleared hypotheses: x, n
-- 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
x h : M
n : ℕ
zero :
  ∀ (x : M),
    Δ_[h]^[0] (⇑φ : (a : M) → R) x =
      HMul.hMul (β := R) (HPow.hPow (β := ℕ) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R)) 0)
        ((φ : (a : M) → R) x : R)
⊢ Δ_[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)
have succ : ∀ (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)
Tactic: induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]
    rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
have h₁ : ∀ (x : R),
  Eq (α := R) (Δ_[1] (fun (r : R) ↦ r ^ j) x)
    ((∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ j) 0
have this : Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
  (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
Tactic: have : (Δ_[1] fun (r : R) ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ j) 0
have succ : Eq.{u_3 + 1} (α := R → R) (∑ k ∈ range j, Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose k) fun (r : R) ↦ r ^ k)) 0
Tactic: rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range j
⊢ i < n
have this₁ : i < j
Tactic: have := mem_range.1 hi
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range j
⊢ Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i) = 0
have rw : HSMul.hSMul (β := R → R) (j.choose i) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0
Tactic: rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range j
rw : HSMul.hSMul (β := R → R) (j.choose i) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0
⊢ Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i) = 0
have rw₁ : HSMul.hSMul (β := R → R) (j.choose i) 0 = 0
Tactic: rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
j : ℕ
h : j < n + 1
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ j)
    (∑ i ∈ range j, HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range j
rw : HSMul.hSMul (β := R → R) (j.choose i) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0
rw₁ : HSMul.hSMul (β := R → R) (j.choose i) 0 = 0
⊢ Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i) = 0
have rw₂ : Eq.{u_3 + 1} (α := R → R) 0 0
Tactic: rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
j n : ℕ
h : j < n
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
have zero : ∀ {j : ℕ} (h : j < 0), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ r ^ j) 0
Tactic: induction n generalizing j with
  | zero => aesop
  | succ n ih =>
    have : (Δ_[1] fun (r : R) ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]
    exact sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]
Cleared hypotheses: j, n, h
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
j n : ℕ
h : j < n
zero : ∀ {j : ℕ} (h : j < 0), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ r ^ j) 0
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0
have succ : ∀ (n : ℕ) (ih : ∀ {j : ℕ} (h : j < n), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ j) 0) {j : ℕ}
  (h : j < n + 1), Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ j) 0
Tactic: induction n generalizing j with
  | zero => aesop
  | succ n ih =>
    have : (Δ_[1] fun (r : R) ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]
    exact sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]
Cleared hypotheses: j, n, h
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
have h : ∀ (x : R),
  Eq (α := R) (Δ_[1] (fun (r : R) ↦ r ^ (n + 1)) x)
    ((∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i) x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ (n + 1)) (↑(n + 1)! : R → R)
have this : Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
  (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
Tactic: have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ (n + 1)) (↑(n + 1)! : R → R)
have succ : ∑ x ∈ range n, HSMul.hSMul (β := R → R) ((n + 1).choose x) (Δ_[1]^[n] fun (r : R) ↦ r ^ x) +
    HSMul.hSMul (β := R → R) ((n + 1).choose n) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) =
  (↑(n + 1)! : R → R)
Tactic: simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range n
⊢ HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0
have rw : HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) 0 = 0
Tactic: rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
this :
  Eq.{u_3 + 1} (α := R → R) (Δ_[1] fun (r : R) ↦ r ^ (n + 1))
    (∑ i ∈ range (n + 1), HSMul.hSMul (β := (r : R) → R) ((n + 1).choose i) fun (r : R) ↦ r ^ i)
i : ℕ
hi : i ∈ range n
rw : HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) 0 = 0
⊢ HMul.hMul (α := R → R) (↑((n + 1).choose i) : R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ i) = 0
have rw₁ : Eq.{u_3 + 1} (α := R → R) 0 0
Tactic: rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
have zero : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ HPow.hPow (β := ℕ) r 0) (↑0! : R → R)
Tactic: induction n with
  | zero => aesop
  | succ n IH =>
    have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]
    simpa [IH, factorial_succ] using sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
zero : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ HPow.hPow (β := ℕ) r 0) (↑0! : R → R)
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)
have succ : ∀ (n : ℕ) (IH : Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ r ^ n) (↑n ! : R → R)),
  Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ (n + 1)) (↑(n + 1)! : R → R)
Tactic: induction n with
  | zero => aesop
  | succ n IH =>
    have : (Δ_[1] fun (r : R) ↦ r ^ (n + 1)) =
      ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i := by
      ext x
      simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]
    simp_rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum, fwdDiff_iter_const_smul,
       sum_range_succ]
    simpa [IH, factorial_succ] using sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_pow_eq_zero_of_lt (by have := mem_range.1 hi; lia), mul_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun (x : R) ↦ eval x P) x = HSMul.hSMul (β := R → R) P.leadingCoeff (↑P.natDegree ! : R → R) x
have simp_rw : (∑ x ∈ range (P.natDegree + 1), HSMul.hSMul (β := R → R) (P.coeff x) (Δ_[1]^[P.natDegree] fun (i : R) ↦ i ^ x)) x =
  HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) x)
Tactic: simp_rw [P.eval_eq_sum_range, ← sum_apply _ _ (fun i x ↦ P.coeff i * x ^ i),
    fwdDiff_iter_finsetSum, ← smul_eq_mul, ← Pi.smul_def, fwdDiff_iter_const_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
⊢ (∑ x ∈ range (P.natDegree + 1), HSMul.hSMul (β := R → R) (P.coeff x) (Δ_[1]^[P.natDegree] fun (i : R) ↦ i ^ x)) x =
    HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) x)
have rw : ∀ (i : ℕ) (hi : i ∈ range P.natDegree),
  HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0
Tactic: rw [sum_apply, sum_range_succ, sum_eq_zero (fun i hi ↦ ?_), zero_add,
    fwdDiff_iter_eq_factorial, leadingCoeff, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0
have rw : HSMul.hSMul (β := R → R) (P.coeff i) 0 x = 0
Tactic: rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
rw : HSMul.hSMul (β := R → R) (P.coeff i) 0 x = 0
⊢ HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0
have rw₁ : Eq.{u_3 + 1} (α := R) (0 x) 0
Tactic: rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
rw : HSMul.hSMul (β := R → R) (P.coeff i) 0 x = 0
rw₁ : Eq.{u_3 + 1} (α := R) (0 x) 0
⊢ HSMul.hSMul (β := R → R) (P.coeff i) (Δ_[1]^[P.natDegree] fun (i_1 : R) ↦ i_1 ^ i) x = 0
have rw₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
n : ℕ
hP : P.natDegree < n
x : R
⊢ Eq.{u_3 + 1} (α := R) (Δ_[1]^[n] (fun (x : R) ↦ eval x P) x : R) (0 x : R)
have obtain : ∀ (j : ℕ) (hP : P.natDegree < P.natDegree + j + 1),
  Eq.{u_3 + 1} (α := R) (Δ_[1]^[P.natDegree + j + 1] (fun (x : R) ↦ eval x P) x : R) (0 x : R)
Tactic: obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_lt hP
Cleared hypotheses: n, hP
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Eq.{u_3 + 1} (α := R) (Δ_[1]^[P.natDegree + j + 1] (fun (x : R) ↦ eval x P) x : R) (0 x : R)
have rw : Eq.{u_3 + 1} (α := R)
  (Δ_[1]^[j] (Δ_[1] fun (i : R) ↦ HSMul.hSMul (β := R) P.leadingCoeff ((↑P.natDegree ! : R → R) i)) x : R) (0 x : R)
Tactic: rw [add_assoc, add_comm, Function.iterate_add_apply, Function.iterate_succ_apply,
    P.fwdDiff_iter_degree_eq_factorial, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
P : R[X]
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[P.natDegree + 1] fun (x : R) ↦ eval x P) 0
have hP : P.natDegree < P.natDegree + 1
Tactic: have hP : P.natDegree < P.natDegree + 1 := Nat.lt_succ_self P.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Group.ForwardDiff (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
P : ℕ → R
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] fun (r : R) ↦ ∑ k ∈ range n, P k * r ^ k) 0
have simp_rw : Eq.{u_3 + 1} (α := R → R) (∑ c ∈ range n, HSMul.hSMul (β := R → R) (P c) (Δ_[1]^[n] fun (i : R) ↦ i ^ c)) 0
Tactic: simp_rw [← sum_apply _ _ (fun i x ↦ P i * x ^ i), fwdDiff_iter_finsetSum, sum_fn, ← smul_eq_mul,
    ← Pi.smul_def, fwdDiff_iter_const_smul, ← sum_fn]