awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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
⊢ (r • f).derivativeFun = r • f.derivativeFun
have 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
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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
⊢ (r • f).derivativeFun = r • f.derivativeFun
have 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
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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
⊢ (r • f).derivativeFun = r • f.derivativeFun
have 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
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) X : R⟦X⟧) (1 : R⟦X⟧)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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)
have h : (if n = 0 then HAdd.hAdd (α := R) (↑n : R) 1 else 0) = if n = 0 then 1 else 0
Tactic: simp only [coeff_derivative, coeff_one, coeff_X, boole_mul, add_eq_right]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ (if n = 0 then HAdd.hAdd (α := R) (↑n : R) 1 else 0) = if n = 0 then 1 else 0
have pos : n = 0 → HAdd.hAdd (α := R) (↑n : R) 1 = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
pos : n = 0 → HAdd.hAdd (α := R) (↑n : R) 1 = 1
⊢ (if n = 0 then HAdd.hAdd (α := R) (↑n : R) 1 else 0) = if n = 0 then 1 else 0
have neg : ¬n = 0 → Eq.{u_1 + 1} (α := R) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ 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])
have 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])
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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])
⊢ 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])
have 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])
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
⊢ f = g
have h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) f : R) ((coeff 0 : (a : R⟦X⟧) → R) g : R)
have h₁ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) g : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
Tactic: rw [coeff_zero_eq_constantCoeff, hc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
have rw : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
Tactic: rw [hD]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have equ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
Tactic: have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h : ∀
  (equ :
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
      (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₁ : ∀
  (equ :
    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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₂ : ∀
  (equ :
    HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₂ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₃ : ∀
  (equ :
    HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₂ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₃ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₄ : ∀
  (equ :
    HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₂ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₃ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₄ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₅ : ∀
  (equ :
    HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
      HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₂ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₃ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₄ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₅ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₆ : ∀
  (equ :
    HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
  Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
Cleared hypotheses: equ