Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_5.h₀
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝

pp: case h₁
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝

Tactic:
<;>

Goal state after:
case refine_5.h₀
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝

case h₁
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
x✝ : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)) ≫
          ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom))
      x✝