awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
have h₇ : ∀ (equ : 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)
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 : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)
have h : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) f : R) ((coeff 0 : (a : R⟦X⟧) → R) g : R)
Tactic: cases n with
  | zero =>
    rw [coeff_zero_eq_constantCoeff, hc]
  | succ n =>
    have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
    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: 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)
n : ℕ
h : Eq (α := R) ((coeff 0 : (a : R⟦X⟧) → R) f : R) ((coeff 0 : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)
have h₁ : ∀ (n : ℕ), Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
Tactic: cases n with
  | zero =>
    rw [coeff_zero_eq_constantCoeff, hc]
  | succ n =>
    have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
    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: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R⟦X⟧ˣ
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) (↑f⁻¹ : R⟦X⟧) =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (↑f⁻¹ : R⟦X⟧) 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) (↑f : R⟦X⟧) : R⟦X⟧)
have h : (↑f⁻¹ : R⟦X⟧) * (↑f : R⟦X⟧) = 1
Tactic: apply Derivation.leibniz_of_mul_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R⟦X⟧
inst_1 : Invertible f
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) 2)
      ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw : HSMul.hSMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne f _) 2)
    ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) =
  HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) 2)
    ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [Derivation.leibniz_invOf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R⟦X⟧
inst_1 : Invertible f
rw :
  HSMul.hSMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne f _) 2)
      ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) 2)
      ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) 2)
      ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₁ : HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne f _) 2)
    ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) =
  HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) (@Invertible.invOf _ MvPowerSeries.instMul MvPowerSeries.instOne f _) 2)
    ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [Derivation.leibniz_invOf, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have pos : ∀ (h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)),
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: by_cases h : constantCoeff f = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
pos :
  ∀ (h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)),
    (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
      HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have neg : ∀ (h : ¬Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)),
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: by_cases h : constantCoeff f = 0
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw : (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
  HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
rw :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₁ : (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
  HMul.hMul (β := R⟦X⟧) (-HMul.hMul (α := R⟦X⟧) 0 0) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
rw :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₁ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HMul.hMul (α := R⟦X⟧) 0 0) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₂ : (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (-0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
rw :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₁ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HMul.hMul (α := R⟦X⟧) 0 0) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₂ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (-0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₃ : (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
rw :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₁ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HMul.hMul (α := R⟦X⟧) 0 0) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₂ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (-0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₃ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₄ : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 : R⟦X⟧) (0 : R⟦X⟧)
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this : f⁻¹ = 0
rw :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (α := R⟦X⟧) (β := ℕ) 0 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₁ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 =
    HMul.hMul (β := R⟦X⟧) (-HMul.hMul (α := R⟦X⟧) 0 0) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₂ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (-0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₃ :
  (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 = HMul.hMul (α := R⟦X⟧) (β := R⟦X⟧) (0 : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
rw₄ : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) 0 : R⟦X⟧) (0 : R⟦X⟧)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have rw₅ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 0
Tactic: rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have pos : f⁻¹ = 0
Tactic: suffices f⁻¹ = 0 by
      rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ f⁻¹ = 0
have pos : Eq (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
Tactic: rwa [MvPowerSeries.inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : ¬Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ (d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f⁻¹ =
    HMul.hMul (β := R⟦X⟧) (-HPow.hPow (β := ℕ) f⁻¹ 2) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
have neg : f⁻¹ * f = 1
Tactic: apply Derivation.leibniz_of_mul_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommSemiring A
g : A⟦X⟧
n : ℕ
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (g ^ n) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
have rw : n • HSMul.hSMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
  HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
Tactic: rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommSemiring A
g : A⟦X⟧
n : ℕ
rw :
  n • HSMul.hSMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (g ^ n) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
have rw₁ : n • HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
  HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
Tactic: rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommSemiring A
g : A⟦X⟧
n : ℕ
rw :
  n • HSMul.hSMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
rw₁ :
  n • HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (g ^ n) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
have rw₂ : (↑n : A⟦X⟧) * HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
  HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
Tactic: rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommSemiring A
g : A⟦X⟧
n : ℕ
rw :
  n • HSMul.hSMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
rw₁ :
  n • HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
rw₂ :
  (↑n : A⟦X⟧) * HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (g ^ n) =
    HMul.hMul (β := A⟦X⟧) ((↑n : A⟦X⟧) * g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
have rw₃ : (↑n : A⟦X⟧) * HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) =
  (↑n : A⟦X⟧) * HMul.hMul (β := A⟦X⟧) (g ^ (n - 1)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
Tactic: rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (subst g f) =
    HMul.hMul (β := A⟦X⟧) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (subst g f) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (β := A⟦X⟧) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f))
          ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)) :
      A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (subst g f) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (β := A⟦X⟧) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f))
          ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)) :
      A)
have h : ∀ (m : ℕ) (hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (subst g f) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A)
        (HMul.hMul (β := A⟦X⟧) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f))
          ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)) :
      A)
Tactic: obtain ⟨m, hm⟩ := (hg.eventually_coeff_pow_eq_zero (n + 1)).exists_forall_of_atTop
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst g f) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (subst (R := A) g (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧)) : A)
have rw : Eq.{u_1 + 1} (α := A)
  (∑ᶠ (d : ℕ),
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A))
  (∑ᶠ (d : ℕ),
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A))
Tactic: rw [coeff_subst' hg, coeff_subst' hg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
        ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A))
have refine : ∀ (d : ℕ),
  HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
Tactic: refine finsum_congr fun d ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
d : ℕ
⊢ HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
have inl : ∀ (hd : d < m),
  HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
Tactic: obtain hd | hd := lt_or_ge d m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
d : ℕ
inl :
  ∀ (hd : d < m),
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
      HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
        ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
⊢ HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
have inr : ∀ (hd : m ≤ d),
  HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
Tactic: obtain hd | hd := lt_or_ge d m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ b ≥ m, ∀ n' ≤ n + 1, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (g ^ b) : A) (0 : A)
d : ℕ
hd : d < m
⊢ HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
    HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
have inl : HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A) =
  HSMul.hSMul (α := A) (β := A) ((coeff d : (a : A⟦X⟧) → A) f : A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (g ^ d) : A)
Tactic: rw [coeff_coe_trunc_of_lt (by lia)]