Module: Mathlib.RingTheory.RingHom.Flat

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

Tactic:
<;>

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