awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a : σ → MvPowerSeries τ S
inst_1 : TopologicalSpace S
inst_2 : DiscreteTopology S
simp_rw :
  ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
    HasEval a
simp_rw₁ :
  ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
      ∀ (d : τ →₀ ℕ),
        Set.Finite.{u_1} (α := σ)
          {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
    (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧ Filter.Tendsto a Filter.cofinite (nhds 0)
⊢ HasSubst a ↔ HasEval a
have simp_rw₂ : ((∀ (s : σ), IsNilpotent.{u_5} (R := S) ((constantCoeff : (a : MvPowerSeries τ S) → S) (a s) : S)) ∧
    ∀ (d : τ →₀ ℕ),
      Set.Finite.{u_1} (α := σ)
        {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}) ↔
  (∀ (s : σ), IsTopologicallyNilpotent (a s)) ∧
    ∀ (d : τ →₀ ℕ),
      Set.Finite.{u_1} (α := σ)
        {s : σ | Ne.{u_5 + 1} (α := S) ((coeff d : (a : MvPowerSeries τ S) → S) (a s) : S) (0 : S)}
Tactic: simp_rw [hasSubst_def, hasEval_def, coeff_zero_iff,
    isTopologicallyNilpotent_iff_constantCoeff_isNilpotent]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
a b : σ → MvPowerSeries τ S
ha : HasSubst a
hb : HasSubst b
this : UniformSpace S := ⊥
⊢ HasSubst (a + b)
have rw : ∀ (hb : HasEval b) (ha : HasEval a), HasEval (a + b)
Tactic: rw [hasSubst_iff_hasEval_of_discreteTopology] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst : CommRing S
b a : σ → MvPowerSeries τ S
ha : HasSubst a
this : UniformSpace S := ⊥
⊢ HasSubst (b * a)
have rw : ∀ (ha : HasEval a), HasEval (b * a)
Tactic: rw [hasSubst_iff_hasEval_of_discreteTopology] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
a : σ → R
⊢ HasSubst (HSMul.hSMul (β := (s : σ) → MvPowerSeries σ R) a X)
have h : Eq (α := ((s : σ) → MvPowerSeries σ R) → σ → MvPowerSeries σ R) (HSMul.hSMul a)
  (HMul.hMul (α := σ → MvPowerSeries σ R) fun (s : σ) ↦
    (algebraMap R (MvPowerSeries σ R) : (a : R) → MvPowerSeries σ R) (a s))
Tactic: convert! HasSubst.X.mul_left (fun s ↦ algebraMap R (MvPowerSeries σ R) (a s))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : UniformSpace R
inst_4 : DiscreteUniformity R
inst_5 : UniformSpace S
inst_6 : DiscreteUniformity S
⊢ Eq (α := (a : σ → MvPowerSeries τ S) → (f : MvPowerSeries σ R) → MvPowerSeries τ S) subst
    (eval₂ (algebraMap R (MvPowerSeries τ S)))
have h : ∀ (x : σ → MvPowerSeries τ S) (x_1 : MvPowerSeries σ R) (n : τ →₀ ℕ),
  Eq.{u_5 + 1} (α := S) ((coeff n : (a : MvPowerSeries τ S) → S) (subst x x_1) : S)
    ((coeff n : (a : MvPowerSeries τ S) → S) (eval₂ (algebraMap R (MvPowerSeries τ S)) x x_1) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ subst a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
have rw : eval₂ (algebraMap R (MvPowerSeries τ S)) a (↑p : MvPowerSeries σ R) =
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPolynomial σ R) → MvPowerSeries τ S)
    p
Tactic: rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  eval₂ (algebraMap R (MvPowerSeries τ S)) a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
⊢ subst a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
have rw₁ : MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p =
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPolynomial σ R) → MvPowerSeries τ S)
    p
Tactic: rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  eval₂ (algebraMap R (MvPowerSeries τ S)) a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
rw₁ :
  MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
⊢ subst a (↑p : MvPowerSeries σ R) =
    ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      p
