Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
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)
⊢ pushout (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S T))
      (CommRingCat.ofHom (algebraMap R S) ≫ CommRingCat.ofHom (algebraMap S A)) ≅
    CommRingCat.of (T ⊗[R] A)

pp: case refine_3
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)
⊢ pushout (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) ≅ CommRingCat.of (T ⊗[S] A)

pp: case refine_4
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)
⊢ 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)) ⋯ ⋯ ≫
      Iso.hom ?refine_2 =
    ⋯.isoPushout.symm.hom ≫
      CommRingCat.ofHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom

pp: case refine_5
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)
⊢ pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom =
    ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom

pp: case refine_6
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)
⊢ 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)) ⋯ ⋯ ≫
      Iso.hom ?refine_3 =
    Iso.hom ?refine_2 ≫ CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom

pp: case refine_7
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)
⊢ (CommRingCat.ofHom (algebraMap S T) ≫
        pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
      Iso.hom ?refine_3 =
    (Iso.refl (CommRingCat.of S)).hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))

Tactic:
· exact pushout.congrHom (by simp [IsScalarTower.algebraMap_eq R S T])
          (by simp [IsScalarTower.algebraMap_eq R S A]) ≪≫
        (CommRingCat.isPushout_tensorProduct R T A).isoPushout.symm

Goal state after:
case refine_3
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)
⊢ pushout (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)) ≅ CommRingCat.of (T ⊗[S] A)

case refine_4
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)
⊢ 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 =
    ⋯.isoPushout.symm.hom ≫
      CommRingCat.ofHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A)).toRingHom

case refine_5
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)
⊢ pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ (Iso.refl (CommRingCat.of S)).hom =
    ⋯.isoPushout.symm.hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom

case refine_6
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)
⊢ 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)) ⋯ ⋯ ≫
      Iso.hom ?refine_3 =
    (pushout.congrHom ⋯ ⋯ ≪≫ ⋯.isoPushout.symm).hom ≫
      CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom

case refine_7
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)
⊢ (CommRingCat.ofHom (algebraMap S T) ≫
        pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A))) ≫
      Iso.hom ?refine_3 =
    (Iso.refl (CommRingCat.of S)).hom ≫ CommRingCat.ofHom (Algebra.TensorProduct.includeLeft.comp (algebraMap S T))