awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h_1 : Nontrivial A
h : ¬Eq.{u_2 + 1} (α := A⟦X⟧) X 0
⊢ LT.lt (α := Ideal A⟦X⟧) ⊥ (Ideal.span {X})

Tactic:
rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, bot_lt_iff_ne_bot, Ne
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ¬Eq.{u_2 + 1} (α := A⟦X⟧) X 0

Tactic:
X_ne_zero

Premises used: PowerSeries.X_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ¬Eq.{u_2 + 1} (α := A⟦X⟧) X 0

Tactic:
exact X_ne_zero

Premises used: PowerSeries.X_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h_1 : Nontrivial A
h : ¬Eq.{u_2 + 1} (α := A) 1 0
⊢ LT.lt (α := Ideal A⟦X⟧) (Ideal.span {X}) ⊤

Tactic:
rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
        X_dvd_iff, constantCoeff_one]

Premises used: PowerSeries.constantCoeff_one, Ne, lt_top_iff_ne_top, Ideal.eq_top_iff_one, Ideal.mem_span_singleton, PowerSeries.X_dvd_iff
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ¬Eq.{u_2 + 1} (α := A) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
hA : ¬Subsingleton A
h : Nontrivial A
⊢ ¬Eq.{u_2 + 1} (α := A) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
a : A
h :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) : A)
      ((coeff n : (a : A⟦X⟧) → A) (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X) : A)
⊢ (rescale a : (a : A⟦X⟧) → A⟦X⟧) X = HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
h : (a ^ n * if n = 1 then 1 else 0) = a * if n = 1 then 1 else 0
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((rescale a : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) a : A⟦X⟧) X) : A)

Tactic:
simp only [coeff_rescale, coeff_C_mul, coeff_X]

Premises used: PowerSeries.coeff_rescale, PowerSeries.coeff_X, PowerSeries.coeff_C_mul
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
pos : ∀ (h : n = 1), a ^ n * 1 = a * 1
neg : ∀ (h : ¬n = 1), a ^ n * 0 = a * 0
⊢ (a ^ n * if n = 1 then 1 else 0) = a * if n = 1 then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
h : n = 1
⊢ a ^ n * 1 = a * 1

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
a : A
n : ℕ
h : ¬n = 1
⊢ a ^ n * 0 = a * 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
rw : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) ((C : (a : A) → A⟦X⟧) (-1) : A⟦X⟧) X = -X
rw₁ : HMul.hMul (α := A⟦X⟧) (β := A⟦X⟧) (-(C : (a : A) → A⟦X⟧) 1 : A⟦X⟧) X = -X
rw₂ : HMul.hMul (α := A⟦X⟧) (-1) X = -X
rw₃ rw₄ : Eq.{u_2 + 1} (α := A⟦X⟧) (-X) (-X)
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((rescale (-1) : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)

Tactic:
rw [rescale_X, map_neg, map_one, neg_one_mul]

Premises used: PowerSeries.rescale_X, neg_one_mul, map_neg, map_one
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
A : Type u_2
inst : CommRing A
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((evalNegHom : (a : A⟦X⟧) → A⟦X⟧) X : A⟦X⟧) (-X : A⟦X⟧)

Tactic:
rescale_neg_one_X

Premises used: PowerSeries.rescale_neg_one_X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ Eq (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) ((algebraMap R R⟦X⟧ : (a : R) → R⟦X⟧) r : R⟦X⟧)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{u_2 + 1} (α := A⟦X⟧) ((algebraMap R A⟦X⟧ : (a : R) → A⟦X⟧) r : A⟦X⟧)
    ((C : (a : A) → A⟦X⟧) ((algebraMap R A : (a : R) → A) r : A) : A⟦X⟧)

Tactic:
MvPowerSeries.algebraMap_apply

Premises used: MvPowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Nontrivial R
⊢ Nontrivial.{u_1} (Subalgebra R R⟦X⟧)

Tactic:
{ (inferInstance : Nontrivial <| Subalgebra R <| MvPowerSeries Unit R) with }

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
φ : A →ₐ[R] B
f : A⟦X⟧
⊢ Eq.{u_3 + 1} (α := B⟦X⟧) ((mapAlgHom φ : (a : A⟦X⟧) → B⟦X⟧) f : B⟦X⟧)
    (((map (↑φ : A →+* B) : RingHom.{u_2, u_3} A⟦X⟧ B⟦X⟧) : (a : A⟦X⟧) → B⟦X⟧) f : B⟦X⟧)

Tactic:
MvPowerSeries.mapAlgHom_apply φ f

Premises used: MvPowerSeries.mapAlgHom_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ (↑φ : PowerSeries R) = PowerSeries.mk φ.coeff

Tactic:
rfl

Premises used: Polynomial.toPowerSeries, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
n : ℕ
⊢ (PowerSeries.coeff n : (a : PowerSeries R) → R) (↑φ : PowerSeries R) = φ.coeff n

Tactic:
congr_arg (coeff φ) Finsupp.single_eq_same

Premises used: Finsupp.single_eq_same, Polynomial.coeff, congr_arg, Polynomial.toPowerSeries, PowerSeries.mk
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
h :
  ∀ (n_1 : ℕ),
    Eq.{u_1 + 1} (α := R)
      ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R) (↑((monomial n : (a : R) → R[X]) a) : PowerSeries R) : R)
      ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R)
          ((PowerSeries.monomial n : (a : R) → PowerSeries R) a : PowerSeries R) :
        R)
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial n : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.monomial n : (a : R) → PowerSeries R) a)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
n_1 : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R) (↑((monomial n : (a : R) → R[X]) a) : PowerSeries R) : R)
    ((PowerSeries.coeff n_1 : (a : PowerSeries R) → R)
        ((PowerSeries.monomial n : (a : R) → PowerSeries R) a : PowerSeries R) :
      R)

