-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Flat (goal)
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_1 :
  pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap R S)) ≅
    CommRingCat.of (S ⊗[R] S)
refine_2 :
  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 ⊗[R] A)
refine_3 :
  pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A) (CommRingCat.ofHom (algebraMap S T))
      (CommRingCat.ofHom (algebraMap S A)) ≅
    CommRingCat.of (T ⊗[S] A)
refine_4 :
  Eq (α :=
    pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap R S)) ⟶
      CommRingCat.of (T ⊗[R] A))
    (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.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
        (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 R)) ⋯ ⋯)
      (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 ⋯)))))
    (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
      CommRingCat.ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
            S ⊗[R] S →ₐ[R] T ⊗[R] A)))
refine_5 :
  Eq (α :=
    pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap R S)) ⟶
      CommRingCat.of S)
    (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))
    (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫ CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
    CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
          S ⊗[R] S →ₐ[R] T ⊗[R] A)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
    (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))
have refine_6 : 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)) sorry sorry)
    (Iso.hom (Iso.symm (IsPushout.isoPushout sorry))))
  (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 sorry sorry) (Iso.symm (IsPushout.isoPushout sorry))))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A))))
Tactic: refine .of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_