awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ eval₂ PowerSeries.C PowerSeries.X φ = (↑(eval₂ C X φ) : PowerSeries R)
have rw : Eq.{u_1 + 1} (α := PowerSeries R)
  (∑ i ∈ Finset.range (φ.natDegree + 1),
    HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff i) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X i))
  (∑ x ∈ Finset.range (φ.natDegree + 1),
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x)))
Tactic: rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ Eq.{u_1 + 1} (α := PowerSeries R)
    (∑ i ∈ Finset.range (φ.natDegree + 1),
      HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff i) : PowerSeries R)
        (HPow.hPow (α := PowerSeries R) PowerSeries.X i))
    (∑ x ∈ Finset.range (φ.natDegree + 1),
      (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x)))
have apply : ∀ x ∈ Finset.range (φ.natDegree + 1),
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
    ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) : PowerSeries R)
    ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
rw :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw₁ : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  HMul.hMul (α := PowerSeries R)
    ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x)
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
rw :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
rw₁ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      (HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x)
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw₂ : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) *
    HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
rw :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
rw₁ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      (HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x)
rw₂ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) *
      HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw₃ : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) * HPow.hPow (α := PowerSeries R) (↑X : PowerSeries R) x
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
rw :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
rw₁ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      (HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x)
rw₂ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) *
      HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x
rw₃ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) * HPow.hPow (α := PowerSeries R) (↑X : PowerSeries R) x
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw₄ : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) (↑X : PowerSeries R) x)
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
x : ℕ
h : x ∈ Finset.range (φ.natDegree + 1)
rw :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) (β := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) (HPow.hPow (α := R[X]) X x) : PowerSeries R)
rw₁ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R)
      ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) :
        PowerSeries R)
      (HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x)
rw₂ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) *
      HPow.hPow (α := PowerSeries R) ((coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R) X : PowerSeries R) x
rw₃ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (↑((C : (a : R) → R[X]) (φ.coeff x)) : PowerSeries R) * HPow.hPow (α := PowerSeries R) (↑X : PowerSeries R) x
rw₄ :
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) (↑X : PowerSeries R) x)
⊢ HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
      (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
    (coeToPowerSeries.ringHom : (a : R[X]) → PowerSeries R)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (φ.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
have rw₅ : HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x) =
  HMul.hMul (α := PowerSeries R) ((PowerSeries.C : (a : R) → PowerSeries R) (φ.coeff x) : PowerSeries R)
    (HPow.hPow (α := PowerSeries R) PowerSeries.X x)
Tactic: rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ single () ((d : (a : PUnit.{1}) → ℕ) ()) = d
have h : Eq (α := ℕ) (((single () ((d : (a : PUnit.{1}) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
  ((d : (a : Unit) → ℕ) default : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ Eq.{u_1 + 1} (α := MvPowerSeries PUnit.{1} R)
    (↑((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r) : MvPowerSeries PUnit.{1} R)
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X])
          ((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r)) :
      PowerSeries R)
have this : single () ((d : (a : PUnit.{1}) → ℕ) ()) = d
Tactic: have : single () (d ()) = d := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : MvPolynomial PUnit.{1} R
⊢ (↑f : MvPowerSeries PUnit.{1} R) =
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) f) : PowerSeries R)
have monomial : ∀ (d : PUnit.{1} →₀ ℕ) (r : R),
  Eq.{u_1 + 1} (α := MvPowerSeries PUnit.{1} R)
    (↑((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r) : MvPowerSeries PUnit.{1} R)
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X])
          ((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r)) :
      PowerSeries R)
Tactic: induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    --Note: this `have` should be a generic `simp` lemma for a `Unique` type with `()` replaced
    --by any element.
    have : single () (d ()) = d := by ext; simp
    simp only [MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial,
      Polynomial.coe_monomial, PowerSeries.monomial, this]
  | add f g hf hg => simp [hf, hg]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : MvPolynomial PUnit.{1} R
monomial :
  ∀ (d : PUnit.{1} →₀ ℕ) (r : R),
    Eq.{u_1 + 1} (α := MvPowerSeries PUnit.{1} R)
      (↑((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r) : MvPowerSeries PUnit.{1} R)
      (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X])
            ((MvPolynomial.monomial d : (a : R) → MvPolynomial PUnit.{1} R) r)) :
        PowerSeries R)
⊢ (↑f : MvPowerSeries PUnit.{1} R) =
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) f) : PowerSeries R)
have add : ∀ (f g : MvPolynomial PUnit.{1} R)
  (hf :
    (↑f : MvPowerSeries PUnit.{1} R) =
      (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) f) : PowerSeries R))
  (hg :
    (↑g : MvPowerSeries PUnit.{1} R) =
      (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g) : PowerSeries R)),
  (↑(f + g) : MvPowerSeries PUnit.{1} R) =
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) (f + g)) : PowerSeries R)
Tactic: induction f using MvPolynomial.induction_on' with
  | monomial d r =>
    --Note: this `have` should be a generic `simp` lemma for a `Unique` type with `()` replaced
    --by any element.
    have : single () (d ()) = d := by ext; simp
    simp only [MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial,
      Polynomial.coe_monomial, PowerSeries.monomial, this]
  | add f g hf hg => simp [hf, hg]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (hypothesis)
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 : PowerSeries R) = (↑g : MvPowerSeries PUnit.{1} R)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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
⊢ (↑f : PowerSeries R) = (↑g : MvPowerSeries PUnit.{1} R)
have rw : (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g) : PowerSeries R) =
  (↑g : MvPowerSeries PUnit.{1} R)
Tactic: rw [this, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Basic (goal)
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)
⊢ (↑f : PowerSeries R) = (↑g : MvPowerSeries PUnit.{1} R)
have 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)
Tactic: rw [this, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (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)
have 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)
Tactic: rw [derivativeFun, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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)
⊢ (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)
have 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)
Tactic: rw [derivativeFun, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ (↑f : R⟦X⟧).derivativeFun = (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
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)
have 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⟧)
Tactic: rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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⟧)
⊢ 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)
have 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⟧)
Tactic: rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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⟧)
⊢ 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)
have h₂ : f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = Polynomial.coeff ((derivative : (a : R[X]) → R[X]) f) n
Tactic: rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
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
⊢ 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)
have h₃ : f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
⊢ (f + g).derivativeFun = f.derivativeFun + g.derivativeFun
have 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)
Tactic: ext