awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
heq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsIso (IsLimit.lift (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (Fork.ofι h' w')) ↔
    Function.Bijective (α := TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
      (β :=
      ↥(AlgHom.equalizer (F :=
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
      (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (toAlgHom f) (toAlgHom g)) :
        (a : TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) →
          ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f))
              (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g))))

Tactic:
rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
    ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.Under.forget, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
heq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
rw :
  Function.Bijective (α :=
    TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)))
    (β :=
    ↥(AlgHom.equalizer (F :=
        TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
          TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
    (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)) :
      (a :
          TensorProduct (↑R : Type u) (↑S : Type u)
            ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))) →
        ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f))
            (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g))))
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)

Tactic:
rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]

Premises used: CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ Function.Bijective (α :=
    TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)))
    (β :=
    ↥(AlgHom.equalizer (F :=
        TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
          TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
    (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)) :
      (a :
          TensorProduct (↑R : Type u) (↑S : Type u)
            ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))) →
        ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f))
            (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g))))

Tactic:
hPse _ _ hA hB

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ Function.Bijective (α :=
    TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)))
    (β :=
    ↥(AlgHom.equalizer (F :=
        TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
          TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
        (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g) :
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
    (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)) :
      (a :
          TensorProduct (↑R : Type u) (↑S : Type u)
            ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))) →
        ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f))
            (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g))))

Tactic:
exact hPse _ _ hA hB
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
⊢ PreservesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
⟨fun {K} ↦ ?_⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.mk
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
refine :
  ∀ {K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R},
    PreservesLimit K
      (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
⊢ PreservesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
refine ⟨fun {K} ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
have :
  ∀
    (this :
      CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
        WalkingParallelPair
        (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)),
    PreservesLimit K
      (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
have := hPe.createsLimitsWalkingParallelPair hPi R
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
rw :
  PreservesLimit
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)
⊢ PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)

Tactic:
rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]

Premises used: CommRingCat.ofHom_hom, CommRingCat.tensorProdIsoPushout, CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Limits.preservesLimit_iff_of_iso_diagram, CategoryTheory.Limits.preservesLimit_iff_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)

Tactic:
hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)

Premises used: CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Functor.obj, RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit
    (parallelPair
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.left)
      ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
        WalkingParallelPairHom.right))
    (R.tensorProd S)

Tactic:
exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)

Premises used: CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Functor.obj, RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)

Tactic:
have : PreservesLimit (K ⋙ Under.forget (toMorphismProperty P) ⊤ R)
      (CategoryTheory.Under.pushout f) := by
    rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
    exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
rw :
  PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R ⋙
      CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)

Tactic:
rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]

Premises used: CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso, CategoryTheory.Limits.preservesLimit_iff_of_natIso
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R ⋙
      CategoryTheory.Under.pushout f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)

Tactic:
have : PreservesLimit K (Under.pushout (toMorphismProperty P) ⊤ f ⋙
        Under.forget (toMorphismProperty P) ⊤ S) := by
    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
    infer_instance