Tactic:
simp [coeff_coe, PowerSeries.coeff_monomial, Polynomial.coeff_monomial, eq_comm]

Premises used: Polynomial.coeff_monomial, eq_comm, PowerSeries.coeff_monomial, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑0 : PowerSeries R) 0

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) 1)

Tactic:
have := coe_monomial 0 (1 : R)
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
this :
  Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) 1)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) 1) : PowerSeries R)
        ((PowerSeries.C : (a : R) → PowerSeries R) 1)),
    Eq.{u_1 + 1} (α := PowerSeries R) (↑1 : PowerSeries R) 1
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑1 : PowerSeries R) 1

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

Premises used: PowerSeries.monomial_zero_eq_C_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R[X]
h :
  ∀ (n : ℕ),
    Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑(φ + ψ) : PowerSeries R) : R)
      ((PowerSeries.coeff n : (a : PowerSeries R) → R) ((↑φ : PowerSeries R) + (↑ψ : PowerSeries R)) : R)
⊢ (↑(φ + ψ) : PowerSeries R) = (↑φ : PowerSeries R) + (↑ψ : PowerSeries R)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R[X]
n : ℕ
⊢ Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑(φ + ψ) : PowerSeries R) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) ((↑φ : PowerSeries R) + (↑ψ : PowerSeries R)) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R[X]
n : ℕ
⊢ Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑(φ * ψ) : PowerSeries R) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) ((↑φ : PowerSeries R) * (↑ψ : PowerSeries R)) : R)

Tactic:
simp only [coeff_coe, PowerSeries.coeff_mul, coeff_mul]

Premises used: Polynomial.coeff_mul, PowerSeries.coeff_mul, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
r : R
⊢ (↑(r • φ) : PowerSeries R) = r • (↑φ : PowerSeries R)

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) a)

Tactic:
have := coe_monomial 0 a
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
a : R
this :
  Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.monomial 0 : (a : R) → PowerSeries R) a)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := PowerSeries R) (↑((monomial 0 : (a : R) → R[X]) a) : PowerSeries R)
        ((PowerSeries.C : (a : R) → PowerSeries R) a)),
    Eq.{u_1 + 1} (α := PowerSeries R) (↑((C : (a : R) → R[X]) a) : PowerSeries R)
      ((PowerSeries.C : (a : R) → PowerSeries R) a)
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑((C : (a : R) → R[X]) a) : PowerSeries R)
    ((PowerSeries.C : (a : R) → PowerSeries R) a)

Tactic:
rwa [PowerSeries.monomial_zero_eq_C_apply] at this

Premises used: PowerSeries.monomial_zero_eq_C_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := PowerSeries R) (↑X : PowerSeries R) PowerSeries.X

Tactic:
coe_monomial _ _

Premises used: Polynomial.coe_monomial, PowerSeries.X, MvPowerSeries.X, Polynomial.X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
U : Type u_2
V : Type u_3
inst : CommSemiring U
inst_1 : CommSemiring V
φ : U →+* V
f : U[X]
h :
  ∀ (n : ℕ),
    Eq (α := V) ((PowerSeries.coeff n : (a : PowerSeries V) → V) (↑(map φ f) : PowerSeries V) : V)
      ((PowerSeries.coeff n : (a : PowerSeries V) → V)
          ((PowerSeries.map φ : (a : PowerSeries U) → PowerSeries V) (↑f : PowerSeries U) : PowerSeries V) :
        V)
⊢ (↑(map φ f) : PowerSeries V) = (PowerSeries.map φ : (a : PowerSeries U) → PowerSeries V) (↑f : PowerSeries U)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
U : Type u_2
V : Type u_3
inst : CommSemiring U
inst_1 : CommSemiring V
φ : U →+* V
f : U[X]
n : ℕ
⊢ Eq (α := V) ((PowerSeries.coeff n : (a : PowerSeries V) → V) (↑(map φ f) : PowerSeries V) : V)
    ((PowerSeries.coeff n : (a : PowerSeries V) → V)
        ((PowerSeries.map φ : (a : PowerSeries U) → PowerSeries V) (↑f : PowerSeries U) : PowerSeries V) :
      V)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ (PowerSeries.constantCoeff : (a : PowerSeries R) → R) (↑φ : PowerSeries R) = φ.coeff 0

Tactic:
rfl

