-- 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 : P.Hom P'
⊢ (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'))
      ((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') }))
        f) =
    f
have val : ∀ (x : ι) (m : ι' →₀ ℕ),
  coeff m
      (val.{w, u, v, u_1, u_2, u_3} (R := R) (S := S) (P := P)
        ((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'))
          ((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') }))
            f))
        x) =
    coeff m (f.val x)
Tactic: ext