-- Module: Mathlib.RingTheory.Extension.Generators
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') }
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 ⋯ :
                      { 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)) :
              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)))
⊢ (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

Tactic:
ext