awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
n : ℤ
x : V
rw :
  Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single (n - (↑k : ℤ) + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single (n - (↑k : ℤ) + (↑k : ℤ) - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) :
      V⟦ℤ⟧)
rw₁ :
  Eq (α := V⸨X⸩) ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) : V⟦ℤ⟧)
    ((single (n - (↑k : ℤ) + (↑k : ℤ) - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose (n - (↑k : ℤ) + (↑k : ℤ)) k • x) :
      V⟦ℤ⟧)
⊢ Eq (α := V⸨X⸩) ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((single n : (a : V) → V⟦ℤ⟧) x) : V⸨X⸩)
    ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose n k • x) : V⟦ℤ⟧)
have rw₂ : Eq (α := V⸨X⸩) ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose n k • x) : V⟦ℤ⟧)
  ((single (n - (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) (Ring.choose n k • x) : V⟦ℤ⟧)
Tactic: rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R l : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) ((k + l).choose k) ((hasseDeriv R (k + l) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have rw : HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R l : (a : V⸨X⸩) → V⸨X⸩) f)) n =
  HSMul.hSMul (β := ℤ → V) ((k + l).choose k) (HahnSeries.coeff ((hasseDeriv R (k + l) : (a : V⸨X⸩) → V⸨X⸩) f)) n
Tactic: rw [coeff_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R l : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    HSMul.hSMul (β := ℤ → V) ((k + l).choose k) (HahnSeries.coeff ((hasseDeriv R (k + l) : (a : V⸨X⸩) → V⸨X⸩) f)) n
have simp : Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
  (k + l).choose k •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw : (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
  (k + l).choose k •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw₁ : (Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l * Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
  (k + l).choose k •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₁ :
  (Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l * Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw₂ : ((k + l).choose l • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) (k + l)) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
  (k + l).choose k •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₁ :
  (Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l * Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₂ :
  ((k + l).choose l • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) (k + l)) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw₃ : ((k + l).choose l • Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l)) •
    f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
  (k + l).choose k •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₁ :
  (Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l * Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₂ :
  ((k + l).choose l • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) (k + l)) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₃ :
  ((k + l).choose l • Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l)) •
      f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw₄ : ((k + l).choose l • Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l)) •
    f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
  (k + l).choose l •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (Ring.choose (n + (↑k : ℤ)) k * Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₁ :
  (Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l * Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₂ :
  ((k + l).choose l • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) (k + l)) • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₃ :
  ((k + l).choose l • Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l)) •
      f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
rw₄ :
  ((k + l).choose l • Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l)) •
      f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
    (k + l).choose l •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
⊢ Ring.choose (n + (↑k : ℤ)) k • Ring.choose (n + (↑k : ℤ) + (↑l : ℤ)) l • f.coeff (n + (↑k : ℤ) + (↑l : ℤ)) =
    (k + l).choose k •
      Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
        f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
have rw₅ : (k + l).choose l •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) •
      f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) =
  (k + l).choose l •
    Ring.choose (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ)) (k + l) • f.coeff (n + HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑l : ℤ))
Tactic: rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k l : ℕ
f : V⸨X⸩
⊢ (hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R l : (a : V⸨X⸩) → V⸨X⸩) f) =
    HSMul.hSMul (β := V⸨X⸩) ((k + l).choose k) ((hasseDeriv R (k + l) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)
have coeff : ∀ (n : ℤ),
  HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R l : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) ((k + l).choose k) ((hasseDeriv R (k + l) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
k : ℕ
f : V⸨X⸩
⊢ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f =
    HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)
have coeff : ∀ (n : ℤ),
  ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff : HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
coeff :
  HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff₁ : HahnSeries.coeff ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f)) n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
coeff :
  HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₁ :
  HahnSeries.coeff ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff₂ : (HSMul.hSMul (β := V⸨X⸩) k.factorial
        ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
    n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
coeff :
  HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₁ :
  HahnSeries.coeff ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₂ :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial
          ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff₃ : (HSMul.hSMul (β := V⸨X⸩) k.factorial
        ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R 1 : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
    n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
coeff :
  HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₁ :
  HahnSeries.coeff ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₂ :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial
          ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₃ :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial
          ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R 1 : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff₄ : (k.factorial • HSMul.hSMul (β := V⸨X⸩) ((k + 1).choose k) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff
    n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
k : ℕ
ih :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
f : V⸨X⸩
coeff :
  HahnSeries.coeff (((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ∘ (⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)) f) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₁ :
  HahnSeries.coeff ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₂ :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial
          ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₃ :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial
          ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) ((hasseDeriv R 1 : (a : V⸨X⸩) → V⸨X⸩) f) : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
coeff₄ :
  (k.factorial • HSMul.hSMul (β := V⸨X⸩) ((k + 1).choose k) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff
      n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k + 1] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
have coeff₅ : (k.factorial • HSMul.hSMul (β := V⸨X⸩) ((k + 1).choose 1) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff
    n =
  (HSMul.hSMul (β := V⸨X⸩) (k + 1).factorial ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]