awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
H :
  Eq (α := MvPowerSeries τ S)
    (((AlgHom.comp (B := MvPolynomial Unit R) (MvPolynomial.aeval (R := R) (S₁ := MvPowerSeries τ S) fun (x : Unit) ↦ a)
              (Polynomial.aeval (MvPolynomial.X ())) :
            Polynomial R →ₐ[R] MvPowerSeries τ S) :
          (a : Polynomial R) → MvPowerSeries τ S)
        Polynomial.X :
      MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) Polynomial.X : MvPowerSeries τ S)
⊢ Eq (α := Polynomial R →ₐ[R] MvPowerSeries τ S)
    (AlgHom.comp (B := MvPolynomial Unit R) (MvPolynomial.aeval (R := R) (S₁ := MvPowerSeries τ S) fun (x : Unit) ↦ a)
        (Polynomial.aeval (MvPolynomial.X ())) :
      Polynomial R →ₐ[R] MvPowerSeries τ S)
    (Polynomial.aeval a : Polynomial R →ₐ[R] MvPowerSeries τ S)

Tactic:
apply Polynomial.algHom_ext

Premises used: Polynomial.algHom_ext
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
p : Polynomial R
⊢ Eq (α := MvPowerSeries τ S)
    (((AlgHom.comp (B := MvPolynomial Unit R) (MvPolynomial.aeval (R := R) (S₁ := MvPowerSeries τ S) fun (x : Unit) ↦ a)
              (Polynomial.aeval (MvPolynomial.X ())) :
            Polynomial R →ₐ[R] MvPowerSeries τ S) :
          (a : Polynomial R) → MvPowerSeries τ S)
        Polynomial.X :
      MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) Polynomial.X : MvPowerSeries τ S)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
