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
f : R⟦X⟧
e : τ →₀ ℕ
h :
  Eq.{max 1 (u_4 + 1)} (α := ℕ → 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))
    ((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)) ∘
      (⇑(Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()))) :
        (a : ℕ) → Unit →₀ ℕ))
⊢ 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)

Tactic:
rw [← Equiv.eq_comp_symm]

Premises used: Equiv.eq_comp_symm
-- 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 :
  ∀ (x : ℕ),
    HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ x) : 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)) ∘
          (⇑(Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()))) :
            (a : ℕ) → Unit →₀ ℕ))
        x
⊢ Eq.{max 1 (u_4 + 1)} (α := ℕ → 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))
    ((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)) ∘
      (⇑(Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()))) :
        (a : ℕ) → Unit →₀ ℕ))

Tactic:
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
f : R⟦X⟧
e : τ →₀ ℕ
x : ℕ
⊢ HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ x) : 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)) ∘
        (⇑(Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()))) :
          (a : ℕ) → Unit →₀ ℕ))
      x

Tactic:
simp [coeff]

Premises used: PowerSeries.coeff
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
b : S⟦X⟧
hb : HasSubst b
f : R⟦X⟧
e : ℕ
⊢ Function.HasFiniteSupport.{0, u_4} (M := S) fun (d : ℕ) ↦
    HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R) ((coeff e : (a : S⟦X⟧) → S) (b ^ d) : S)

Tactic:
coeff_subst_finite hb f _

Premises used: PowerSeries.coeff_subst_finite
-- 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 : τ →₀ ℕ
rw :
  Eq.{u_4 + 1} (α := S)
    (∑ᶠ (i : ℕ),
      HSMul.hSMul (α := R) (β := S)
        ((MvPowerSeries.coeff
                ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                    (a : ℕ) → Unit →₀ ℕ)
                  i) :
              (a : MvPowerSeries Unit R) → R)
            f :
          R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S)
            (Finsupp.prod
              ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                  (a : ℕ) → Unit →₀ ℕ)
                i)
              fun (s : Unit) (e : ℕ) ↦ a ^ e) :
          S))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S))
⊢ Eq.{u_4 + 1} (α := S) ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (subst a f) : S)
    (∑ᶠ (d : ℕ),
        HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S) :
      S)

Tactic:
rw [subst, MvPowerSeries.coeff_subst ha.const f e, ← finsum_comp_equiv
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm]

Premises used: Unit.unit, finsum_comp_equiv, Finsupp.uniqueLinearEquiv, PowerSeries.subst, MvPowerSeries.coeff_subst, Nat, LinearEquiv.toEquiv, Equiv.symm, 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 : R⟦X⟧
e : τ →₀ ℕ
h :
  ∀ (x : ℕ),
    HSMul.hSMul (α := R) (β := S)
        ((MvPowerSeries.coeff
                ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                    (a : ℕ) → Unit →₀ ℕ)
                  x) :
              (a : MvPowerSeries Unit R) → R)
            f :
          R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S)
            (Finsupp.prod
              ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                  (a : ℕ) → Unit →₀ ℕ)
                x)
              fun (s : Unit) (e : ℕ) ↦ a ^ e) :
          S) =
      HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ x) : S)
⊢ Eq.{u_4 + 1} (α := S)
    (∑ᶠ (i : ℕ),
      HSMul.hSMul (α := R) (β := S)
        ((MvPowerSeries.coeff
                ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                    (a : ℕ) → Unit →₀ ℕ)
                  i) :
              (a : MvPowerSeries Unit R) → R)
            f :
          R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S)
            (Finsupp.prod
              ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                  (a : ℕ) → Unit →₀ ℕ)
                i)
              fun (s : Unit) (e : ℕ) ↦ a ^ e) :
          S))
    (∑ᶠ (d : ℕ),
      HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
        ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ d) : S))

Tactic:
apply finsum_congr

Premises used: finsum_congr
-- 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 : τ →₀ ℕ
x : ℕ
h :
  (Finsupp.prod
      ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
          (a : ℕ) → Unit →₀ ℕ)
        x)
      fun (s : Unit) (e : ℕ) ↦ a ^ e) =
    a ^ x
