awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
ha :
  Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.coeff 0 : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
ha₁ : (if 0 = n then s else 0) = 0
ha₂ ha₃ : Eq.{u_4 + 1} (α := S) 0 0
⊢ Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)

Tactic:
rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, Ne.symm, MvPowerSeries.coeff_monomial, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
ha :
  Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
⊢ HasSubst.{u_3, u_4} (τ := τ) (S := S) ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s)

Tactic:
classical
  apply HasSubst.of_constantCoeff_zero
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, Ne.symm, MvPowerSeries.coeff_monomial, PowerSeries.HasSubst.of_constantCoeff_zero, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
S : Type u_4
inst : CommRing S
n : ℕ
hn : n ≠ 0
s : S
⊢ HasSubst.{0, u_4} (τ := Unit) (S := S) ((monomial n : (a : S) → S⟦X⟧) s)

Tactic:
HasSubst.monomial (Finsupp.single_ne_zero.mpr hn) s

Premises used: Iff.mpr, Finsupp.single_ne_zero, PowerSeries.HasSubst.monomial
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
rw : MvPowerSeries.HasSubst.{0, u_3, u_2} (τ := τ) (S := R) (Function.const Unit 0)
⊢ HasSubst.{u_3, u_2} (τ := τ) (S := R) 0

Tactic:
rw [hasSubst_iff]

Premises used: PowerSeries.hasSubst_iff
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
⊢ MvPowerSeries.HasSubst.{0, u_3, u_2} (τ := τ) (S := R) (Function.const Unit 0)

Tactic:
MvPowerSeries.HasSubst.zero

Premises used: MvPowerSeries.HasSubst.zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
⊢ MvPowerSeries.HasSubst.{0, u_3, u_2} (τ := τ) (S := R) (Function.const Unit 0)

Tactic:
exact MvPowerSeries.HasSubst.zero

Premises used: MvPowerSeries.HasSubst.zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
⊢ HasSubst.{0, u_2} (τ := Unit) (S := R) 0

Tactic:
PowerSeries.HasSubst.zero

Premises used: PowerSeries.HasSubst.zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
hg : HasSubst g
⊢ HasSubst (f + g)

Tactic:
(Commute.all _ _).isNilpotent_add hf hg

Premises used: Commute.isNilpotent_add
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
simp :
  IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R))
⊢ HasSubst (f * g)

Tactic:
simp only [HasSubst, map_mul]

Premises used: PowerSeries.HasSubst, map_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R))

Tactic:
(Commute.all _ _).isNilpotent_mul_right hf

Premises used: Commute.isNilpotent_mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R))

Tactic:
exact (Commute.all _ _).isNilpotent_mul_right hf

Premises used: Commute.isNilpotent_mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
simp :
  IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))
⊢ HasSubst (g * f)

Tactic:
simp only [HasSubst, map_mul]

Premises used: PowerSeries.HasSubst, map_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))

Tactic:
(Commute.all _ _).isNilpotent_mul_left hf

Premises used: Commute.isNilpotent_mul_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ IsNilpotent
    (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))

Tactic:
exact (Commute.all _ _).isNilpotent_mul_left hf

Premises used: Commute.isNilpotent_mul_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
r a : MvPowerSeries τ S
ha : HasSubst a
⊢ HasSubst (r • a)

Tactic:
ha.mul_right

Premises used: PowerSeries.HasSubst.mul_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_3
f : MvPowerSeries τ R
a : A
hf : HasSubst f
simp : IsNilpotent (HSMul.hSMul (β := R) a ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))
⊢ HasSubst (a • f)

Tactic:
simp only [HasSubst, MvPowerSeries.constantCoeff_smul]

Premises used: PowerSeries.HasSubst, MvPowerSeries.constantCoeff_smul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_3
f : MvPowerSeries τ R
a : A
hf : HasSubst f
⊢ IsNilpotent (HSMul.hSMul (β := R) a ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))

Tactic:
IsNilpotent.smul hf _

Premises used: IsNilpotent.smul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_3
f : MvPowerSeries τ R
a : A
hf : HasSubst f
⊢ IsNilpotent (HSMul.hSMul (β := R) a ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))

Tactic:
exact IsNilpotent.smul hf _

Premises used: IsNilpotent.smul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_3
a : A
t : τ
⊢ HasSubst (HSMul.hSMul (β := MvPowerSeries τ R) a (MvPowerSeries.X t))

Tactic:
(HasSubst.X t).smul' _

Premises used: PowerSeries.HasSubst.smul', PowerSeries.HasSubst.X
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
a : A
⊢ HasSubst (HSMul.hSMul (β := R⟦X⟧) a X)

Tactic:
HasSubst.X'.smul' _

Premises used: PowerSeries.HasSubst.smul', PowerSeries.HasSubst.X'
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n : ℕ
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0),
    ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (f ^ m) : A) (0 : A)
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (f ^ m) : A) (0 : A)

