-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' S' : Type u
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
h :
  IsPushout (Z := of R) (X := of R') (Y := of S) (P := of S') (ofHom (algebraMap R R')) (ofHom (algebraMap R S))
    (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' :=
  (Iso.trans (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
      (IsPushout.isoPushout ⋯) (Iso.symm h.isoPushout)).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    Eq (α :=
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of (R' ⊗[R] S)) (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (Iso.hom (IsPushout.isoPushout ⋯)) :
            (a : (↑(of (R' ⊗[R] S)) : Type u)) →
              (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          (r ⊗ₜ[R] 1) :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
              of R') (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
            (a : (↑(of R') : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
          r :
        (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
h3 :
  ∀ (x : R'),
    Eq (α := S')
      ((Hom.hom (Iso.inv h.isoPushout) :
            (a : (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u)) → S')
          ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
                (a : R') → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
              x :
            (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
              Type u)) :
        S')
      ((algebraMap R' S' : (a : R') → S') x : S')
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  Eq (α :=
    (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of (R' ⊗[R] S)) (Y :=
            pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
            (Iso.hom (IsPushout.isoPushout ⋯)) :
          (a : (↑(of (R' ⊗[R] S)) : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
        ((algebraMap S (R' ⊗[R] S) : (a : S) → R' ⊗[R] S) s : R' ⊗[R] S) :
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of S) (Y := pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
            (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) :
          (a : (↑(of S) : Type u)) → (↑(pushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
        s :
      (↑(pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) : Type u))
⊢ Eq (α := S') ((e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S)) : (a : S) → S') s : S')
    ((algebraMap S S' : (a : S) → S') s : S')
have h4 : ∀ (x : S),
  Eq (α := (↑(of S') : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (CategoryStruct.comp (Y :=
              pushout (X := of R) (Y := of R') (Z := of S) (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))
              (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S))) (Iso.inv h.isoPushout)) :
          (a : (↑(of S) : Type u)) → (↑(of S') : Type u))
        x :
      (↑(of S') : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            of S) (Y := of S') (ofHom (algebraMap S S')) :
          (a : (↑(of S) : Type u)) → (↑(of S') : Type u))
        x :
      (↑(of S') : Type u))
Tactic: have h4 (x : S) := congr($(h.inr_isoPushout_inv) x)