awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
h₇ 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)
⊢ (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]

Premises used: Module.End.intCast_apply, mul_assoc, fwdDiff_aux.shiftₗ_pow_apply, Module.End.mul_apply, map_smul, Pi.smul_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
m : M
n : ℕ
y : M
⊢ Δ_[h]^[n] (fun (r : M) ↦ f (r + m)) y = Δ_[h]^[n] f (y + m)

Tactic:
simp [fwdDiff_iter_eq_sum_shift, add_right_comm]

Premises used: fwdDiff_iter_eq_sum_shift, add_right_comm
-- 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
m y : M
⊢ Δ_[h] (fun (r : M) ↦ f (r + m)) y = Δ_[h] f (y + m)

Tactic:
fwdDiff_iter_comp_add h f m 1 y

Premises used: fwdDiff_iter_comp_add, fwdDiff, Nat.iterate, OfNat.ofNat
-- 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
⊢ 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)
    ((∑ 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:
congr_fun (LinearMap.congr_fun ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y

Premises used: Commute.add_pow, fwdDiff_aux.fwdDiffₗ, LinearMap.congr_fun, congr_fun, Commute.one_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
h₁ : f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y
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)
⊢ f (y + n • h) = ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y

Tactic:
convert!
    congr_fun (LinearMap.congr_fun ((Commute.one_right (fwdDiffₗ M G h)).add_pow n) f) y using 1

Premises used: Commute.add_pow, fwdDiff_aux.fwdDiffₗ, LinearMap.congr_fun, congr_fun, Commute.one_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
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)
h₂ 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)
⊢ f (y + n • h) = (HAdd.hAdd (α := Module.End ℤ (M → G)) (fwdDiffₗ M G h) 1 ^ n : (a : M → G) → M → G) f y

Tactic:
rw [← shiftₗ_pow_apply h f, shiftₗ]

Premises used: fwdDiff_aux.shiftₗ, fwdDiff_aux.shiftₗ_pow_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
⊢ 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:
simp [Module.End.pow_apply, coe_fwdDiffₗ]

Premises used: Module.End.pow_apply, fwdDiff_aux.coe_fwdDiffₗ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
j : ℕ
h : ∀ (n : ℕ), Eq (α := ℤ) (Δ_[1] (fun (x : ℕ) ↦ (↑(x.choose (j + 1)) : ℤ)) n) (↑(n.choose j) : ℤ)
⊢ Eq (α := ℕ → ℤ) (Δ_[1] fun (x : ℕ) ↦ (↑(x.choose (j + 1)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)

Tactic:
ext n
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
j n : ℕ
⊢ Eq (α := ℤ) (Δ_[1] (fun (x : ℕ) ↦ (↑(x.choose (j + 1)) : ℤ)) n) (↑(n.choose j) : ℤ)

Tactic:
simp only [fwdDiff, choose_succ_succ' n j, cast_add, add_sub_cancel_right]

Premises used: fwdDiff, Nat.cast_add, Nat.choose_succ_succ', add_sub_cancel_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
j : ℕ
⊢ Eq (α := ℕ → ℤ) (Δ_[1]^[0] fun (x : ℕ) ↦ (↑(x.choose (0 + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)

Tactic:
simp only [zero_add, iterate_zero, id_eq]

Premises used: Function.iterate_zero, zero_add, id_eq
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
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:
simp only [iterate_succ_apply', add_assoc, add_comm 1 j, IH, fwdDiff_choose]

Premises used: Function.iterate_succ_apply', add_assoc, fwdDiff_choose, add_comm, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
j k : ℕ
zero : ∀ (j : ℕ), Eq (α := ℕ → ℤ) (Δ_[1]^[0] fun (x : ℕ) ↦ (↑(x.choose (0 + j)) : ℤ)) fun (x : ℕ) ↦ (↑(x.choose j) : ℤ)
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) : ℤ)
⊢ Eq (α := ℕ → ℤ) (Δ_[1]^[k] fun (x : ℕ) ↦ (↑(x.choose (k + 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]

Premises used: Function.iterate_succ_apply', add_assoc, Function.iterate_zero, fwdDiff_choose, zero_add, add_comm, Nat.zero, OfNat.ofNat, Nat.succ, id_eq
-- Module: Mathlib.Algebra.Group.ForwardDiff
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 : ℤ)
inr₁ : ∀ (hnm : n < m), 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 : ℤ)

Tactic:
rcases lt_trichotomy m n with hmn | rfl | hnm

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
m n : ℕ
hmn : m < n
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 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)

Tactic:
rcases Nat.exists_eq_add_of_lt hmn with ⟨k, rfl⟩

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
m k : ℕ
hmn : m < m + k + 1
⊢ m + k + 1 = k + 1 + m

Tactic:
ring
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
inl₁₀ : Eq (α := ℤ) (∑ x ∈ range (k + 1), 0) 0
⊢ Eq (α := ℤ) (Δ_[1]^[m + k + 1] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m + k + 1 = m 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]

Premises used: fwdDiff_const, Function.iterate_add_apply, fwdDiff_iter_eq_sum_shift, if_false, smul_zero, Finset.sum_const_zero, LT.lt.ne', Function.iterate_one, Nat.cast_one, Nat.choose_zero_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
m : ℕ
⊢ Eq (α := ℤ) (Δ_[1]^[m] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if m = m then 1 else 0 : ℤ)

Tactic:
simp only [if_true, add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, cast_one]

Premises used: if_true, Nat.cast_one, Nat.choose_zero_right
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
m n : ℕ
hnm : n < m
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 : ℤ)
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose m) : ℤ)) 0 : ℤ) (if n = m then 1 else 0 : ℤ)

