-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
hC :
  ∀ (x : R),
    Eq.{v + 1} (α := S)
      ((comp (β := MvPolynomial (Fin n) R)
              (comp (β := MvPolynomial σ (MvPolynomial (Fin n) R))
                (AlgHom.toRingHom
                  (MvPolynomial.aeval fun (x : σ) ↦
                    (algebraMap P.Ring S : (a : P.Ring) → S)
                      ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
                MvPolynomial.C)
              MvPolynomial.C :
            (a : R) → S)
          x :
        S)
      ((comp (comp (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom) MvPolynomial.C) MvPolynomial.C : (a : R) → S)
          x :
        S)
hC₁ :
  ∀ (i : Fin n),
    Eq.{v + 1} (α := S)
      ((comp (β := MvPolynomial σ (MvPolynomial (Fin n) R))
              (AlgHom.toRingHom
                (MvPolynomial.aeval fun (x : σ) ↦
                  (algebraMap P.Ring S : (a : P.Ring) → S)
                    ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
              MvPolynomial.C :
            (a : MvPolynomial (Fin n) R) → S)
          (MvPolynomial.X i) :
        S)
      ((comp (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom) MvPolynomial.C : (a : MvPolynomial (Fin n) R) → S)
          (MvPolynomial.X i) :
        S)
⊢ Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
have hX : ∀ (i : σ),
  Eq.{v + 1} (α := S)
    ((AlgHom.toRingHom
            (MvPolynomial.aeval fun (x : σ) ↦
              (algebraMap P.Ring S : (a : P.Ring) → S)
                ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)) :
          (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
        (MvPolynomial.X i) :
      S)
    ((comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
        (MvPolynomial.X i) :
      S)
Tactic: ext