⊢ HSMul.hSMul (α := R) (β := S)
      ((MvPowerSeries.coeff
              ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                  (a : ℕ) → Unit →₀ ℕ)
                x) :
            (a : MvPowerSeries Unit R) → R)
          f :
        R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S)
          (Finsupp.prod
            ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
                (a : ℕ) → Unit →₀ ℕ)
              x)
            fun (s : Unit) (e : ℕ) ↦ a ^ e) :
        S) =
    HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries τ S) → S) (a ^ x) : S)

Tactic:
congr
-- 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 : τ →₀ ℕ
x : ℕ
⊢ (Finsupp.prod
      ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
          (a : ℕ) → Unit →₀ ℕ)
        x)
      fun (s : Unit) (e : ℕ) ↦ a ^ e) =
    a ^ x

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
b : S⟦X⟧
hb : HasSubst b
f : R⟦X⟧
e : ℕ
⊢ Eq (α := S) ((coeff e : (a : S⟦X⟧) → S) (subst b f) : S)
    (∑ᶠ (d : ℕ),
        HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R) ((coeff e : (a : S⟦X⟧) → S) (b ^ d) : S) :
      S)

Tactic:
simp [PowerSeries.coeff, coeff_subst hb]

Premises used: PowerSeries.coeff_subst, 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
ha : HasSubst a
f : R⟦X⟧
⊢ Eq.{u_4 + 1} (α := S) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S)
    (∑ᶠ (d : ℕ),
        HSMul.hSMul (α := R) (β := S) ((coeff d : (a : R⟦X⟧) → R) f : R)
          ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) (a ^ d) : S) :
      S)

Tactic:
simp only [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, PowerSeries.coeff_subst, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
pos :
  ∀ (h : k ∣ n),
    Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S)
      ((algebraMap R S : (a : R) → S) ((coeff (n / k) : (a : R⟦X⟧) → R) f : R) : S)
neg : ∀ (h : ¬k ∣ n), Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S) (0 : S)
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S)
    (if k ∣ n then (algebraMap R S : (a : R) → S) ((coeff (n / k) : (a : R⟦X⟧) → R) f : R) else 0 : S)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
pos :
  ∀ (x : ℕ),
    x ≠ n / k →
      HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
          ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) X k ^ x) : S) =
        0
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S)
    ((algebraMap R S : (a : R) → S) ((coeff (n / k) : (a : R⟦X⟧) → R) f : R) : S)

Tactic:
rw [coeff_subst' (.X_pow hk), finsum_eq_single _ (n / k), ← pow_mul, Nat.mul_div_cancel' h,
      coeff_X_pow_self, Algebra.algebraMap_eq_smul_one]

Premises used: PowerSeries.HasSubst.X_pow, HDiv.hDiv, pow_mul, Algebra.algebraMap_eq_smul_one, PowerSeries.coeff_X_pow_self, PowerSeries.coeff_subst', finsum_eq_single, Nat.mul_div_cancel'
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
j : ℕ
hj : j ≠ n / k
pos : ¬n = k * j
⊢ HSMul.hSMul (α := R) (β := S) ((coeff j : (a : R⟦X⟧) → R) f : R)
      ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) X k ^ j) : S) =
    0

Tactic:
rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]

Premises used: smul_zero, pow_mul, PowerSeries.coeff_X_pow, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
j : ℕ
hj : j ≠ n / k
pos : ∀ (hj : n = k * j), j = n / k
⊢ ¬n = k * j

Tactic:
contrapose hj
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : k ∣ n
j : ℕ
hj : n = k * j
pos : j = k * j / k
pos₁ pos₂ : j = j
⊢ j = n / k

Tactic:
rw [hj, Nat.mul_div_cancel_left j hk.pos]

Premises used: Ne.pos, Nat.mul_div_cancel_left
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
neg :
  ∀ (x : ℕ),
    HSMul.hSMul (α := R) (β := S) ((coeff x : (a : R⟦X⟧) → R) f : R)
        ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) X k ^ x) : S) =
      0
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S) (0 : S)