rw : (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (↑Polynomial.X : R⟦X⟧) = a
rw₁ : (Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) Polynomial.X = a
rw₂ rw₃ : a = a
⊢ (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a

Tactic:
rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]

Premises used: Polynomial.coe_X, PowerSeries.substAlgHom_coe, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
a : MvPowerSeries τ S
r : S
⊢ subst (R := S) a ((C : (a : S) → S⟦X⟧) r) = (MvPowerSeries.C : (a : S) → MvPowerSeries τ S) r

Tactic:
MvPowerSeries.subst_C _

Premises used: MvPowerSeries.subst_C, PowerSeries.subst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
rw : (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a
rw₁ rw₂ : a = a
⊢ subst.{u_2, u_3, u_4} (R := R) a X = a

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_X]

Premises used: PowerSeries.substAlgHom_X, PowerSeries.coe_substAlgHom
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
a : MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : R⟦X⟧
⊢ Eq (α := MvPowerSeries τ S)
    ((MvPowerSeries.map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) (subst a f) : MvPowerSeries τ S)
    (subst (R := S) ((MvPowerSeries.map h : (a : MvPowerSeries τ R) → MvPowerSeries τ S) a)
        ((map h : (a : R⟦X⟧) → S⟦X⟧) f) :
      MvPowerSeries τ S)

Tactic:
MvPowerSeries.map_subst (HasSubst.const ha) f

Premises used: MvPowerSeries.map_subst, PowerSeries.subst, PowerSeries.HasSubst.const
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
⊢ f.order * MvPowerSeries.weightedOrder w a ≤ MvPowerSeries.weightedOrder w (subst a f)

Tactic:
.trans ?_ (MvPowerSeries.le_weightedOrder_subst _ (PowerSeries.hasSubst_iff.mp ha) _)

Premises used: MvPowerSeries.le_weightedOrder_subst, PowerSeries.hasSubst_iff, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
refine :
  f.order * MvPowerSeries.weightedOrder w a ≤
    ⨅ (d : Unit →₀ ℕ),
      ⨅ (_ : Ne (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)),
        (Finsupp.weight (MvPowerSeries.weightedOrder w ∘ Function.const Unit a) : (a : Unit →₀ ℕ) → ℕ∞) d
⊢ f.order * MvPowerSeries.weightedOrder w a ≤ MvPowerSeries.weightedOrder w (subst a f)

Tactic:
refine .trans ?_ (MvPowerSeries.le_weightedOrder_subst _ (PowerSeries.hasSubst_iff.mp ha) _)
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
simp :
  ∀ (i : Unit →₀ ℕ) (i_1 : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)),
    f.order * MvPowerSeries.weightedOrder w a ≤
      (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
⊢ f.order * MvPowerSeries.weightedOrder w a ≤
    ⨅ (d : Unit →₀ ℕ),
      ⨅ (_ : Ne (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)),
        (Finsupp.weight (MvPowerSeries.weightedOrder w ∘ Function.const Unit a) : (a : Unit →₀ ℕ) → ℕ∞) d

Tactic:
simp only [ne_eq, Function.comp_const, le_iInf_iff]

Premises used: Function.comp_const, le_iInf_iff, ne_eq
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
trans : f.order * MvPowerSeries.weightedOrder w a ≤ (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a
trans₁ :
  (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i
⊢ f.order * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i

Tactic:
trans i () * MvPowerSeries.weightedOrder w a

Premises used: Unit.unit, MvPowerSeries.weightedOrder, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
delta : Ne (α := R) ((MvPowerSeries.coeff (Finsupp.single () ((i : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ Ne (α := R) ((coeff ((i : (a : Unit) → ℕ) ()) : (a : R⟦X⟧) → R) f : R) (0 : R)

Tactic:
delta PowerSeries.coeff

Premises used: PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)

Tactic:
hi
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
h : Finsupp.single () ((i : (a : Unit) → ℕ) ()) = i
⊢ Ne (α := R) ((MvPowerSeries.coeff (Finsupp.single () ((i : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) f : R) (0 : R)

Tactic:
convert! hi
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ Finsupp.single () ((i : (a : Unit) → ℕ) ()) = i

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ f.order * MvPowerSeries.weightedOrder w a ≤ (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a

Tactic:
exact mul_le_mul_left (f.order_le (i ()) (by delta PowerSeries.coeff; convert! hi; aesop)) _

Premises used: Unit.unit, PowerSeries.order_le, mul_le_mul_left, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬Eq (α := R) ((MvPowerSeries.coeff i : (a : MvPowerSeries Unit R) → R) f : R) (0 : R)
⊢ (↑((i : (a : Unit) → ℕ) ()) : ℕ∞) * MvPowerSeries.weightedOrder w a ≤
    (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a)) : (a : Unit →₀ ℕ) → ℕ∞) i

Tactic:
simp [Finsupp.weight_apply, Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
⊢ a.order * f.order ≤ (subst a f).order

Tactic:
.trans ?_ (MvPowerSeries.le_order_subst (PowerSeries.hasSubst_iff.mp ha) _)

Premises used: MvPowerSeries.le_order_subst, PowerSeries.hasSubst_iff, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
refine : a.order * f.order ≤ (⨅ (i : Unit), (Function.const Unit a i).order) * MvPowerSeries.order f
⊢ a.order * f.order ≤ (subst a f).order

Tactic:
refine .trans ?_ (MvPowerSeries.le_order_subst (PowerSeries.hasSubst_iff.mp ha) _)
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
⊢ a.order * f.order ≤ (⨅ (i : Unit), (Function.const Unit a i).order) * MvPowerSeries.order f

Tactic:
simp [order_eq_order]

Premises used: PowerSeries.order_eq_order
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f : MvPowerSeries τ R
φ : R⟦X⟧
hf : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R) (0 : R)
⊢ φ.order ≤ (subst f φ).order

Tactic:
.trans (ENat.self_le_mul_left φ.order (f.order_ne_zero_iff_constCoeff_eq_zero.mpr hf))
    (PowerSeries.le_order_subst f (HasSubst.of_constantCoeff_zero hf) _)

Premises used: Iff.mpr, ENat.self_le_mul_left, PowerSeries.le_order_subst, MvPowerSeries.order_ne_zero_iff_constCoeff_eq_zero, PowerSeries.HasSubst.of_constantCoeff_zero, PowerSeries.order, LE.le.trans
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f : MvPowerSeries τ R
φ : R⟦X⟧
hf : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R) (0 : R)
hφ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ f.order ≤ (subst f φ).order

Tactic:
.trans (ENat.self_le_mul_right _ (order_ne_zero_iff_constCoeff_eq_zero.mpr hφ))
    (PowerSeries.le_order_subst f (HasSubst.of_constantCoeff_zero hf) _)

Premises used: Iff.mpr, PowerSeries.le_order_subst, PowerSeries.HasSubst.of_constantCoeff_zero, LE.le.trans, PowerSeries.order_ne_zero_iff_constCoeff_eq_zero, ENat.self_le_mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
rw : (subst f φ).order
| order (subst f φ)

Tactic:
rw [order_eq_order]

Premises used: PowerSeries.order_eq_order
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
conv_rhs : φ.order ≤ (subst f φ).order
⊢ φ.order ≤ order (subst f φ)

Tactic:
conv_rhs => rw [order_eq_order]

Premises used: PowerSeries.order_eq_order
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ φ.order ≤ (subst f φ).order

Tactic:
le_order_subst_left hf

Premises used: PowerSeries.le_order_subst_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ φ.order ≤ (subst f φ).order

Tactic:
exact le_order_subst_left hf

Premises used: PowerSeries.le_order_subst_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
hφ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
simp_rw : MvPowerSeries.order f ≤ (subst f φ).order
⊢ f.order ≤ order (subst f φ)

Tactic:
simp_rw [order_eq_order]

Premises used: PowerSeries.order_eq_order
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
hφ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ MvPowerSeries.order f ≤ (subst f φ).order

Tactic:
le_order_subst_right hf hφ

Premises used: PowerSeries.le_order_subst_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f φ : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
hφ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ MvPowerSeries.order f ≤ (subst f φ).order

Tactic:
exact le_order_subst_right hf hφ

Premises used: PowerSeries.le_order_subst_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
S : Type u_4
inst : CommRing S
υ : Type u_5
T : Type u_6
inst_1 : CommRing T
inst_2 : Algebra S T
a : S⟦X⟧
ha : HasSubst a
b : MvPowerSeries υ T
hb : HasSubst b
⊢ HasSubst.{u_5, u_6} (τ := υ) (S := T) ((substAlgHom hb : (a : S⟦X⟧) → MvPowerSeries υ T) a)

Tactic:
MvPowerSeries.IsNilpotent_subst hb.const ha

Premises used: MvPowerSeries.IsNilpotent_subst, PowerSeries.HasSubst.const
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
υ : Type u_5
T : Type u_6
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
a : S⟦X⟧
b : MvPowerSeries υ T
inst_6 : IsScalarTower R S T
ha : HasSubst a
hb : HasSubst b
⊢ Eq (α := R⟦X⟧ →ₐ[R] MvPowerSeries υ T) (AlgHom.comp (AlgHom.restrictScalars R (substAlgHom hb)) (substAlgHom ha))
    (substAlgHom (a := (substAlgHom hb : (a : S⟦X⟧) → MvPowerSeries υ T) a) ⋯)

Tactic:
MvPowerSeries.substAlgHom_comp_substAlgHom _ _

Premises used: PowerSeries.substAlgHom, MvPowerSeries.substAlgHom_comp_substAlgHom
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
υ : Type u_5
T : Type u_6
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
a : S⟦X⟧
b : MvPowerSeries υ T
inst_6 : IsScalarTower R S T
ha : HasSubst a
hb : HasSubst b
f : R⟦X⟧
⊢ Eq (α := MvPowerSeries υ T)
    ((substAlgHom hb : (a : S⟦X⟧) → MvPowerSeries υ T) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries Unit S) f) :
      MvPowerSeries υ T)
    ((substAlgHom (a := (substAlgHom hb : (a : S⟦X⟧) → MvPowerSeries υ T) a) ⋯ : (a : R⟦X⟧) → MvPowerSeries υ T) f :
      MvPowerSeries υ T)

Tactic:
DFunLike.congr_fun (substAlgHom_comp_substAlgHom ha hb) f

Premises used: DFunLike.congr_fun, Classical.epsilon, Set.Mem, PowerSeries.substAlgHom_comp_substAlgHom, Filter.lim, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
υ : Type u_5
T : Type u_6
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
a : S⟦X⟧
b : MvPowerSeries υ T
inst_6 : IsScalarTower R S T
ha : HasSubst a
hb : HasSubst b
⊢ Eq (α := R⟦X⟧ → MvPowerSeries υ T) (subst b ∘ subst a) (subst (subst b a))

Tactic:
simpa [funext_iff, DFunLike.ext_iff, coe_substAlgHom] using substAlgHom_comp_substAlgHom ha hb

Premises used: funext_iff, PowerSeries.substAlgHom_comp_substAlgHom, DFunLike.ext_iff, PowerSeries.coe_substAlgHom
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
υ : Type u_5
T : Type u_6
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
a : S⟦X⟧
b : MvPowerSeries υ T
inst_6 : IsScalarTower R S T
ha : HasSubst a
hb : HasSubst b
f : R⟦X⟧
⊢ subst b (subst a f) = subst (subst b a) f

Tactic:
congr_fun (subst_comp_subst ha hb) f

Premises used: PowerSeries.subst, MvPowerSeries.subst, dite, congr_fun, MvPowerSeries.eval₂, PowerSeries.subst_comp_subst
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R)
          ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
            MvPowerSeries Unit R) :
        R)
⊢ Eq (α := R⟦X⟧) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧)
    ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
      MvPowerSeries Unit R)

Tactic:
ext n
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
h :
  HMul.hMul (β := R) (r ^ n) ((MvPowerSeries.coeff (Finsupp.single () n) : (a : R⟦X⟧) → R) f : R) =
    HMul.hMul (α := R) (β := R) (Finsupp.prod (Finsupp.single () n) fun (s : Unit) (m : ℕ) ↦ r ^ m : R)
      ((MvPowerSeries.coeff (Finsupp.single () n) : (a : MvPowerSeries Unit R) → R) f : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)

Tactic:
rw [coeff_rescale, coeff, MvPowerSeries.coeff_rescale]

Premises used: PowerSeries.coeff_rescale, PowerSeries.coeff, MvPowerSeries.coeff_rescale
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
⊢ HMul.hMul (β := R) (r ^ n) ((MvPowerSeries.coeff (Finsupp.single () n) : (a : R⟦X⟧) → R) f : R) =
    HMul.hMul (α := R) (β := R) (Finsupp.prod (Finsupp.single () n) fun (s : Unit) (m : ℕ) ↦ r ^ m : R)
      ((MvPowerSeries.coeff (Finsupp.single () n) : (a : MvPowerSeries Unit R) → R) f : R)

Tactic:
simp [pow_zero, Finsupp.prod_single_index]

Premises used: pow_zero, Finsupp.prod_single_index
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
rw :
  (MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₁ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r X) f
rw₂ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    subst (HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
rw₃ :
  MvPowerSeries.subst
      (HSMul.hSMul (α := Unit → R) (β := (s : Unit) → MvPowerSeries Unit R) (fun (x : Unit) ↦ r) MvPowerSeries.X) f =
    MvPowerSeries.subst (fun (x : Unit) ↦ HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f
rw₄ rw₅ :
  Eq (α := R⟦X⟧)
    (MvPowerSeries.subst (fun (i : Unit) ↦ HSMul.hSMul (β := MvPowerSeries Unit R) r (MvPowerSeries.X i)) f)
    (MvPowerSeries.subst (fun (x : Unit) ↦ HSMul.hSMul (β := R⟦X⟧) r (MvPowerSeries.X ())) f)
⊢ (rescale r : (a : R⟦X⟧) → R⟦X⟧) f = subst (HSMul.hSMul (β := R⟦X⟧) r X) f

Tactic:
rw [rescale_eq, MvPowerSeries.rescale_eq_subst, X, subst, Pi.smul_def']

Premises used: PowerSeries.subst, PowerSeries.X, Pi.smul_def', MvPowerSeries.rescale_eq_subst, PowerSeries.rescale_eq
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
a :
  ∀ (f : R⟦X⟧) (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
⊢ Eq (α := R⟦X⟧ →+* R⟦X⟧) (↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) (rescale r)

Tactic:
ext f
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
r : R
f : R⟦X⟧
n : ℕ
a :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
a₁ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescaleAlgHom r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
a₂ a₃ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
    ((coeff n : (a : R⟦X⟧) → R)
        ((MvPowerSeries.rescale fun (x : Unit) ↦ r : (a : MvPowerSeries Unit R) → MvPowerSeries Unit R) f :
          MvPowerSeries Unit R) :
      R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (((↑(rescaleAlgHom r) : R⟦X⟧ →+* R⟦X⟧) : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale r : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)

Tactic:
rw [rescale_eq, RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply]

Premises used: RingHom.coe_coe, MvPowerSeries.rescaleAlgHom_apply, PowerSeries.rescale_eq
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
ha : Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries σ R) → R) p : R) (0 : R)
⊢ HasSubst p

Tactic:
apply HasSubst.of_constantCoeff_zero

Premises used: PowerSeries.HasSubst.of_constantCoeff_zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
ha : p 0 = 0
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)
f : R⟦X⟧
⊢ p 0 ≠ 0 → Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) 0 : ℕ) (1 : ℕ)

Tactic:
have : (p 0 ≠ 0) → (0 : σ →₀ ℕ).degree = 1 := hp_lin 0