awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ IsPushout.{u, u + 1} (Z := CommRingCat.of (S ⊗[R] S)) (X := CommRingCat.of (T ⊗[R] A)) (Y := CommRingCat.of S) (P :=
    CommRingCat.of (T ⊗[S] A))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
          S ⊗[R] S →ₐ[R] T ⊗[R] A)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A)))
    (CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))

Tactic:
.of_iso
      (isPushout_map_codiagonal (CommRingCat.ofHom <| algebraMap S T)
        (CommRingCat.ofHom <| algebraMap S A) (CommRingCat.ofHom <| algebraMap R S))
      ?_ ?_ (.refl _) ?_ ?_ ?_ ?_ ?_

Premises used: Algebra.algebraMap, CommRingCat.ofHom, CategoryTheory.Iso.refl, CategoryTheory.Limits.isPushout_map_codiagonal, CategoryTheory.IsPushout.of_iso
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap R S)) ≅
    CommRingCat.of (S ⊗[R] S)

Tactic:
exact (CommRingCat.isPushout_tensorProduct R S S).isoPushout.symm

Premises used: CategoryTheory.IsPushout.isoPushout, CommRingCat.isPushout_tensorProduct, CategoryTheory.Iso.symm
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ Eq (α := CommRingCat.of R ⟶ CommRingCat.of T)
    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap S T)))
    (CommRingCat.ofHom (algebraMap R T))

Tactic:
simp [IsScalarTower.algebraMap_eq R S T]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ Eq (α := CommRingCat.of R ⟶ CommRingCat.of A)
    (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
      (CommRingCat.ofHom (algebraMap S A)))
    (CommRingCat.ofHom (algebraMap R A))

Tactic:
simp [IsScalarTower.algebraMap_eq R S A]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
⊢ pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
      (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap S T)))
      (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
        (CommRingCat.ofHom (algebraMap S A))) ≅
    CommRingCat.of (T ⊗[R] A)

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

Premises used: CategoryTheory.IsPushout.isoPushout, CommRingCat.isPushout_tensorProduct, CategoryTheory.Limits.pushout.congrHom, CategoryTheory.Iso.symm
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
x : (↑(CommRingCat.of S) : Type u)
⊢ Eq (α := (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (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
                  (Iso.trans (Y :=
                    pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                      (CommRingCat.ofHom (algebraMap R T)) (CommRingCat.ofHom (algebraMap R A)))
                    (pushout.congrHom ⋯ ⋯) (Iso.symm (IsPushout.isoPushout ⋯)))))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
                CommRingCat.ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
                      S ⊗[R] S →ₐ[R] T ⊗[R] A)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[R] A)) : Type u))

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
x : (↑(CommRingCat.of S) : Type u)
⊢ Eq (α := (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S A))))
                (pushout.map (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))
                    (CommRingCat.ofHom (algebraMap S T)))
                  (CategoryStruct.comp (Y := CommRingCat.of S) (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
                  (Iso.trans (Y :=
                    pushout (X := CommRingCat.of R) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                      (CommRingCat.ofHom (algebraMap R T)) (CommRingCat.ofHom (algebraMap R A)))
                    (pushout.congrHom ⋯ ⋯) (Iso.symm (IsPushout.isoPushout ⋯)))))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
                CommRingCat.ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R S T) (IsScalarTower.toAlgHom R S A) :
                      S ⊗[R] S →ₐ[R] T ⊗[R] A)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[R] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[R] A)) : Type u))

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
x : (↑(CommRingCat.of S) : Type u)
⊢ Eq (α := (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inl (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
                CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
x : (↑(CommRingCat.of S) : Type u)
⊢ Eq (α := (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.codiagonal (CommRingCat.ofHom (algebraMap R S)) ≫ Iso.hom (Iso.refl (CommRingCat.of S)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of R) (Y := CommRingCat.of S) (Z := CommRingCat.of S)
                (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (pushout.inr (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R S)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)) ≫
                CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of S) : Type u))
        x :
      (↑(CommRingCat.of S) : Type u))

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
refine_7 :
  ∀ (x : (↑(CommRingCat.of S) : Type u)),
    Eq (α := (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                  (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
                (CommRingCat.ofHom (algebraMap S T) ≫
                  pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
                (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)))) :
            (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
      ((CommRingCat.Hom.hom
              (Iso.hom (Iso.refl (CommRingCat.of S)) ≫
                CommRingCat.ofHom
                  (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T))) :
            (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
          x :
        (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
⊢ Eq (α := CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A))
    (CategoryStruct.comp (Y :=
      pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
        (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
      (CommRingCat.ofHom (algebraMap S T) ≫
        pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
      (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯))))
    (Iso.hom (Iso.refl (CommRingCat.of S)) ≫
      CommRingCat.ofHom (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T)))

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T A : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing A
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra S T
inst_7 : IsScalarTower R S T
inst_8 : Algebra R A
inst_9 : Algebra S A
inst_10 : IsScalarTower R S A
h :
  CommRingCat.flat.{u} (X := CommRingCat.of (S ⊗[R] S)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom (AlgHom.toRingHom (Algebra.TensorProduct.lmul' R)))
x : (↑(CommRingCat.of S) : Type u)
⊢ Eq (α := (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              pushout (X := CommRingCat.of S) (Y := CommRingCat.of T) (Z := CommRingCat.of A)
                (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
              (CommRingCat.ofHom (algebraMap S T) ≫
                pushout.inl (CommRingCat.ofHom (algebraMap S T)) (CommRingCat.ofHom (algebraMap S A)))
              (Iso.hom (Iso.symm (IsPushout.isoPushout ⋯)))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
    ((CommRingCat.Hom.hom
            (Iso.hom (Iso.refl (CommRingCat.of S)) ≫
              CommRingCat.ofHom
                (RingHom.comp (AlgHom.toRingHom (R := R) Algebra.TensorProduct.includeLeft) (algebraMap S T))) :
          (a : (↑(CommRingCat.of S) : Type u)) → (↑(CommRingCat.of (T ⊗[S] A)) : Type u))
        x :
      (↑(CommRingCat.of (T ⊗[S] A)) : Type u))

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)
⊢ ∀ [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
_ :
  ∀ [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)
⊢ ∀ [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
        f →
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          g →
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
            Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
          (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective (α := S) (β := T) (⇑g : (a : S) → T)
simp : Function.Injective (α := R) (β := T) (Function.comp (β := S) (⇑g : (a : S) → T) (⇑f : (a : R) → S))
⊢ Function.Injective (α := R) (β := T) (⇑(g.comp f) : (a : R) → T)

Tactic:
simp only [RingHom.coe_comp]

Premises used: RingHom.coe_comp
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective (α := S) (β := T) (⇑g : (a : S) → T)
⊢ Function.Injective (α := R) (β := T) (Function.comp (β := S) (⇑g : (a : S) → T) (⇑f : (a : R) → S))

Tactic:
Function.Injective.comp hg hf

Premises used: Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Injective (α := S) (β := T) (⇑g : (a : S) → T)
⊢ Function.Injective (α := R) (β := T) (Function.comp (β := S) (⇑g : (a : S) → T) (⇑f : (a : R) → S))

Tactic:
exact Function.Injective.comp hg hf

Premises used: Function.Injective.comp
-- Module: Mathlib.RingTheory.RingHom.Injective
Goal:
apply :
  ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Injective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ RingHom.RespectsIso.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
apply RingHom.injective_stableUnderComposition.respectsIso

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.injective_stableUnderComposition