Tactic:
rw [coeff_subst' (.X_pow hk), finsum_eq_zero_of_forall_eq_zero]

Premises used: PowerSeries.HasSubst.X_pow, PowerSeries.coeff_subst', finsum_eq_zero_of_forall_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
j : ℕ
neg : ¬n = k * j
⊢ HSMul.hSMul (α := R) (β := S) ((coeff j : (a : R⟦X⟧) → R) f : R)
      ((coeff n : (a : S⟦X⟧) → S) (HPow.hPow (α := S⟦X⟧) X k ^ j) : S) =
    0

Tactic:
rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]

Premises used: smul_zero, pow_mul, PowerSeries.coeff_X_pow, if_neg
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
h : ¬k ∣ n
j : ℕ
neg : ∀ (h : n = k * j), k ∣ n
⊢ ¬n = k * j

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n j : ℕ
h : n = k * j
w : ℕ
h₁ : n = k * j
⊢ k ∣ n

Tactic:
use j
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
rw :
  Eq (α := S) ((coeff 0 : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
rw₁ :
  Eq.{u_4 + 1} (α := S)
    (if k ∣ 0 then (algebraMap R S : (a : R) → S) ((coeff (0 / k) : (a : R⟦X⟧) → R) f : R) else 0 : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
rw₂ :
  Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((coeff (0 / k) : (a : R⟦X⟧) → R) f : R) : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
rw₃ :
  Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((coeff 0 : (a : R⟦X⟧) → R) f : R) : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
rw₄ rw₅ :
  Eq.{u_4 + 1} (α := S) ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)
⊢ Eq (α := S) ((constantCoeff : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S)
    ((algebraMap R S : (a : R) → S) ((constantCoeff : (a : R⟦X⟧) → R) f : R) : S)

Tactic:
rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]

Premises used: dvd_zero, Nat.zero_div, if_pos, PowerSeries.coeff_subst_X_pow, PowerSeries.coeff_zero_eq_constantCoeff
-- 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 : Eq.{u_4 + 1} (α := S) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) a : S) (0 : S)
f : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
⊢ Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) (MvPowerSeries.subst (Function.const Unit a) f) : S)
    (0 : S)

Tactic:
have := MvPowerSeries.constantCoeff_subst_eq_zero
    (hasSubst_iff.mp <| HasSubst.of_constantCoeff_zero ha) (fun _ ↦ ha) hf
-- 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 : Eq.{u_4 + 1} (α := S) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) a : S) (0 : S)
f : R⟦X⟧
hf : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) (0 : R)
this :
  Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) (MvPowerSeries.subst (Function.const Unit a) f) : S)
    (0 : S)
⊢ Eq.{u_4 + 1} (α := S) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S) (subst a f) : S) (0 : S)

Tactic:
simpa [hasSubst_iff]

Premises used: PowerSeries.hasSubst_iff
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
f : R⟦X⟧
⊢ Eq.{u_4 + 1} (α := S⟦X⟧) (((map (algebraMap R S) : RingHom.{u_2, u_4} R⟦X⟧ S⟦X⟧) : (a : R⟦X⟧) → S⟦X⟧) f : S⟦X⟧)
    (subst X f : MvPowerSeries Unit S)

Tactic:
MvPowerSeries.map_algebraMap_eq_subst_X f

Premises used: MvPowerSeries.map_algebraMap_eq_subst_X, PowerSeries.subst, PowerSeries.X
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_7
inst_1 : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
rw :
  HSMul.hSMul (α := R) (β := R) ((coeff ((e : (a : σ) → ℕ) s) : (a : R⟦X⟧) → R) f : R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (MvPowerSeries.X s) ((e : (a : σ) → ℕ) s : ℕ)) :
        R) =
    if e = Finsupp.single s ((e : (a : σ) → ℕ) s) then (coeff ((e : (a : σ) → ℕ) s) : (a : R⟦X⟧) → R) f else 0
