awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
dsimp :
  P (R := (↑S : Type u)) (S :=
    (↑(Functor.obj
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F :=
              span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
              (CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u))))
          WalkingSpan.left) :
      Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
⊢ P (R := (↑S : Type u)) (S :=
    (↑(Functor.obj
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F :=
              span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
              (ColimitCocone.cocone
                { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
                  isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) :
                  ColimitCocone
                    (span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                      CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                      (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u)))) })))
          WalkingSpan.left) :
      Type u))
    (CommRingCat.Hom.hom
      (NatTrans.app
        (Cocone.ι
          (ColimitCocone.cocone
            { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
              isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) }))
        WalkingSpan.left))

Tactic:
dsimp only [CommRingCat.pushoutCocone_inl, PushoutCocone.ι_app_left]

Premises used: CommRingCat.pushoutCocone_inl, CategoryTheory.Limits.PushoutCocone.ι_app_left
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
apply : P (R := (↑R : Type u)) (S := (↑T : Type u)) (algebraMap (↑R : Type u) (↑T : Type u))
⊢ P (R := (↑S : Type u)) (S :=
    (↑(Functor.obj
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F :=
              span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
              (CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u))))
          WalkingSpan.left) :
      Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))

Tactic:
apply hP R T S (S ⊗[R] T)

Premises used: CommRingCat.carrier, TensorProduct
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (R := (↑R : Type u)) (S := (↑T : Type u)) (algebraMap (↑R : Type u) (↑T : Type u))

Tactic:
H
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (R := (↑R : Type u)) (S := (↑T : Type u)) (algebraMap (↑R : Type u) (↑T : Type u))

Tactic:
exact H
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_12 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : Algebra.IsPushout R S R' S'
h : P (algebraMap R S) ∧ Q (algebraMap R S)
⊢ P (algebraMap R' S') ∧ Q (algebraMap R' S')

Tactic:
⟨hP R S R' S' h.1, hQ R S R' S' h.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_12 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
inst_11 : Algebra.IsPushout R S R' S'
h : P (algebraMap R S) ∧ Q (algebraMap R S)
⊢ P (algebraMap R' S') ∧ Q (algebraMap R' S')

Tactic:
exact ⟨hP R S R' S' h.1, hQ R S R' S' h.2⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk, RingHom.toMorphismProperty, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : X ≅ Y)
    (f : Y ⟶ Z),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
refine_2 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : Y ≅ Z)
    (f : X ⟶ Y),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
