awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
h : ∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) g : R)
⊢ f = g

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
h₁ h₂ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) g : 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)

Tactic:
rw [coeff_zero_eq_constantCoeff, hc]

Premises used: PowerSeries.coeff_zero_eq_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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 : ℕ
rw 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)
⊢ 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:
rw [hD]
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)

Tactic:
have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
h₁ : ∀ (n : ℕ), Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (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

Premises used: Nat.cast_succ, Nat.succ_ne_zero, PowerSeries.coeff_zero_eq_constantCoeff, mul_comm, nsmul_eq_mul, PowerSeries.coeff_derivative, Nat.zero, Nat.succ, smul_right_inj
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommRing R
f : R⟦X⟧ˣ
h : (↑f⁻¹ : R⟦X⟧) * (↑f : R⟦X⟧) = 1
⊢ (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⟧)

Tactic:
apply Derivation.leibniz_of_mul_eq_one

Premises used: Derivation.leibniz_of_mul_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommRing R
f : R⟦X⟧ˣ
⊢ (↑f⁻¹ : R⟦X⟧) * (↑f : R⟦X⟧) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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⟧)
rw₁ 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⟧)
⊢ (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⟧)

Tactic:
rw [Derivation.leibniz_invOf, smul_eq_mul]

Premises used: smul_eq_mul, Derivation.leibniz_invOf
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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⟧)
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⟧)
⊢ (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

Premises used: PowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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⟧)
rw₅ rw₆ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 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⟧)

Tactic:
rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]

Premises used: pow_two, MulZeroClass.zero_mul, map_zero, neg_zero
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
pos : 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⟧)

Tactic:
suffices f⁻¹ = 0 by
      rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
pos pos₁ pos₂ pos₃ : Eq (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ f⁻¹ = 0

Tactic:
rwa [MvPowerSeries.inv_eq_zero]

Premises used: MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : ¬Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
neg : f⁻¹ * f = 1
⊢ (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:
apply Derivation.leibniz_of_mul_eq_one

Premises used: Derivation.leibniz_of_mul_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : ¬Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ f⁻¹ * f = 1

Tactic:
PowerSeries.inv_mul_cancel (h := h)

Premises used: PowerSeries.inv_mul_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : Field R
f : R⟦X⟧
h : ¬Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ f⁻¹ * f = 1

Tactic:
exact PowerSeries.inv_mul_cancel (h := h)

Premises used: PowerSeries.inv_mul_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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⟧)
rw₃ 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⟧)
⊢ (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⟧)

Tactic:
rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]

Premises used: mul_assoc, Derivation.leibniz_pow, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
p : A[X]
g : A⟦X⟧
hg : HasSubst g
⊢ (d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (subst g (↑p : A⟦X⟧)) =
    HMul.hMul (β := A⟦X⟧) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑p : A⟦X⟧)))
      ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧)

Tactic:
simp [subst_coe hg, derivative_coe, Derivation.comp_aeval_eq (a := g) (derivative A) p,
    smul_eq_mul]

Premises used: PowerSeries.derivative, Derivation.comp_aeval_eq, PowerSeries.subst_coe, PowerSeries.derivative_coe, smul_eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
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)
⊢ (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⟧)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
A : Type u_1
inst : CommRing A
f g : A⟦X⟧
hg : HasSubst g
n : ℕ
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)
⊢ 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

Premises used: HAdd.hAdd, OfNat.ofNat, PowerSeries.HasSubst.eventually_coeff_pow_eq_zero, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
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))
⊢ 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)

Tactic:
rw [coeff_subst' hg, coeff_subst' hg]

Premises used: PowerSeries.coeff_subst'
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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))

Tactic:
finsum_congr fun d ↦ ?_

Premises used: finsum_congr
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
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)
⊢ 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:
refine finsum_congr fun d ↦ ?_

Premises used: finsum_congr
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
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)
⊢ 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

Premises used: lt_or_ge
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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
⊢ d < m + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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
inl 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)
⊢ 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:
rw [coeff_coe_trunc_of_lt (by lia)]

Premises used: PowerSeries.coeff_coe_trunc_of_lt
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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 : 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:
simp [coeff_trunc, hd, hm]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)

Tactic:
have : coeff (n + 1) (f.subst g) = coeff (n + 1) ((↑(trunc (m + 1) f) : A⟦X⟧).subst g) := by
    rw [coeff_subst' hg, coeff_subst' hg]
    refine finsum_congr fun d ↦ ?_
    obtain hd | hd := lt_or_ge d m
    · rw [coeff_coe_trunc_of_lt (by lia)]
    · simp [coeff_trunc, hd, hm]
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
this :
  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)
h :
  Eq.{u_1 + 1} (α := A)
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A)
        ((coeff p.1 : (a : A⟦X⟧) → A)
            (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
          A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A))
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : 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:
rw [coeff_derivative, this, ← coeff_derivative, derivative_subst_coe A _ hg, coeff_mul, coeff_mul]

Premises used: _private.0.PowerSeries.derivative_subst_coe, PowerSeries.coeff_mul, PowerSeries.coeff_derivative
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
this :
  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)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A)
        ((coeff p.1 : (a : A⟦X⟧) → A)
            (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
          A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A))
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A))

Tactic:
Finset.sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_

Premises used: HMul.hMul, PowerSeries.derivative, PowerSeries.subst, PowerSeries.coeff, Prod.fst, HAdd.hAdd, Polynomial.toPowerSeries, OfNat.ofNat, Eq, Prod.snd, DFunLike.coe, Finset.sum_congr, _private.0.PowerSeries.derivative_subst.match_1, rfl, PowerSeries.trunc
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
this :
  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)
h :
  ∀ (x : ℕ × ℕ) (i j : ℕ) (hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n),
    HMul.hMul (α := A) (β := A)
        ((coeff (i, j).1 : (a : A⟦X⟧) → A)
            (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
          A)
        ((coeff (i, j).2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A) =
      HMul.hMul (α := A) (β := A)
        ((coeff (i, j).1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
        ((coeff (i, j).2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A)
        ((coeff p.1 : (a : A⟦X⟧) → A)
            (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
          A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A))
    (∑ p ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (β := A) ((coeff p.1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
        ((coeff p.2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A))

Tactic:
refine Finset.sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
this :
  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)
x : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ instAddMonoid _ n
h :
  Eq (α := A)
    ((coeff (i, j).1 : (a : A⟦X⟧) → A)
        (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
      A)
    ((coeff (i, j).1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
⊢ HMul.hMul (α := A) (β := A)
      ((coeff (i, j).1 : (a : A⟦X⟧) → A)
          (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (↑((trunc (m + 1) : (a : A⟦X⟧) → A[X]) f) : A⟦X⟧))) :
        A)
      ((coeff (i, j).2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A) =
    HMul.hMul (α := A) (β := A)
      ((coeff (i, j).1 : (a : A⟦X⟧) → A) (subst (R := A) g ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) f)) : A)
      ((coeff (i, j).2 : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) g : A⟦X⟧) : A)

Tactic:
congr 1