awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
a : MvPowerSeries τ S
rw : MvPowerSeries.HasSubst (Function.const Unit a) ↔ HasEval a
rw₁ : MvPowerSeries.HasEval (Function.const Unit a) ↔ HasEval a
⊢ HasSubst a ↔ HasEval a
have rw₂ : MvPowerSeries.HasEval (Function.const Unit a) ↔ MvPowerSeries.HasEval (S := MvPowerSeries τ S) fun (x : Unit) ↦ a
Tactic: rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
a : MvPowerSeries τ S
rw : MvPowerSeries.HasSubst (Function.const Unit a) ↔ HasEval a
rw₁ : MvPowerSeries.HasEval (Function.const Unit a) ↔ HasEval a
rw₂ : MvPowerSeries.HasEval (Function.const Unit a) ↔ MvPowerSeries.HasEval (S := MvPowerSeries τ S) fun (x : Unit) ↦ a
⊢ HasSubst a ↔ HasEval a
have rw₃ : MvPowerSeries.HasEval (Function.const Unit a) ↔ MvPowerSeries.HasEval (Function.const Unit a)
Tactic: rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff,
    Function.const_def]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
⊢ HasSubst.{u_3, u_4} (τ := τ) (S := S) ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s)
have 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)
Tactic: apply HasSubst.of_constantCoeff_zero
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
⊢ Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
have 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)
Tactic: rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
have ha₁ : (if 0 = n then s else 0) = 0
Tactic: rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ Eq.{u_4 + 1} (α := S)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ S) → S)
        ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s : MvPowerSeries τ S) :
      S)
    (0 : S)
have ha₂ : Eq.{u_4 + 1} (α := S) 0 0
Tactic: rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
τ : Type u_3
S : Type u_4
inst : CommRing S
n : τ →₀ ℕ
hn : n ≠ 0
s : S
⊢ HasSubst.{u_3, u_4} (τ := τ) (S := S) ((MvPowerSeries.monomial n : (a : S) → MvPowerSeries τ S) s)
have 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)
Tactic: classical
  apply HasSubst.of_constantCoeff_zero
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial,
    if_neg hn.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
⊢ HasSubst.{u_3, u_2} (τ := τ) (S := R) 0
have rw : MvPowerSeries.HasSubst.{0, u_3, u_2} (τ := τ) (S := R) (Function.const Unit 0)
Tactic: rw [hasSubst_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ HasSubst (f * g)
have simp : IsNilpotent
  (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R))
Tactic: simp only [HasSubst, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
R : Type u_2
inst : CommRing R
τ : Type u_3
f g : MvPowerSeries τ R
hf : HasSubst f
⊢ HasSubst (g * f)
have simp : IsNilpotent
  (HMul.hMul (α := R) (β := R) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) g : R)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))
Tactic: simp only [HasSubst, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ HasSubst (a • f)
have simp : IsNilpotent (HSMul.hSMul (β := R) a ((MvPowerSeries.constantCoeff : (a : MvPowerSeries τ R) → R) f : R))
Tactic: simp only [HasSubst, MvPowerSeries.constantCoeff_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
Goal:
A : Type u_1
inst : CommRing A
f : A⟦X⟧
hf : HasSubst f
n : ℕ
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, Eq (α := A) ((coeff n' : (a : A⟦X⟧) → A) (f ^ m) : A) (0 : A)
have 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)
Tactic: obtain ⟨k, hk⟩ := id hf
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
have refine : ∀ (m : ℕ) (hm : m ∈ Set.Ici (k * (n + 1))) (n' : ℕ) (hn' : n' ≤ n), (↑n' : ℕ∞) < (f ^ m).order
Tactic: refine Filter.eventually_of_mem (Filter.Ici_mem_atTop (k * (n + 1))) fun m hm n' hn' ↦
    coeff_of_lt_order _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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
⊢ (↑n' : ℕ∞) < (f ^ m).order
have obtain : ∀ (m : ℕ) (hm : k * (n + 1) + m ∈ Set.Ici (k * (n + 1))), (↑n' : ℕ∞) < (f ^ (k * (n + 1) + m)).order
Tactic: obtain ⟨m, rfl⟩ := le_iff_exists_add.mp (Set.mem_Ici.mp hm)
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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))
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (f ^ k) : A) (0 : A)
have rwa : HPow.hPow (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) k = 0
Tactic: rwa [map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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' : ℕ∞) < (f ^ (k * (n + 1) + m)).order
have grw : n' < n + 1
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]
-- 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
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
ha : HasSubst a
⊢ Eq (α := R⟦X⟧ →ₐ[R] MvPowerSeries τ S) (substAlgHom ha) (aeval (R := R) (S := MvPowerSeries τ S) (a := a) ⋯)
have 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) sorry : R⟦X⟧ →ₐ[R] MvPowerSeries τ S) :
          (a : R⟦X⟧) → MvPowerSeries τ S)
        f :
      MvPowerSeries τ S)
Tactic: ext1 f
-- 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 g : R⟦X⟧
⊢ subst a (f + g) = subst a f + subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_add]
-- 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 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)
⊢ subst a (f + g) = subst a f + subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_add]
-- 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 g : R⟦X⟧
⊢ subst a (f - g) = subst a f - subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_sub]
-- 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 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)
⊢ subst a (f - g) = subst a f - subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_sub]
-- 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⟧
n : ℕ
⊢ subst a (f ^ n) = subst a f ^ n
have 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
Tactic: rw [← coe_substAlgHom ha, map_pow]
-- 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⟧
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
⊢ subst a (f ^ n) = subst a f ^ n
have 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
Tactic: rw [← coe_substAlgHom ha, map_pow]
-- 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 g : R⟦X⟧
⊢ subst a (f * g) = subst a f * subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_mul]
-- 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 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)
⊢ subst a (f * g) = subst a f * subst a g
have 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)
Tactic: rw [← coe_substAlgHom ha, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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⟧
⊢ subst a (r • f) = r • subst a f
have 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)
Tactic: rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Substitution (goal)
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)
⊢ subst a (r • f) = r • subst a f
have 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)
Tactic: rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]
-- 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 : τ →₀ ℕ
⊢ 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))
have 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)))
Tactic: convert (MvPowerSeries.coeff_subst_finite ha.const f e).image
    (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv
-- 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 (α := 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)))
have 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))
Tactic: rw [← Equiv.preimage_eq_iff_eq_image, ← Function.support_comp_eq_preimage]
-- 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 (α := 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))
have 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)
Tactic: apply congr_arg
-- 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} (α := (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)
have 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 →₀ ℕ))
Tactic: rw [← Equiv.eq_comp_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.{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 →₀ ℕ))
have 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
Tactic: ext