Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_6.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 T)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (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)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).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 A)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (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)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom))
      x✝

Tactic:
<;>

Goal state after:
case refine_6.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 T)
⊢ (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (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)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inl (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).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 A)
⊢ (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          pushout.map (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
              (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)) ⋯ ⋯ ≫
            ⋯.isoPushout.symm.hom))
      x✝ =
    (CommRingCat.Hom.hom
        (pushout.inr (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
            (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≫
          (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
            CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom))
      x✝