rw₁ :
  ∀ (x : ℕ),
    x ≠ (e : (a : σ) → ℕ) s →
      HSMul.hSMul (α := R) (β := R) ((coeff x : (a : R⟦X⟧) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries σ R) → R)
              (HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) x) :
            R) =
        0
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff e : (a : MvPowerSeries σ R) → R) (subst (MvPowerSeries.X s) f) : R)
    (if e = Finsupp.single s ((e : (a : σ) → ℕ) s) then (coeff ((e : (a : σ) → ℕ) s) : (a : R⟦X⟧) → R) f else 0 : R)

Tactic:
rw [coeff_subst (HasSubst.X s), finsum_eq_single _ (e s)]

Premises used: PowerSeries.coeff_subst, PowerSeries.HasSubst.X, DFunLike.coe, finsum_eq_single
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_7
inst_1 : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ HSMul.hSMul (α := R) (β := R) ((coeff ((e : (a : σ) → ℕ) s) : (a : R⟦X⟧) → R) f : R)
      ((MvPowerSeries.coeff e : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (β := ℕ) (MvPowerSeries.X s) ((e : (a : σ) → ℕ) s : ℕ)) :
        R) =
    if e = Finsupp.single s ((e : (a : σ) → ℕ) s) then (coeff ((e : (a : σ) → ℕ) s) : (a : R⟦X⟧) → R) f else 0

Tactic:
grind [MvPowerSeries.coeff_X_pow, smul_eq_mul]

Premises used: MvPowerSeries.coeff_X_pow, smul_eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_7
inst_1 : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ),
    x ≠ (e : (a : σ) → ℕ) s →
      HSMul.hSMul (α := R) (β := R) ((coeff x : (a : R⟦X⟧) → R) f : R)
          ((MvPowerSeries.coeff e : (a : MvPowerSeries σ R) → R)
              (HPow.hPow (α := MvPowerSeries σ R) (MvPowerSeries.X s) x) :
            R) =
        0

Tactic:
grind [MvPowerSeries.coeff_X_pow, smul_eq_mul]

Premises used: MvPowerSeries.coeff_X_pow, smul_eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
rw : (map (RingHom.id R) : (a : R⟦X⟧) → R⟦X⟧) f = f
⊢ subst X f = f

Tactic:
rw [← map_algebraMap_eq_subst_X (S := R), Algebra.algebraMap_self]

Premises used: Algebra.algebraMap_self, PowerSeries.map_algebraMap_eq_subst_X
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
⊢ (map (RingHom.id R) : (a : R⟦X⟧) → R⟦X⟧) f = f

Tactic:
congr_fun map_id f

Premises used: congr_fun, PowerSeries.map_id
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
⊢ (map (RingHom.id R) : (a : R⟦X⟧) → R⟦X⟧) f = f

Tactic:
exact congr_fun map_id f

Premises used: congr_fun, PowerSeries.map_id
-- Module: Mathlib.RingTheory.PowerSeries.Substitution
Goal:
R : Type u_2
inst : CommRing R
p : Polynomial R
⊢ (↑p : R⟦X⟧) =
    (↑((Polynomial.aeval (MvPolynomial.X ()) : (a : Polynomial R) → MvPolynomial Unit R) p) : MvPowerSeries Unit R)

Tactic:
Polynomial.pUnitAlgEquiv_symm_toPowerSeries

Premises used: Polynomial.pUnitAlgEquiv_symm_toPowerSeries, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, MvPolynomial.C, Finsupp.single
-- 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
rw :
  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)
        p :
      MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) p : MvPowerSeries τ S)
⊢ Eq (α := MvPowerSeries τ S) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (↑p : R⟦X⟧) : MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) p : MvPowerSeries τ S)

Tactic:
rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom,
    MvPowerSeries.subst_coe, ← AlgHom.comp_apply]

Premises used: Polynomial.toPowerSeries_toMvPowerSeries, PowerSeries.substAlgHom, MvPowerSeries.coe_substAlgHom, AlgHom.comp_apply, MvPowerSeries.subst_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
p : Polynomial R
H :
  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)
⊢ 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)
        p :
      MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) p : MvPowerSeries τ S)

Tactic:
apply AlgHom.congr_fun

Premises used: AlgHom.congr_fun