refine_3 :
  ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso) {R S T : Type u}
    [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
refine_4 :
  ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso) {R S T : Type u}
    [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : X ≅ Y
f : Y ⟶ Z
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

Tactic:
h.right f.hom e.commRingCatIsoToRingEquiv hf

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.right, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : X ≅ Y
f : Y ⟶ Z
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

Tactic:
exact h.right f.hom e.commRingCatIsoToRingEquiv hf

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.right
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : Y ≅ Z
f : X ⟶ Y
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
h.left f.hom e.commRingCatIsoToRingEquiv hf

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.left, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : Y ≅ Z
f : X ⟶ Y
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
exact h.left f.hom e.commRingCatIsoToRingEquiv hf

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.left
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
refine_3 :
  ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
⊢ ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
refine_3 :
  ∀ [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
⊢ ∀ [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
refine_3 :
  ∀ [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
⊢ ∀ [inst_2 : CommRing Z] (f : X →+* Y) (e : Y ≃+* Z),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
inst_2 : CommRing Z
f : X →+* Y
e : Y ≃+* Z
hf : P f
⊢ P (e.toRingHom.comp f)

Tactic:
MorphismProperty.RespectsIso.postcomp (toMorphismProperty P)
      e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp, RingEquiv.toCommRingCatIso, CommRingCat.ofHom, RingHom.toMorphismProperty, CategoryTheory.Iso.hom
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
inst_2 : CommRing Z
f : X →+* Y
e : Y ≃+* Z
hf : P f
⊢ P (e.toRingHom.comp f)

Tactic:
exact MorphismProperty.RespectsIso.postcomp (toMorphismProperty P)
      e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp, RingEquiv.toCommRingCatIso, CommRingCat.ofHom, RingHom.toMorphismProperty, CategoryTheory.Iso.hom
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
refine_4 :
  ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
⊢ ∀ [inst : CommRing X] [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
refine_4 :
  ∀ [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
⊢ ∀ [inst_1 : CommRing Y] [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
refine_4 :
  ∀ [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
⊢ ∀ [inst_2 : CommRing Z] (f : Y →+* Z) (e : X ≃+* Y),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
inst_2 : CommRing Z
f : Y →+* Z
e : X ≃+* Y
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
MorphismProperty.RespectsIso.precomp (toMorphismProperty P)
      e.toCommRingCatIso.hom (CommRingCat.ofHom f)

Premises used: CategoryTheory.MorphismProperty.RespectsIso.precomp, RingEquiv.toCommRingCatIso, CommRingCat.ofHom, RingHom.toMorphismProperty, CategoryTheory.Iso.hom
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
X Y Z : Type u
inst : CommRing X
inst_1 : CommRing Y
inst_2 : CommRing Z
f : Y →+* Z
e : X ≃+* Y
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P)
      e.toCommRingCatIso.hom (CommRingCat.ofHom f)

Premises used: CategoryTheory.MorphismProperty.RespectsIso.precomp, RingEquiv.toCommRingCatIso, CommRingCat.ofHom, RingHom.toMorphismProperty, CategoryTheory.Iso.hom
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩

Premises used: Iff.intro, CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange)
    (R S R' S' : Type u) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing R') (x_3 : CommRing S') (x_4 : Algebra R S)
    (x_5 : Algebra R R') (x_6 : Algebra R S') (x_7 : Algebra S S') (x_8 : Algebra R' S') (x_9 : IsScalarTower R S S')
    (x_10 : IsScalarTower R R' S') (hsq : Algebra.IsPushout R S R' S')
    (hRS : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R S)),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R' S')
refine_2 :
  ∀ (h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {R : CommRingCat.{u}}
    (S R' S' : CommRingCat.{u}) (f : R ⟶ S) (g : R ⟶ R') (f' : R' ⟶ S') (g' : S ⟶ S') (hsq : IsPushout g f f' g')
    (hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
refine ⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing R'
x_3 : CommRing S'
x_4 : Algebra R S
x_5 : Algebra R R'
x_6 : Algebra R S'
x_7 : Algebra S S'
x_8 : Algebra R' S'
h_1 : IsScalarTower R S S'
h_2 : IsScalarTower R R' S'
hsq : Algebra.IsPushout R S R' S'
hRS : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R S)
refine_1 :
  ∀
    (hsq :
      IsPushout (Z := CommRingCat.of R) (X := CommRingCat.of S) (Y := CommRingCat.of R') (P := CommRingCat.of S')
        (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R R')) (CommRingCat.ofHom (algebraMap S S'))
        (CommRingCat.ofHom (algebraMap R' S')))
    (hRS : P (algebraMap R S)), P (algebraMap R' S')
⊢ P (algebraMap R' S')

Tactic:
rw [← CommRingCat.isPushout_iff_isPushout] at hsq

Premises used: CommRingCat.isPushout_iff_isPushout
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing R'
x_3 : CommRing S'
x_4 : Algebra R S
x_5 : Algebra R R'
x_6 : Algebra R S'
x_7 : Algebra S S'
x_8 : Algebra R' S'
h_1 : IsScalarTower R S S'
h_2 : IsScalarTower R R' S'
hsq :
  IsPushout (Z := CommRingCat.of R) (X := CommRingCat.of S) (Y := CommRingCat.of R') (P := CommRingCat.of S')
    (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R R')) (CommRingCat.ofHom (algebraMap S S'))
    (CommRingCat.ofHom (algebraMap R' S'))
hRS : P (algebraMap R S)
⊢ P (algebraMap R' S')

Tactic:
h.1 (f := CommRingCat.ofHom (algebraMap R S)) hsq.flip hRS

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout, CategoryTheory.IsPushout.flip, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing R'
x_3 : CommRing S'
x_4 : Algebra R S
x_5 : Algebra R R'
x_6 : Algebra R S'
x_7 : Algebra S S'
x_8 : Algebra R' S'
h_1 : IsScalarTower R S S'
h_2 : IsScalarTower R R' S'
hsq :
  IsPushout (Z := CommRingCat.of R) (X := CommRingCat.of S) (Y := CommRingCat.of R') (P := CommRingCat.of S')
    (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R R')) (CommRingCat.ofHom (algebraMap S S'))
    (CommRingCat.ofHom (algebraMap R' S'))
hRS : P (algebraMap R S)
⊢ P (algebraMap R' S')

Tactic:
exact h.1 (f := CommRingCat.ofHom (algebraMap R S)) hsq.flip hRS

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.of_isPushout, CategoryTheory.IsPushout.flip