awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
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
m : ℤ
h : m = n
⊢ HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
      (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
    HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.LaurentSeries
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
m : ℤ
h : ¬m = n
⊢ m + (↑k : ℤ) ≠ n + (↑k : ℤ)

Tactic:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
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
m : ℤ
h : ¬m = n
⊢ HSMul.hSMul (β := V) (Ring.choose (m + (↑k : ℤ)) k)
      (HahnSeries.coeff ((single (n + (↑k : ℤ)) : (a : V) → V⟦ℤ⟧) x) (m + (↑k : ℤ))) =
    HahnSeries.coeff ((single n : (a : V) → V⟦ℤ⟧) (Ring.choose (n + (↑k : ℤ)) k • x)) m

Tactic:
simp [h, show m + k ≠ n + k by lia]
-- Module: Mathlib.RingTheory.LaurentSeries
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⟦ℤ⟧)
rw₂ 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⟦ℤ⟧)
⊢ 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⟦ℤ⟧)

Tactic:
rw [← Int.sub_add_cancel n k, hasseDeriv_single_add, Int.sub_add_cancel n k]

Premises used: Nat.cast, Int.sub_add_cancel, LaurentSeries.hasseDeriv_single_add
-- Module: Mathlib.RingTheory.LaurentSeries
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 :
  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
⊢ 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:
rw [coeff_nsmul]

Premises used: HahnSeries.coeff_nsmul
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ
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 : ℤ))
⊢ 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:
simp only [hasseDeriv_coeff, Pi.smul_apply, Nat.cast_add]

Premises used: LaurentSeries.hasseDeriv_coeff, Nat.cast_add, Pi.smul_apply
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ))
rw₅ 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 : ℤ))

Tactic:
rw [smul_smul, mul_comm, ← Ring.choose_add_smul_choose (n + k), add_assoc, Nat.choose_symm_add,
    smul_assoc]

Premises used: smul_assoc, add_assoc, smul_smul, Nat.cast, Nat.choose_symm_add, Ring.choose_add_smul_choose, HAdd.hAdd, mul_comm
-- Module: Mathlib.RingTheory.LaurentSeries
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⸩
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
⊢ (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⸩)

Tactic:
ext n
-- Module: Mathlib.RingTheory.LaurentSeries
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

Tactic:
simp [hasseDeriv_comp_coeff k l f n]

Premises used: LaurentSeries.hasseDeriv_comp_coeff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V⸨X⸩
⊢ Eq (α := V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩) ((hasseDeriv R 1 : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
f : V⸨X⸩
⊢ Eq (α := V⸨X⸩) ((derivative R : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩) ((hasseDeriv R 1 : (a : V⸨X⸩) → V⸨X⸩) f : V⸨X⸩)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
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⸩
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
⊢ (⇑(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⸩)

Tactic:
ext n
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module R V
n : ℤ
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:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
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
coeff₈ 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
⊢ ((⇑(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:
rw [Function.iterate_succ, Function.comp_apply, ih, derivative_apply, hasseDeriv_comp,
      Nat.choose_symm_add, Nat.choose_one_right, Nat.factorial, mul_nsmul]

Premises used: Function.iterate_succ, LaurentSeries.derivative_apply, Nat.choose_one_right, mul_nsmul, Nat.choose_symm_add, LaurentSeries.hasseDeriv_comp, Nat.factorial, Function.comp_apply
-- Module: Mathlib.RingTheory.LaurentSeries
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
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
⊢ ((⇑(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:
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]

Premises used: Function.iterate_succ, LaurentSeries.derivative_apply, Nat.choose_one_right, mul_nsmul, Nat.choose_symm_add, LaurentSeries.hasseDeriv_comp, Nat.factorial, Function.comp_apply
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ))
rw₅ 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 : ℤ))

Tactic:
rw [derivative_iterate, coeff_nsmul, Pi.smul_apply, hasseDeriv_coeff,
    Ring.descPochhammer_eq_factorial_smul_choose, smul_assoc]

Premises used: smul_assoc, LaurentSeries.hasseDeriv_coeff, LaurentSeries.derivative_iterate, Ring.descPochhammer_eq_factorial_smul_choose, HahnSeries.coeff_nsmul, Pi.smul_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⟦X⟧
n : ℕ
rw rw₁ : Eq (α := R) ((PowerSeries.coeff n : (a : R⟦X⟧) → R) x : R) ((PowerSeries.coeff n : (a : R⟦X⟧) → R) x : R)
⊢ 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)

Tactic:
rw [ofPowerSeries_apply_coeff]

Premises used: HahnSeries.ofPowerSeries_apply_coeff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℕ
⊢ (PowerSeries.coeff n : (a : R⟦X⟧) → R) x.powerSeriesPart = x.coeff (order x + (↑n : ℤ))

Tactic:
PowerSeries.coeff_mk _ _

Premises used: PowerSeries.coeff_mk, LaurentSeries.powerSeriesPart
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
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)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (powerSeriesPart 0) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
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:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
mp : x.powerSeriesPart = 0 → x = 0
mpr : x = 0 → x.powerSeriesPart = 0
⊢ x.powerSeriesPart = 0 ↔ x = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
mp : x ≠ 0 → x.powerSeriesPart ≠ 0
⊢ x.powerSeriesPart = 0 → x = 0

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
h : ¬x = 0
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)
⊢ ¬x.powerSeriesPart = 0

Tactic:
rw [PowerSeries.ext_iff, not_forall]

Premises used: PowerSeries.ext_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
h : ¬x = 0
h₁ :
  ¬Eq (α := R) ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) x.powerSeriesPart : R)
      ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) 0 : R)
