-- 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_5 :
  ∀ (x : (↑(CommRingCat.of S) : Type u)),
    Eq (α := (↑(CommRingCat.of S) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                  (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
                (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
                (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))) :
            (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
          x :
        (↑(CommRingCat.of S) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                  (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
                (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
                (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
                  CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))) :
            (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
          x :
        (↑(CommRingCat.of S) : Type u))
⊢ 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)))
have refine_5₁ : ∀ (x : (↑(CommRingCat.of S) : Type u)),
  Eq (α := (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout sorry)) ≫
                CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
Tactic: ext