Tactic:
obtain ⟨k, hk⟩ := id hf

Premises used: id
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (f ^ m) : A) (0 : A)

Tactic:
Filter.eventually_of_mem (Filter.Ici_mem_atTop (k * (n + 1))) fun m hm n' hn' ↦
    coeff_of_lt_order _ ?_

Premises used: PowerSeries.coeff_of_lt_order, HMul.hMul, Filter.eventually_of_mem, Filter.Ici_mem_atTop, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
refine : ∀ (m : ℕ) (hm : m ∈ Set.Ici (k * (n + 1))) (n' : ℕ) (hn' : n' ≤ n), (↑n' : ℕ∞) < (f ^ m).order
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (f ^ m) : A) (0 : A)

Tactic:
refine Filter.eventually_of_mem (Filter.Ici_mem_atTop (k * (n + 1))) fun m hm n' hn' ↦
    coeff_of_lt_order _ ?_

Premises used: HMul.hMul, Filter.eventually_of_mem, Filter.Ici_mem_atTop, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
m : ℕ
hm : m ∈ Set.Ici (k * (n + 1))
n' : ℕ
hn' : n' ≤ n
obtain : ∀ (m : ℕ) (hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))), (↑n' : ℕ∞) < (f ^ (k * (n + 1) + m)).order
⊢ (↑n' : ℕ∞) < (f ^ m).order

Tactic:
obtain ⟨m, rfl⟩ := le_iff_exists_add.mp (Set.mem_Ici.mp hm)

Premises used: le_iff_exists_add, Set.mem_Ici, Iff.mp, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
rwa rwa₁ rwa₂ rwa₃ : HPow.hPow (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) k = 0
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (f ^ k) : A) (0 : A)

Tactic:
rwa [map_pow]

Premises used: map_pow
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
grw : n' < n + 1
⊢ (↑n' : ℕ∞) < (f ^ (k * (n + 1) + m)).order

Tactic:
grw [pow_add, ← order_mul_ge, pow_mul, ← le_order_pow_of_constantCoeff_eq_zero _
    (by rwa [map_pow]), ← _root_.le_add_right le_rfl, Nat.cast_lt]

Premises used: le_rfl, PowerSeries.order_mul_ge, pow_add, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, pow_mul, Nat.cast_lt, le_add_right
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : HPow.hPow (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) k = 0
n' : ℕ
hn' : n' ≤ n
m : ℕ
hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))
⊢ n' < n + 1

Tactic:
lia
-- 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
f : R⟦X⟧
⊢ subst a f = MvPowerSeries.subst (fun (x : Unit) ↦ a) f

Tactic:
rfl

Premises used: PowerSeries.subst, rfl
-- 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
⊢ Eq (α := (a : R⟦X⟧) → MvPowerSeries τ S) (⇑(substAlgHom ha) : (a : R⟦X⟧) → MvPowerSeries τ S) (subst a)

Tactic:
MvPowerSeries.coe_substAlgHom ha.const

