-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : CommRing T'
inst_5 : Algebra R S
inst_6 : Algebra R T
inst_7 : Algebra R S'
inst_8 : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
h :
  ∀ (x : S),
    Eq (α := TensorProduct R S' T')
      (((AlgHom.comp (B := TensorProduct R S T)
                (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T')
                (Algebra.TensorProduct.includeLeft : S →ₐ[R] TensorProduct R S T) :
              S →ₐ[R] TensorProduct R S' T') :
            (a : S) → TensorProduct R S' T')
          x :
        TensorProduct R S' T')
      (((AlgHom.comp
                (AlgHom.comp
                  (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
                  (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
                      (AlgHom.comp
                        (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
                        ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                          TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
                    TensorProduct R S T →ₐ[R] TensorProduct R S T'))
                Algebra.TensorProduct.includeLeft :
              S →ₐ[R] TensorProduct R S' T') :
            (a : S) → TensorProduct R S' T')
          x :
        TensorProduct R S' T')
⊢ Eq (α := TensorProduct R S T →ₐ[R] TensorProduct R S' T')
    (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T')
    (AlgHom.comp (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
        (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
            (AlgHom.comp (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
              ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
          TensorProduct R S T →ₐ[R] TensorProduct R S T') :
      TensorProduct R S T →ₐ[R] TensorProduct R S' T')
have h₁ : ∀ (x : T),
  Eq (α := TensorProduct R S' T')
    ((AlgHom.comp (B := TensorProduct R S T)
            (AlgHom.restrictScalars R (Algebra.TensorProduct.map f g : TensorProduct R S T →ₐ[R] TensorProduct R S' T'))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (AlgHom.comp
                  (Algebra.TensorProduct.map f (AlgHom.id R T') : TensorProduct R S T' →ₐ[R] TensorProduct R S' T')
                  (AlgHom.comp (↑(Algebra.TensorProduct.comm R T' S) : TensorProduct R T' S →ₐ[R] TensorProduct R S T')
                      (AlgHom.comp
                        (Algebra.TensorProduct.map g (AlgHom.id R S) : TensorProduct R T S →ₐ[R] TensorProduct R T' S)
                        ((↑(Algebra.TensorProduct.comm R S T) : TensorProduct R S T →ₐ[R] TensorProduct R T S) :
                          TensorProduct R S T →ₐ[R] TensorProduct R T S)) :
                    TensorProduct R S T →ₐ[R] TensorProduct R S T') :
                TensorProduct R S T →ₐ[R] TensorProduct R S' T'))
            Algebra.TensorProduct.includeRight :
          (a : T) → TensorProduct R S' T')
        x :
      TensorProduct R S' T')
Tactic: ext