awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 : τ →₀ ℕ
⊢ 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)
have 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))
Tactic: rw [subst, MvPowerSeries.coeff_subst ha.const f e, ← finsum_comp_equiv
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 : τ →₀ ℕ
⊢ 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))
have 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)
Tactic: apply finsum_congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
      ((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)
have h : (Finsupp.prod
    ((Equiv.symm (LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ())) :
        (a : ℕ) → Unit →₀ ℕ)
      x)
    fun (s : Unit) (e : ℕ) ↦ a ^ e) =
  a ^ x
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬k ∣ n), Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S) (0 : S)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ 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
have pos : ¬n = k * j
Tactic: rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ ¬n = k * j
have pos : ∀ (hj : n = k * j), j = n / k
Tactic: contrapose hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ j = n / k
have pos : j = k * j / k
Tactic: rw [hj, Nat.mul_div_cancel_left j hk.pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ j = n / k
have pos₁ : j = j
Tactic: rw [hj, Nat.mul_div_cancel_left j hk.pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ Eq (α := S) ((coeff n : (a : S⟦X⟧) → S) (subst (HPow.hPow (α := S⟦X⟧) X k) f) : S) (0 : S)
have 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
Tactic: rw [coeff_subst' (.X_pow hk), finsum_eq_zero_of_forall_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 : ℕ
⊢ 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
have neg : ¬n = k * j
Tactic: rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 : ℕ
⊢ ¬n = k * j
have neg : ∀ (h : n = k * j), k ∣ n
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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⟧
⊢ 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)
have 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)
Tactic: rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← coeff_zero_eq_constantCoeff, coeff_subst_X_pow hk, if_pos (dvd_zero k),
    Nat.zero_div, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (hypothesis)
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) (subst a f) : S) (0 : S)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
σ : Type u_7
inst_1 : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ 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)
have 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
Tactic: rw [coeff_subst (HasSubst.X s), finsum_eq_single _ (e s)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ 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)
have 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
Tactic: rw [coeff_subst (HasSubst.X s), finsum_eq_single _ (e s)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
f : R⟦X⟧
⊢ subst X f = f
have rw : (map (RingHom.id R) : (a : R⟦X⟧) → R⟦X⟧) f = f
Tactic: rw [← map_algebraMap_eq_subst_X (S := R), Algebra.algebraMap_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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) ((substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (↑p : R⟦X⟧) : MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) p : MvPowerSeries τ S)
have 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)
Tactic: rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom,
    MvPowerSeries.subst_coe, ← AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
        p :
      MvPowerSeries τ S)
    ((Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) p : MvPowerSeries τ S)
have 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)
Tactic: apply AlgHom.congr_fun
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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 (α := 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)
have 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)
Tactic: apply Polynomial.algHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a
have rw : (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) (↑Polynomial.X : R⟦X⟧) = a
Tactic: rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a
have rw₁ : (Polynomial.aeval a : (a : Polynomial R) → MvPowerSeries τ S) Polynomial.X = a
Tactic: rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a
have rw₂ : a = a
Tactic: rw [← Polynomial.coe_X, substAlgHom_coe, Polynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ subst.{u_2, u_3, u_4} (R := R) a X = a
have rw : (substAlgHom ha : (a : R⟦X⟧) → MvPowerSeries τ S) X = a
Tactic: rw [← coe_substAlgHom ha, substAlgHom_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ subst.{u_2, u_3, u_4} (R := R) a X = a
have rw₁ : a = a
Tactic: rw [← coe_substAlgHom ha, substAlgHom_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
have 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
Tactic: refine .trans ?_ (MvPowerSeries.le_weightedOrder_subst _ (PowerSeries.hasSubst_iff.mp ha) _)