Premises used: MvPowerSeries.coe_substAlgHom, 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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
H :
  ∀ (f : R⟦X⟧),
    Eq (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      (((aeval (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : R⟦X⟧ →ₐ[R] MvPowerSeries τ S) :
            (a : R⟦X⟧) → MvPowerSeries τ S)
          f :
        MvPowerSeries τ S)
⊢ Eq (α := R⟦X⟧ →ₐ[R] MvPowerSeries τ S) (substAlgHom ha) (aeval (R := R) (S := MvPowerSeries τ S) (a := a) ⋯)

Tactic:
ext1 f
-- 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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
f : R⟦X⟧
⊢ Eq (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
    (((aeval (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : R⟦X⟧ →ₐ[R] MvPowerSeries τ S) :
          (a : R⟦X⟧) → MvPowerSeries τ S)
        f :
      MvPowerSeries τ S)

Tactic:
simpa [substAlgHom] using congr_fun (MvPowerSeries.substAlgHom_eq_aeval ha.const) f

Premises used: PowerSeries.substAlgHom, MvPowerSeries.substAlgHom_eq_aeval, congr_fun, 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
ha : HasSubst a
f g : R⟦X⟧
rw :
  (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (f + g) =
    HAdd.hAdd (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
rw₁ rw₂ :
  HAdd.hAdd (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S) =
    HAdd.hAdd (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
⊢ subst a (f + g) = subst a f + subst a g

Tactic:
rw [← coe_substAlgHom ha, map_add]

Premises used: map_add, 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
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f g : R⟦X⟧
rw :
  (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (f - g) =
    HSub.hSub (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
rw₁ rw₂ :
  HSub.hSub (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S) =
    HSub.hSub (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
⊢ subst a (f - g) = subst a f - subst a g

Tactic:
rw [← coe_substAlgHom ha, map_sub]

Premises used: map_sub, 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
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
n : ℕ
rw :
  (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (f ^ n) =
    HPow.hPow (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S) n
rw₁ rw₂ :
  HPow.hPow (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S) n =
    HPow.hPow (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S) n
⊢ subst a (f ^ n) = subst a f ^ n

Tactic:
rw [← coe_substAlgHom ha, map_pow]

Premises used: map_pow, 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
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f g : R⟦X⟧
rw :
  (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (f * g) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
rw₁ rw₂ :
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
      ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) g : MvPowerSeries τ S)
⊢ subst a (f * g) = subst a f * subst a g

Tactic:
rw [← coe_substAlgHom ha, map_mul]

Premises used: map_mul, PowerSeries.coe_substAlgHom
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
A : Type u_1
inst : CommRing A
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra A R
τ : Type u_3
S : Type u_4
inst_3 : CommRing S
inst_4 : Algebra R S
a : MvPowerSeries τ S
inst_5 : Algebra A S
inst_6 : IsScalarTower A R S
ha : HasSubst a
r : A
f : R⟦X⟧
rw :
  (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (r • f) =
    HSMul.hSMul (β := MvPowerSeries τ S) r ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
rw₁ rw₂ :
  HSMul.hSMul (β := MvPowerSeries τ S) r ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S) =
    HSMul.hSMul (β := MvPowerSeries τ S) r ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) f : MvPowerSeries τ S)
⊢ subst a (r • f) = r • subst a f

Tactic:
rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]

Premises used: AlgHom.map_smul_of_tower, 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
inst_2 : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ Set.Finite (α := ℕ)
    (Set.image (α := Unit →₀ ℕ)
      (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ)
      (Function.support.{0, u_4} (M := S) fun (d : Unit →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S)))

Tactic:
(MvPowerSeries.coeff_subst_finite ha.const f e).image
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv

Premises used: Unit.unit, Finsupp.uniqueLinearEquiv, Set.Finite.image, Nat, LinearEquiv.toEquiv, MvPowerSeries.coeff_subst_finite, PowerSeries.HasSubst.const, 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
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
h :
  Eq (α := Set ℕ)
    (Function.support.{0, u_4} (M := S) fun (d : ℕ) ↦
      HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S))
    (Set.image (α := Unit →₀ ℕ)
      (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ)
      (Function.support.{0, u_4} (M := S) fun (d : Unit →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S)))
⊢ Set.Finite (α := ℕ)
    (Function.support.{0, u_4} (M := S) fun (d : ℕ) ↦
      HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S))

Tactic:
convert (MvPowerSeries.coeff_subst_finite ha.const f e).image
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv

Premises used: Unit.unit, Finsupp.uniqueLinearEquiv, Set.Finite.image, Nat, LinearEquiv.toEquiv, MvPowerSeries.coeff_subst_finite, PowerSeries.HasSubst.const, 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
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
h :
  Eq (α := Set (Unit →₀ ℕ))
    (Function.support.{0, u_4} (M := S)
      ((fun (d : ℕ) ↦
          HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
            ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S)) ∘
        (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
          (a : Unit →₀ ℕ) → ℕ)))
    (Function.support.{0, u_4} (M := S) fun (d : Unit →₀ ℕ) ↦
      HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S))
⊢ Eq (α := Set ℕ)
    (Function.support.{0, u_4} (M := S) fun (d : ℕ) ↦
      HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S))
    (Set.image (α := Unit →₀ ℕ)
      (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ)
      (Function.support.{0, u_4} (M := S) fun (d : Unit →₀ ℕ) ↦
        HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S)))

Tactic:
rw [← Equiv.preimage_eq_iff_eq_image, ← Function.support_comp_eq_preimage]

Premises used: Function.support_comp_eq_preimage, Equiv.preimage_eq_iff_eq_image
-- 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⟧
e : τ →₀ ℕ
h :
  Eq.{u_4 + 1} (α := (Unit →₀ ℕ) → S)
    ((fun (d : ℕ) ↦
        HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S)) ∘
      (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) : (a : Unit →₀ ℕ) → ℕ))
    fun (d : Unit →₀ ℕ) ↦
    HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S)
⊢ Eq (α := Set (Unit →₀ ℕ))
    (Function.support.{0, u_4} (M := S)
      ((fun (d : ℕ) ↦
          HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
            ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S)) ∘
        (⇑(LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
          (a : Unit →₀ ℕ) → ℕ)))
    (Function.support.{0, u_4} (M := S) fun (d : Unit →₀ ℕ) ↦
      HSMul.hSMul (α := R) (β := S) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (d.prod fun (s : Unit) (e : ℕ) ↦ a ^ e) : S))

Tactic:
apply congr_arg

Premises used: congr_arg