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
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
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
⊢ ((⇑(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) ((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
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
coeff₆ :
  (k.factorial • HSMul.hSMul (β := V⸨X⸩) (k + 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
⊢ ((⇑(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) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
  (HSMul.hSMul (β := V⸨X⸩) (k.succ * k.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
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
coeff₆ :
  (k.factorial • HSMul.hSMul (β := V⸨X⸩) (k + 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
coeff₇ :
  (k.factorial • HSMul.hSMul (β := V⸨X⸩) (k + 1) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (k.succ * k.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) ((hasseDeriv R (k + 1) : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
  (k.factorial • HSMul.hSMul (β := V⸨X⸩) k.succ ((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
k : ℕ
f : V⸨X⸩
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
have coeff : ∀ (f : V⸨X⸩),
  ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[0] f).coeff n =
    (HSMul.hSMul (β := V⸨X⸩) (Nat.factorial 0) ((hasseDeriv R 0 : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n
Tactic: induction k generalizing f with
  | zero => simp
  | succ k ih =>
    rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
Cleared hypotheses: k, f
-- 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⸩
n : ℤ
coeff :
  ∀ (f : V⸨X⸩),
    ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[0] f).coeff n =
      (HSMul.hSMul (β := V⸨X⸩) (Nat.factorial 0) ((hasseDeriv R 0 : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).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
have coeff₁ : ∀ (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
Tactic: induction k generalizing f with
  | zero => simp
  | succ k ih =>
    rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]
Cleared hypotheses: k, f
-- 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⸩
n : ℤ
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw : (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
  smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, 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 : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw₁ : HSMul.hSMul (β := ℤ → V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f)) n =
  smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, 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 : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₁ :
  HSMul.hSMul (β := ℤ → V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw₂ : HSMul.hSMul (β := V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f) n) =
  smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, 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 : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₁ :
  HSMul.hSMul (β := ℤ → V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₂ :
  HSMul.hSMul (β := V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f) n) =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw₃ : k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
  smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, 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 : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₁ :
  HSMul.hSMul (β := ℤ → V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₂ :
  HSMul.hSMul (β := V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f) n) =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₃ :
  k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw₄ : k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
  (k.factorial • Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, 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 : ℕ
f : V⸨X⸩
n : ℤ
rw :
  (HSMul.hSMul (β := V⸨X⸩) k.factorial ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₁ :
  HSMul.hSMul (β := ℤ → V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f)) n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₂ :
  HSMul.hSMul (β := V) k.factorial (HahnSeries.coeff ((hasseDeriv R k : (a : V⸨X⸩) → V⸨X⸩) f) n) =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₃ :
  k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
rw₄ :
  k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
    (k.factorial • Ring.choose (n + (↑k : ℤ)) k) • f.coeff (n + (↑k : ℤ))
⊢ ((⇑(derivative R) : (a : V⸨X⸩) → V⸨X⸩)^[k] f).coeff n =
    smeval (descPochhammer ℤ k) (n + (↑k : ℤ)) • f.coeff (n + (↑k : ℤ))
have rw₅ : k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ)) =
  k.factorial • Ring.choose (n + (↑k : ℤ)) k • f.coeff (n + (↑k : ℤ))
Tactic: rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⟦X⟧
n : ℕ
⊢ Eq (α := R) (HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x) (↑n : ℤ) : R)
    ((PowerSeries.coeff n : (a : R⟦X⟧) → R) x : R)
have rw : Eq (α := R) ((PowerSeries.coeff n : (a : R⟦X⟧) → R) x : R) ((PowerSeries.coeff n : (a : R⟦X⟧) → R) x : R)
Tactic: rw [ofPowerSeries_apply_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (powerSeriesPart 0) 0
have h : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R) ((PowerSeries.coeff n : (a : R⟦X⟧) → R) (powerSeriesPart 0) : R)
    ((PowerSeries.coeff n : (a : R⟦X⟧) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 ↔ x = 0
have mp : x.powerSeriesPart = 0 → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
mp : x.powerSeriesPart = 0 → x = 0
⊢ x.powerSeriesPart = 0 ↔ x = 0
have mpr : x = 0 → x.powerSeriesPart = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0
have mp : x ≠ 0 → x.powerSeriesPart ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬x.powerSeriesPart = 0
have mp : ∃ (x_1 : ℕ),
  ¬Eq (α := R) ((PowerSeries.coeff x_1 : (a : R⟦X⟧) → R) x.powerSeriesPart : R)
      ((PowerSeries.coeff x_1 : (a : R⟦X⟧) → R) 0 : R)
Tactic: rw [PowerSeries.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ∃ (x_1 : ℕ),
    ¬Eq (α := R) ((PowerSeries.coeff x_1 : (a : R⟦X⟧) → R) x.powerSeriesPart : R)
        ((PowerSeries.coeff x_1 : (a : R⟦X⟧) → R) 0 : R)
have h₁ : ¬Eq (α := R) ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) x.powerSeriesPart : R)
    ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) 0 : R)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (order x) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧) =
    x
have coeff : ∀ (n : ℤ),
  (HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (order x) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
          (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)).coeff
      n =
    x.coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
⊢ (HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (order x) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
          (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)).coeff
      n =
    x.coeff n
have coeff : HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) = x.coeff n
Tactic: rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos : ∀ (h : order x ≤ n),
  HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
Tactic: by_cases h : x.order ≤ n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
pos :
  ∀ (h : order x ≤ n),
    HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
      x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have neg : ∀ (h : ¬order x ≤ n),
  HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
Tactic: by_cases h : x.order ≤ n
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos : HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart)
    (↑(n - order x).natAbs : ℤ) =
  x.coeff n
Tactic: rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
pos :
  HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart)
      (↑(n - order x).natAbs : ℤ) =
    x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos₁ : (PowerSeries.coeff (n - order x).natAbs : (a : R⟦X⟧) → R) x.powerSeriesPart = x.coeff n
Tactic: rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
pos :
  HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart)
      (↑(n - order x).natAbs : ℤ) =
    x.coeff n
pos₁ : (PowerSeries.coeff (n - order x).natAbs : (a : R⟦X⟧) → R) x.powerSeriesPart = x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos₂ : x.coeff (order x + (↑(n - order x).natAbs : ℤ)) = x.coeff n
Tactic: rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
pos :
  HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart)
      (↑(n - order x).natAbs : ℤ) =
    x.coeff n
pos₁ : (PowerSeries.coeff (n - order x).natAbs : (a : R⟦X⟧) → R) x.powerSeriesPart = x.coeff n
pos₂ : x.coeff (order x + (↑(n - order x).natAbs : ℤ)) = x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos₃ : x.coeff (order x + (n - order x)) = x.coeff n
Tactic: rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : order x ≤ n
pos :
  HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart)
      (↑(n - order x).natAbs : ℤ) =
    x.coeff n
pos₁ : (PowerSeries.coeff (n - order x).natAbs : (a : R⟦X⟧) → R) x.powerSeriesPart = x.coeff n
pos₂ : x.coeff (order x + (↑(n - order x).natAbs : ℤ)) = x.coeff n
pos₃ : x.coeff (order x + (n - order x)) = x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have pos₄ : x.coeff n = x.coeff n
Tactic: rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries,
      powerSeriesPart_coeff, ← Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h),
      add_sub_cancel]