-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
refine_6 :
  ∀ (x : (↑(CommRingCat.of T) : Type u)),
    Eq (α := (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.inl
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (CategoryStruct.comp (Y :=
                  pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                    (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
                  (pushout.map
                    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                      (CommRingCat.ofHom (algebraMap S T)))
                    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                      (CommRingCat.ofHom (algebraMap S A)))
                    (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T))
                    (𝟙 (CommRingCat.of A)) (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯)
                  (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯))))) :
            (a : (↑(CommRingCat.of T) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.inl
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (CategoryStruct.comp (Y := CommRingCat.of (T ⊗[R] A))
                  (Iso.hom
                    (Iso.trans (Y :=
                      pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                        (CommRingCat.ofHom (algebraMap R T)) (CommRingCat.ofHom (algebraMap R A)))
                      (pushout.congrHom ⋯ ⋯) (Iso.symm (IsPushout.isoPushout ⋯))))
                  (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A))))) :
            (a : (↑(CommRingCat.of T) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
refine_6₁ :
  ∀ (x : (↑(CommRingCat.of A) : Type u)),
    Eq (α := (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.inr
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (CategoryStruct.comp (Y :=
                  pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                    (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
                  (pushout.map
                    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                      (CommRingCat.ofHom (algebraMap S T)))
                    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                      (CommRingCat.ofHom (algebraMap S A)))
                    (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T))
                    (𝟙 (CommRingCat.of A)) (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯)
                  (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯))))) :
            (a : (↑(CommRingCat.of A) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.inr
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (CategoryStruct.comp (Y := CommRingCat.of (T ⊗[R] A))
                  (Iso.hom
                    (Iso.trans (Y :=
                      pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                        (CommRingCat.ofHom (algebraMap R T)) (CommRingCat.ofHom (algebraMap R A)))
                      (pushout.congrHom ⋯ ⋯) (Iso.symm (IsPushout.isoPushout ⋯))))
                  (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A))))) :
            (a : (↑(CommRingCat.of A) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
⊢ Eq (α :=
    pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
        (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
          (CommRingCat.ofHom (algebraMap S T)))
        (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
          (CommRingCat.ofHom (algebraMap S A))) ⟶
      CommRingCat.of (T ⊗[S] A))
    (CategoryStruct.comp (Y :=
      pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
        (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
      (pushout.map
        (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
          (CommRingCat.ofHom (algebraMap S T)))
        (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
          (CommRingCat.ofHom (algebraMap S A)))
        (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) (𝟙 (CommRingCat.of T))
        (𝟙 (CommRingCat.of A)) (CommRingCat.ofHom (algebraMap R S)) ⋯ ⋯)
      (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯))))
    (CategoryStruct.comp (Y := CommRingCat.of (T ⊗[R] A))
      (Iso.hom
        (Iso.trans (Y :=
          pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
            (CommRingCat.ofHom (algebraMap R T)) (CommRingCat.ofHom (algebraMap R A)))
          (pushout.congrHom ⋯ ⋯) (Iso.symm (IsPushout.isoPushout ⋯))))
      (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A))))

Tactic:
ext