have rw₂ : MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p = MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p
Tactic: rw [subst_eq_eval₂, eval₂_coe, MvPolynomial.aeval_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
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 (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S)
have simp : (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) sorry : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
    (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
  eval₂ (algebraMap R (MvPowerSeries τ S)) a
Tactic: simp only [substAlgHom, coe_aeval ha.hasEval]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
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
⊢ (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
    eval₂ (algebraMap R (MvPowerSeries τ S)) a
have h : ⊥ = inst_3
Tactic: convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
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 : ⊥ = inst_3
⊢ (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S) =
    eval₂ (algebraMap R (MvPowerSeries τ S)) a
have h₁ : ⊥ = inst_5
Tactic: convert! coe_aeval (R := R) (hasSubst_iff_hasEval_of_discreteTopology.mp ha)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (subst a)
have rw : Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
  (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) sorry : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
    (a : MvPowerSeries σ R) → MvPowerSeries τ S)
  (subst a)
Tactic: rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (subst a)
⊢ Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (subst a)
have rw₁ : eval₂ (algebraMap R (MvPowerSeries τ S)) a = subst a
Tactic: rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
this_1 : UniformSpace R := ⊥
this : UniformSpace S := ⊥
rw :
  Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(aeval (σ := σ) (R := R) (S := MvPowerSeries τ S) (a := a) ⋯ : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (subst a)
rw₁ : eval₂ (algebraMap R (MvPowerSeries τ S)) a = subst a
⊢ Eq (α := (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (⇑(substAlgHom ha) : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (subst a)
have rw₂ : eval₂ (algebraMap R (MvPowerSeries τ S)) a = eval₂ (algebraMap R (MvPowerSeries τ S)) a
Tactic: rw [substAlgHom_eq_aeval, coe_aeval ha.hasEval, subst_eq_eval₂]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
⊢ Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (subst X) id
have rw : Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (⇑(substAlgHom sorry) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
  id
Tactic: rw [← coe_substAlgHom HasSubst.X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
⊢ Eq (α := (f : MvPowerSeries σ R) → MvPowerSeries σ R) (⇑(substAlgHom ⋯) : (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    id
have h : ∀ (f : MvPowerSeries σ R), (substAlgHom sorry : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = id f
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
f : MvPowerSeries σ R
⊢ (substAlgHom ⋯ : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f = id f
have h : ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) sorry :
        MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
      (a : MvPowerSeries σ R) → MvPowerSeries σ R)
    f =
  id f
Tactic: simp only [substAlgHom_eq_aeval]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this : UniformSpace R := ⊥
f : MvPowerSeries σ R
⊢ ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) ⋯ :
          MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
        (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      f =
    id f
have this₁ : Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
  (aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
      (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X s)) sorry :
    MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
  (AlgHom.id R (MvPowerSeries σ R) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
Tactic: have := aeval_unique (ε := AlgHom.id R (MvPowerSeries σ R)) continuous_id
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
this_1 : UniformSpace R := ⊥
f : MvPowerSeries σ R
this :
  Eq (α := MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
        (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X s)) ⋯ :
      MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
    (AlgHom.id R (MvPowerSeries σ R) : MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R)
⊢ ((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦ X s) ⋯ :
          MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
        (a : MvPowerSeries σ R) → MvPowerSeries σ R)
      f =
    id f
have this₁ : ∀ (x : MvPowerSeries σ R),
  Eq (α := MvPowerSeries σ R)
    (((aeval (σ := σ) (R := R) (S := MvPowerSeries σ R) (a := fun (s : σ) ↦
              (AlgHom.toRingHom (AlgHom.id R (MvPowerSeries σ R)) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (X s))
              sorry :
            MvPowerSeries σ R →ₐ[R] MvPowerSeries σ R) :
          (a : MvPowerSeries σ R) → MvPowerSeries σ R)
        x :
      MvPowerSeries σ R)
    ((AlgHom.id R (MvPowerSeries σ R) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) x : MvPowerSeries σ R)
Tactic: rw [DFunLike.ext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f : MvPowerSeries σ R
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f = subst a f
have rw : subst a f = subst a f
Tactic: rw [coe_substAlgHom]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
f g : MvPowerSeries σ R
⊢ subst a (f - g) = subst a f - subst a g
have simp_rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (f - g) =
  HSub.hSub (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) f : MvPowerSeries τ S)
    ((substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) g : MvPowerSeries τ S)
Tactic: simp_rw [← substAlgHom_apply ha, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
have rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
Tactic: rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
have rw₁ : ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPolynomial σ R) → MvPowerSeries τ S)
    (MvPolynomial.X s) =
  a s
Tactic: rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (↑(MvPolynomial.X s) : MvPowerSeries σ R) = a s
rw₁ :
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      (MvPolynomial.X s) =
    a s
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
have rw₂ : a s = a s
Tactic: rw [← MvPolynomial.coe_X, substAlgHom_coe ha, MvPolynomial.aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
have rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
    (↑((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) =
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
Tactic: rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
      (↑((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
have rw₁ : ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
      (a : MvPolynomial σ R) → MvPowerSeries τ S)
    ((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) =
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
Tactic: rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
rw :
  (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S)
      (↑((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) : MvPowerSeries σ R) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
rw₁ :
  ((MvPolynomial.aeval (R := R) a : MvPolynomial σ R →ₐ[R] MvPowerSeries τ S) :
        (a : MvPolynomial σ R) → MvPowerSeries τ S)
      ((MvPolynomial.monomial e : (a : R) → MvPolynomial σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
⊢ (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
have rw₂ : HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (i : σ) (k : ℕ) ↦ a i ^ k : MvPowerSeries τ S) =
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
Tactic: rw [← MvPolynomial.coe_monomial, substAlgHom_coe, MvPolynomial.aeval_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a (X s) = a s
have rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
Tactic: rw [← coe_substAlgHom ha, substAlgHom_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
s : σ
rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) (X s) = a s
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a (X s) = a s
have rw₁ : a s = a s
Tactic: rw [← coe_substAlgHom ha, substAlgHom_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Substitution (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
τ : Type u_4
S : Type u_5
inst_1 : CommRing S
inst_2 : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ subst.{u_1, u_3, u_4, u_5} (R := R) a ((monomial e : (a : R) → MvPowerSeries σ R) r) =
    HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
      ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
      (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
have rw : (substAlgHom ha : (a : MvPowerSeries σ R) → MvPowerSeries τ S) ((monomial e : (a : R) → MvPowerSeries σ R) r) =
  HMul.hMul (α := MvPowerSeries τ S) (β := MvPowerSeries τ S)
    ((algebraMap R (MvPowerSeries τ S) : (a : R) → MvPowerSeries τ S) r : MvPowerSeries τ S)
    (e.prod fun (s : σ) (n : ℕ) ↦ a s ^ n : MvPowerSeries τ S)
Tactic: rw [← coe_substAlgHom ha, substAlgHom_monomial]