Tactic:
rcases Nat.exists_eq_add_of_lt hnm with ⟨k, rfl⟩

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
inr₄ : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ Eq (α := ℤ) (Δ_[1]^[n] (fun (x : ℕ) ↦ (↑(x.choose (n + k + 1)) : ℤ)) 0 : ℤ) (if n = n + k + 1 then 1 else 0 : ℤ)

Tactic:
simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]

Premises used: Nat.choose_zero_succ, add_assoc, if_false, Nat.cast_zero, OfNat.ofNat, fwdDiff_iter_choose, LT.lt.ne
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
M : Type u_3
R : Type u_4
inst : AddCommMonoid M
inst_1 : Ring R
φ : AddChar M R
h 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:
simp
-- Module: Mathlib.Algebra.Group.ForwardDiff
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) (HSub.hSub (α := R) (β := R) ((φ : (a : M) → R) h : R) (1 : R)) ((φ : (a : M) → R) x : R)
⊢ Δ_[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:
simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]

Premises used: Function.iterate_succ_apply', mul_sub, pow_succ, mul_assoc, fwdDiff
-- Module: Mathlib.Algebra.Group.ForwardDiff
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))
succ₃ 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)
⊢ 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:
rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]

Premises used: AddChar.map_add_eq_mul, add_comm, sub_mul, one_mul
-- Module: Mathlib.Algebra.Group.ForwardDiff
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)
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)
⊢ Δ_[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)

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]

Premises used: Function.iterate_succ_apply', mul_sub, pow_succ, mul_assoc, AddChar.map_add_eq_mul, fwdDiff, add_comm, sub_mul, Nat.zero, Nat.succ, one_mul
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
j : ℕ
h : j < 0
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ r ^ j) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
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)
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
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:
simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]

Premises used: fwdDiff, add_pow, mul_comm, nsmul_eq_mul, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Group.ForwardDiff
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)

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]
-- Module: Mathlib.Algebra.Group.ForwardDiff
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)
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
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n + 1] fun (r : R) ↦ r ^ j) 0

Tactic:
rw [iterate_succ_apply, this, fwdDiff_iter_finsetSum]

Premises used: fwdDiff_iter_finsetSum, Function.iterate_succ_apply
-- Module: Mathlib.Algebra.Group.ForwardDiff
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 < j

Tactic:
have := mem_range.1 hi
-- Module: Mathlib.Algebra.Group.ForwardDiff
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_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)
i : ℕ
hi : i ∈ range j
this : i < j
⊢ i < n

Tactic:
lia
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := R → R) 0 0
⊢ Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose i) fun (r : R) ↦ r ^ i) = 0

Tactic:
rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]

Premises used: nsmul_zero, fwdDiff_iter_const_smul
-- Module: Mathlib.Algebra.Group.ForwardDiff
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) (∑ k ∈ range j, Δ_[1]^[n] (HSMul.hSMul (β := (r : R) → R) (j.choose k) fun (r : R) ↦ r ^ k))
    0

Tactic:
exact sum_eq_zero fun i hi ↦ by
      rw [fwdDiff_iter_const_smul, ih (by have := mem_range.1 hi; lia), nsmul_zero]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Algebra.Group.ForwardDiff
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
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
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[n] 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]

Premises used: Finset.sum_eq_zero, fwdDiff_iter_finsetSum, Function.iterate_succ_apply, Nat.zero, Nat.succ
-- Module: Mathlib.Algebra.Group.ForwardDiff
Goal:
R : Type u_3
inst : CommRing R
⊢ Eq.{u_3 + 1} (α := R → R) (Δ_[1]^[0] fun (r : R) ↦ HPow.hPow (β := ℕ) r 0) (↑0! : R → R)

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.ForwardDiff
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)
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)
⊢ 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:
ext x