-- Mathlib/Algebra/Category/Ring/Constructions.lean
lemma isPushout_of_isPushout (R S A B : Type u) [CommRing R] [CommRing S]
    [CommRing A] [CommRing B] [Algebra R S] [Algebra S B] [Algebra R A] [Algebra A B] [Algebra R B]
    [IsScalarTower R A B] [IsScalarTower R S B] [Algebra.IsPushout R S A B] :
    IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R A))
      (ofHom (algebraMap S B)) (ofHom (algebraMap A B)) :=
  (isPushout_tensorProduct R S A).of_iso (Iso.refl _) (Iso.refl _) (Iso.refl _)
    (Algebra.IsPushout.equiv R S A B).toCommRingCatIso (by simp) (by simp)
    (by ext; simp [Algebra.IsPushout.equiv_tmul]) (by ext; simp [Algebra.IsPushout.equiv_tmul])

Proof state:
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫
      (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom =
    (Iso.refl (of A)).hom ≫ ofHom (algebraMap A B)

Tactic:
ext

Result:
case hf.a
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x✝ : ↑(of A)
⊢ (Hom.hom
        (ofHom Algebra.TensorProduct.includeRight.toRingHom ≫
          (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom))
      x✝ =
    (Hom.hom ((Iso.refl (of A)).hom ≫ ofHom (algebraMap A B))) x✝

Proof state:
case hf.a
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x✝ : ↑(of A)
⊢ (Hom.hom
        (ofHom Algebra.TensorProduct.includeRight.toRingHom ≫
          (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom))
      x✝ =
    (Hom.hom ((Iso.refl (of A)).hom ≫ ofHom (algebraMap A B))) x✝

Tactic:
simp [Algebra.IsPushout.equiv_tmul]

Result:
no goals

Proof state:
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom =
    (Iso.refl (of S)).hom ≫ ofHom (algebraMap S B)

Tactic:
ext

Result:
case hf.a
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x✝ : ↑(of S)
⊢ (Hom.hom
        (ofHom Algebra.TensorProduct.includeLeftRingHom ≫
          (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom))
      x✝ =
    (Hom.hom ((Iso.refl (of S)).hom ≫ ofHom (algebraMap S B))) x✝

Proof state:
case hf.a
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x✝ : ↑(of S)
⊢ (Hom.hom
        (ofHom Algebra.TensorProduct.includeLeftRingHom ≫
          (Algebra.IsPushout.equiv R S A B).toRingEquiv.toCommRingCatIso.hom))
      x✝ =
    (Hom.hom ((Iso.refl (of S)).hom ≫ ofHom (algebraMap S B))) x✝

Tactic:
simp [Algebra.IsPushout.equiv_tmul]

Result:
no goals

Proof state:
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom (algebraMap R S) ≫ (Iso.refl (of S)).hom = (Iso.refl (of R)).hom ≫ ofHom (algebraMap R S)

Tactic:
simp

Result:
no goals

Proof state:
R S A B : Type u
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
⊢ ofHom (algebraMap R A) ≫ (Iso.refl (of A)).hom = (Iso.refl (of R)).hom ≫ ofHom (algebraMap R A)

Tactic:
simp

Result:
no goals