⊢ ∃ (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:
use 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬Eq (α := R) ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) x.powerSeriesPart : R)
      ((PowerSeries.coeff 0 : (a : R⟦X⟧) → R) 0 : R)

Tactic:
simpa
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (powerSeriesPart 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
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
⊢ 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

Tactic:
ext n
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
coeff :
  HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.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:
rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]

Premises used: HahnSeries.order, HahnSeries.coeff_single_mul_add, sub_add_cancel, one_mul
-- Module: Mathlib.RingTheory.LaurentSeries
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
neg :
  ∀ (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

Tactic:
by_cases h : x.order ≤ n

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
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
pos₄ pos₅ : x.coeff n = x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (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]

Premises used: sub_nonneg_of_le, LaurentSeries.powerSeriesPart_coeff, add_sub_cancel, Int.eq_natAbs_of_nonneg, LaurentSeries.coeff_coe_powerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
neg : 0 = x.coeff n
neg₁ :
  n - order x ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n

Tactic:
rw [ofPowerSeries_apply, embDomain_notin_range]

Premises used: HahnSeries.embDomain_notin_range, HahnSeries.ofPowerSeries_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
neg : ∀ (h : 0 ≠ x.coeff n), order x ≤ n
⊢ 0 = x.coeff n

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : 0 ≠ x.coeff n
⊢ order x ≤ n

Tactic:
order_le_of_coeff_ne_zero h.symm

Premises used: Ne.symm, HahnSeries.order_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : 0 ≠ x.coeff n
⊢ order x ≤ n

Tactic:
exact order_le_of_coeff_ne_zero h.symm

Premises used: Ne.symm, HahnSeries.order_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
neg :
  ∀
    (h :
      Membership.mem (γ := Set ℤ)
        (Set.range (ι := ℕ)
          (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
                { toFun := Nat.cast, inj' := ⋯ } ⋯) :
            (a : ℕ) → ℤ))
        (n - order x)),
    order x ≤ n
⊢ n - order x ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h :
  Membership.mem (γ := Set ℤ)
    (Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ))
    (n - order x)
⊢ ∃ (y : ℕ), (↑y : ℤ) = n - order x

Tactic:
simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h

Premises used: Set.mem_range, Function.Embedding.coeFn_mk, RelEmbedding.coe_mk
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ∃ (y : ℕ), (↑y : ℤ) = n - order x
⊢ order x ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    (single (-order x) : (a : R) → R⟦ℤ⟧) 1 * x

Tactic:
Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)

Premises used: LaurentSeries.single_order_mul_powerSeriesPart, congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
refine :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    (single (-order x) : (a : R) → R⟦ℤ⟧) 1 *
      HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (order x) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
        (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    (single (-order x) : (a : R) → R⟦ℤ⟧) 1 * x

Tactic:
refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)

Premises used: LaurentSeries.single_order_mul_powerSeriesPart, congr, rfl, Eq.trans