awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R :=
  (AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) : (a : R[X]) → MvPolynomial PUnit.{1} R) f
⊢ f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g

Tactic:
have : f = MvPolynomial.uniqueAlgEquiv R PUnit g := by simp only [g, AlgEquiv.apply_symm_apply]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R :=
  (AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) : (a : R[X]) → MvPolynomial PUnit.{1} R) f
this : f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g
rw :
  (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g) : PowerSeries R) =
    (↑g : MvPowerSeries PUnit.{1} R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := PowerSeries R)
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g) : PowerSeries R)
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g) : PowerSeries R)
⊢ (↑f : PowerSeries R) = (↑g : MvPowerSeries PUnit.{1} R)

Tactic:
rw [this, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv]

Premises used: MvPolynomial.toMvPowerSeries_pUnitAlgEquiv
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
φ ψ : R[X]
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ OneHom.toFun (M := R[X])
      (↑(↑(RingHom.comp (PowerSeries.map (algebraMap R A)) ringHom) : R[X] →* PowerSeries A) :
        OneHom R[X] (PowerSeries A))
      ((algebraMap R R[X] : (a : R) → R[X]) r) =
    (algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r

Tactic:
simp [PowerSeries.algebraMap_apply]

Premises used: PowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
φ : R[X]
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_2 + 1} (α := PowerSeries A) ((algHom A : (a : R[X]) → PowerSeries A) φ : PowerSeries A)
    (((PowerSeries.map (algebraMap R A) : RingHom.{u_1, u_2} (PowerSeries R) (PowerSeries A)) :
          (a : PowerSeries R) → PowerSeries A)
        (↑φ : PowerSeries R) :
      PowerSeries A)

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
⊢ (↑(-p) : PowerSeries R) = -(↑p : PowerSeries R)

Tactic:
coeToPowerSeries.ringHom.map_neg p

Premises used: RingHom.map_neg, Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
⊢ (↑(p - q) : PowerSeries R) = (↑p : PowerSeries R) - (↑q : PowerSeries R)

Tactic:
coeToPowerSeries.ringHom.map_sub p q

Premises used: RingHom.map_sub, Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : R[X]
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((algebraMap R[X] A⟦X⟧ : (a : R[X]) → A⟦X⟧) p : A⟦X⟧)
    (((map (algebraMap R A) : RingHom.{u_1, u_2} R⟦X⟧ A⟦X⟧) : (a : R⟦X⟧) → A⟦X⟧) (↑p : R⟦X⟧) : A⟦X⟧)

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
f : R⟦X⟧
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((algebraMap R⟦X⟧ A⟦X⟧ : (a : R⟦X⟧) → A⟦X⟧) f : A⟦X⟧)
    (((map (algebraMap R A) : RingHom.{u_1, u_2} R⟦X⟧ A⟦X⟧) : (a : R⟦X⟧) → A⟦X⟧) f : A⟦X⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
rw :
  (coeff n : (a : R⟦X⟧) → R)
      (mk fun (n : ℕ) ↦ HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1)) =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1)
rw₁ rw₂ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1)
⊢ (coeff n : (a : R⟦X⟧) → R) f.derivativeFun =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
rw [derivativeFun, coeff_mk]

Premises used: PowerSeries.coeff_mk, PowerSeries.derivativeFun
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑f : R⟦X⟧).derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧) : R)
⊢ (↑f : R⟦X⟧).derivativeFun = (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
h₁ :
  f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
h₂ : f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = Polynomial.coeff ((derivative : (a : R[X]) → R[X]) f) n
h₃ h₄ : f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑f : R⟦X⟧).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧) : R)

Tactic:
rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]

Premises used: Polynomial.coeff_derivative, PowerSeries.coeff_derivativeFun, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
⊢ (f + g).derivativeFun = f.derivativeFun + g.derivativeFun

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₁ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₂ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f.derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
h₃ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (β := R) (HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1))
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
h₄ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1)
h₅ h₆ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)

Tactic:
rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]

Premises used: add_mul, PowerSeries.coeff_derivativeFun, map_add
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
r : R
h :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
      ((coeff n : (a : R⟦X⟧) → R) 0 : R)
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
r : R
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) 0
h₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = (coeff n : (a : R⟦X⟧) → R) 0
h₂ : Eq.{u_1 + 1} (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)
h₃ h₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)

Tactic:
rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]

Premises used: MulZeroClass.zero_mul, PowerSeries.coeff_derivativeFun, LinearMap.map_zero, PowerSeries.coeff_succ_C, PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
a :
  ∀ (d : ℕ),
    Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun) d)
      (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun : R[X])
    ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) : R[X])

Tactic:
ext d
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
a :
  Eq (α := R) (if d < n then (coeff d : (a : R⟦X⟧) → R) f.derivativeFun else 0 : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun) d)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)

Tactic:
rw [coeff_trunc]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
pos :
  ∀ (h : d < n),
    Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
      (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
neg :
  ∀ (h : ¬d < n),
    Eq.{u_1 + 1} (α := R) 0
      (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
⊢ Eq (α := R) (if d < n then (coeff d : (a : R⟦X⟧) → R) f.derivativeFun else 0 : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ d + 1 < n + 1

Tactic:
have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
pos :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d
pos₁ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
pos₂ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
      (HAdd.hAdd (α := R) (↑d : R) 1)
pos₃ pos₄ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1)
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)

Tactic:
rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]

