-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst_6 : CommRing R''
inst_7 : CommRing S''
inst_8 : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst_9 : Algebra R R'
inst_10 : Algebra R' R''
inst_11 : Algebra R' S''
inst_12 : Algebra S S'
inst_13 : Algebra S' S''
inst_14 : Algebra S S''
inst_15 : Algebra R S'
inst_16 : IsScalarTower R R' S'
inst_17 : IsScalarTower R S S'
f :
  { f : P.Ring →ₐ[R] P'.Ring //
    ∀ (x : P.Ring),
      Eq.{u_2 + 1} (α := S')
        ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
        ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }
⊢ (fun (f : P.Hom P') ↦
        (Subtype.mk (p := fun (f : P.Ring →ₐ[R] P'.Ring) ↦
            ∀ (x : P.Ring),
              Eq.{u_2 + 1} (α := S')
                ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S'))
            f.toAlgHom ⋯ :
          { f : P.Ring →ₐ[R] P'.Ring //
            ∀ (x : P.Ring),
              Eq.{u_2 + 1} (α := S')
                ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }))
      ((fun
            (f :
              { f : P.Ring →ₐ[R] P'.Ring //
                ∀ (x : P.Ring),
                  Eq.{u_2 + 1} (α := S')
                    ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) : S')
                    ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }) ↦
          ({ val := fun (i : ι) ↦ ((↑f : P.Ring →ₐ[R] P'.Ring) : (a : P.Ring) → P'.Ring) (X i), aeval_val := ⋯ } :
            P.Hom P'))
        f) =
    f
have a : ∀ (i : ι) (m : ι' →₀ ℕ),
  Eq.{u_1 + 1} (α := R')
    (coeff m
      (((↑((fun (f : P.Hom P') ↦
                  (Subtype.mk (p := fun (f : P.Ring →ₐ[R] P'.Ring) ↦
                      ∀ (x : P.Ring),
                        Eq.{u_2 + 1} (α := S')
                          ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                            S')
                          ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S'))
                      f.toAlgHom sorry :
                    { f : P.Ring →ₐ[R] P'.Ring //
                      ∀ (x : P.Ring),
                        Eq.{u_2 + 1} (α := S')
                          ((aeval P'.val : (a : MvPolynomial ι' R') → S') ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                            S')
                          ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) : S') }))
                ((fun
                      (f :
                        { f : P.Ring →ₐ[R] P'.Ring //
                          ∀ (x : P.Ring),
                            Eq.{u_2 + 1} (α := S')
                              ((aeval P'.val : (a : MvPolynomial ι' R') → S')
                                  ((f : (a : P.Ring) → P'.Ring) x : P'.Ring) :
                                S')
                              ((algebraMap S S' : (a : S) → S') ((aeval P.val : (a : MvPolynomial ι R) → S) x : S) :
                                S') }) ↦
                    ({ val := fun (i : ι) ↦ ((↑f : P.Ring →ₐ[R] P'.Ring) : (a : P.Ring) → P'.Ring) (X i),
                        aeval_val := sorry } :
                      P.Hom P'))
                  f)) :
            P.Ring →ₐ[R] P'.Ring) :
          (a : MvPolynomial ι R) → P'.Ring)
        (X i)))
    (coeff m (((↑f : P.Ring →ₐ[R] P'.Ring) : (a : MvPolynomial ι R) → P'.Ring) (X i)))
Tactic: ext