Premises used: Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
x y : R[X]
h : (↑x : PowerSeries R) = (↑y : PowerSeries R)
a : ∀ (n : ℕ), x.coeff n = y.coeff n
⊢ x = y

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
x y : R[X]
h : (↑x : PowerSeries R) = (↑y : PowerSeries R)
n : ℕ
a :
  Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑x : PowerSeries R) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) (↑y : PowerSeries R) : R)
⊢ x.coeff n = y.coeff n

Tactic:
simp_rw [← coeff_coe, h]

Premises used: Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ ψ : R[X]
⊢ (↑φ : PowerSeries R) = (↑ψ : PowerSeries R) ↔ φ = ψ

Tactic:
(coe_injective R).eq_iff

Premises used: Function.Injective.eq_iff, Polynomial.coe_injective
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
rw : (↑φ : PowerSeries R) = (↑0 : PowerSeries R) ↔ φ = 0
rw₁ rw₂ : φ = 0 ↔ φ = 0
⊢ (↑φ : PowerSeries R) = 0 ↔ φ = 0

Tactic:
rw [← coe_zero, coe_inj]

Premises used: Polynomial.coe_zero, Polynomial.coe_inj
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
rw : (↑φ : PowerSeries R) = (↑1 : PowerSeries R) ↔ φ = 1
rw₁ rw₂ : φ = 1 ↔ φ = 1
⊢ (↑φ : PowerSeries R) = 1 ↔ φ = 1

Tactic:
rw [← coe_one, coe_inj]

Premises used: Polynomial.coe_one, Polynomial.coe_inj
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
⊢ (ringHom : (a : R[X]) → PowerSeries R) φ = (↑φ : PowerSeries R)

Tactic:
rfl

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

Tactic:
coeToPowerSeries.ringHom.map_pow _ _

Premises used: Polynomial.coeff, Polynomial.coeToPowerSeries.ringHom, Polynomial.toPowerSeries, PowerSeries.mk, RingHom.map_pow
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
nth_rw : eval₂ PowerSeries.C PowerSeries.X φ = (↑(eval₂ C X φ) : PowerSeries R)
⊢ eval₂ PowerSeries.C PowerSeries.X φ = (↑φ : PowerSeries R)

Tactic:
nth_rw 2 [← eval₂_C_X (p := φ)]

Premises used: Polynomial.eval₂_C_X
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
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)))
⊢ eval₂ PowerSeries.C PowerSeries.X φ = (↑(eval₂ C X φ) : PowerSeries R)

Tactic:
rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]

Premises used: map_sum, Polynomial.coeToPowerSeries.ringHom_apply, Polynomial.eval₂_eq_sum_range
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : Semiring R
φ : R[X]
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))
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
rw₅ 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)
⊢ 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:
rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply,
    coeToPowerSeries.ringHom_apply, coe_C, coe_X]

Premises used: Polynomial.coe_C, Polynomial.coe_X, map_pow, map_mul, Polynomial.coeToPowerSeries.ringHom_apply
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
h :
  Eq (α := ℕ) (((single () ((d : (a : PUnit.{1}) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
    ((d : (a : Unit) → ℕ) default : ℕ)
⊢ single () ((d : (a : PUnit.{1}) → ℕ) ()) = d

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ Eq (α := ℕ) (((single () ((d : (a : PUnit.{1}) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
    ((d : (a : Unit) → ℕ) default : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ single () ((d : (a : PUnit.{1}) → ℕ) ()) = d

Tactic:
have : single () (d ()) = d := by ext; simp
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
this : single () ((d : (a : PUnit.{1}) → ℕ) ()) = d
⊢ 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:
simp only [MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial,
      Polynomial.coe_monomial, PowerSeries.monomial, this]

Premises used: Polynomial.coe_monomial, MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial, PowerSeries.monomial
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
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:
simp [hf, hg]
-- Module: Mathlib.RingTheory.PowerSeries.Basic
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)
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)
⊢ (↑f : MvPowerSeries PUnit.{1} R) =
    (↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) f) : 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]

Premises used: Polynomial.coe_monomial, MvPolynomial.coe_monomial, MvPolynomial.uniqueAlgEquiv_monomial, Polynomial.monomial, PowerSeries.monomial
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
set :
  let 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)
⊢ (↑f : PowerSeries R) =
    (↑((AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) : (a : R[X]) → MvPolynomial PUnit.{1} R) f) :
      MvPowerSeries PUnit.{1} R)

Tactic:
set g := (MvPolynomial.uniqueAlgEquiv R PUnit).symm f

Premises used: AlgEquiv.symm, MvPolynomial.uniqueAlgEquiv, PUnit, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Basic
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
g : MvPolynomial PUnit.{1} R :=
  (AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R PUnit.{1}) : (a : R[X]) → MvPolynomial PUnit.{1} R) f
⊢ f = (MvPolynomial.uniqueAlgEquiv R PUnit.{1} : (a : MvPolynomial PUnit.{1} R) → R[X]) g

Tactic:
simp only [g, AlgEquiv.apply_symm_apply]

Premises used: AlgEquiv.apply_symm_apply