Premises used: Polynomial.coeff_derivative, PowerSeries.coeff_trunc, PowerSeries.coeff_derivativeFun, if_pos
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h rwa rwa₁ rwa₂ rwa₃ : ¬d < n
⊢ ¬d + 1 < n + 1

Tactic:
rwa [succ_lt_succ_iff]

Premises used: Nat.succ_lt_succ_iff
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ ¬d + 1 < n + 1

Tactic:
have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
neg : 0 = Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
neg₁ :
  0 =
    HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
      (HAdd.hAdd (α := R) (↑d : R) 1)
neg₂ : 0 = 0 * HAdd.hAdd (α := R) (↑d : R) 1
neg₃ neg₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)

Tactic:
rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]

Premises used: Polynomial.coeff_derivative, PowerSeries.coeff_trunc, MulZeroClass.zero_mul, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
rw :
  (↑(f * g) : R⟦X⟧).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₁ :
  (↑((derivative : (a : R[X]) → R[X]) (f * g)) : R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₂ :
  (↑(HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
          HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) :
      R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₃ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) :
      R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₄ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₅ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₆ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : R⟦X⟧)
rw₇ rw₈ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : R⟦X⟧)
⊢ ((↑f : R⟦X⟧) * (↑g : R⟦X⟧)).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)

Tactic:
rw [← coe_mul, derivativeFun_coe, derivative_mul,
    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]

Premises used: Polynomial.derivative_mul, Polynomial.coe_add, PowerSeries.derivativeFun_coe, add_comm, Polynomial.coe_mul, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
⊢ (f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
⊢ n < n + 1

Tactic:
have h₁ : n < n + 1 := lt_succ_self n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
⊢ n < n + 1 + 1

Tactic:
have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun ((C : (a : R) → R⟦X⟧) 1)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 0
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun 1) 0

Tactic:
rw [← map_one C, derivativeFun_C (1 : R)]

Premises used: PowerSeries.derivativeFun_C, PowerSeries.C, map_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R⟦X⟧
rw : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun = r • f.derivativeFun
rw₁ :
  (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₂ :
  HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun +
      HSMul.hSMul (β := R⟦X⟧) f (derivativeFun ((C : (a : R) → R⟦X⟧) r)) =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₃ :
  HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun + HSMul.hSMul (β := R⟦X⟧) f 0 =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₄ :
  HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun + 0 =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₅ :
  HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₆ rw₇ :
  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
⊢ (r • f).derivativeFun = r • f.derivativeFun

Tactic:
rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]

Premises used: smul_zero, PowerSeries.derivativeFun_C, smul_eq_mul, add_zero, PowerSeries.smul_eq_C_mul, PowerSeries.derivativeFun_mul
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R⟦X⟧) (0 : R⟦X⟧)

Tactic:
derivativeFun_C r

Premises used: PowerSeries.derivativeFun_C, PowerSeries.mk, PowerSeries.derivativeFun
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1)

Tactic:
coeff_derivativeFun f n

Premises used: PowerSeries.coeff_derivativeFun, PowerSeries.mk, PowerSeries.derivativeFun
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) (↑f : R⟦X⟧) : R⟦X⟧)
    ((↑((Polynomial.derivative : (a : R[X]) → R[X]) f) : R⟦X⟧) : R⟦X⟧)

Tactic:
derivativeFun_coe f

Premises used: PowerSeries.derivativeFun_coe, PowerSeries.mk, PowerSeries.derivativeFun
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) X : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) 1 : R)
⊢ Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) X : R⟦X⟧) (1 : R⟦X⟧)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
h : (if n = 0 then HAdd.hAdd (α := R) (↑n : R) 1 else 0) = if n = 0 then 1 else 0
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) X : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) 1 : R)

Tactic:
simp only [coeff_derivative, coeff_one, coeff_X, boole_mul, add_eq_right]

Premises used: PowerSeries.coeff_X, PowerSeries.coeff_one, add_eq_right, PowerSeries.coeff_derivative, boole_mul
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
pos : n = 0 → HAdd.hAdd (α := R) (↑n : R) 1 = 1
neg : ¬n = 0 → Eq.{u_1 + 1} (α := R) 0 0
⊢ (if n = 0 then HAdd.hAdd (α := R) (↑n : R) 1 else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
h : n = 0
⊢ HAdd.hAdd (α := R) (↑n : R) 1 = 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
    ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) : R[X])

Tactic:
trunc_derivativeFun ..

Premises used: PowerSeries.mk, PowerSeries.trunc_derivativeFun, PowerSeries.derivativeFun
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
zero :
  Eq (α := R[X]) ((trunc (HSub.hSub (α := ℕ) 0 1) : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
    ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc 0 : (a : R⟦X⟧) → R[X]) f) : R[X])
succ :
  ∀ (n : ℕ),
    Eq (α := R[X]) ((trunc (n + 1 - 1) : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
      ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) : R[X])
⊢ Eq (α := R[X]) ((trunc (n - 1) : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
    ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f) : R[X])

Tactic:
cases n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc (HSub.hSub (α := ℕ) 0 1) : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
    ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc 0 : (a : R⟦X⟧) → R[X]) f) : R[X])

Tactic:
simp [trunc_derivative]

Premises used: PowerSeries.trunc_derivative
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R[X]) ((trunc (n + 1 - 1) : (a : R⟦X⟧) → R[X]) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f) : R[X])
    ((Polynomial.derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) : R[X])

Tactic:
simp [trunc_derivative]

Premises used: PowerSeries.trunc_derivative