awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
h : _root_.Finite J
A : Under R
h_1 :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres :
  ∀ (j : Discrete J), (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u)) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y := limit (J := Discrete J) (Discrete.functor fun (i : J) ↦ pres.diag.obj { as := i }))
      (HasLimit.isoOfNatIso (Discrete.natIso fun (i : Discrete J) ↦ eqToIso ⋯))
      (limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun (i : J) ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun (i : J) ↦ pres.diag.obj { as := i : Discrete J } }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u))).hom

Tactic:
hQp _ fun i ↦ hpres _

Premises used: Pi.ringHom, CategoryTheory.Discrete.mk, RingHom.toMorphismProperty
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
h : _root_.Finite J
A : Under R
h_1 :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres :
  ∀ (j : Discrete J), (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u)) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y := limit (J := Discrete J) (Discrete.functor fun (i : J) ↦ pres.diag.obj { as := i }))
      (HasLimit.isoOfNatIso (Discrete.natIso fun (i : Discrete J) ↦ eqToIso ⋯))
      (limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun (i : J) ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun (i : J) ↦ pres.diag.obj { as := i : Discrete J } }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u))).hom

Tactic:
exact hQp _ fun i ↦ hpres _
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj WalkingParallelPair

Tactic:
⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩

Premises used: _private.0.RingHom.HasEqualizers.isClosedUnderLimitsOfShape.match_1, CategoryTheory.MorphismProperty.underObj, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk, RingHom.toMorphismProperty
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
refine :
  ∀ (A : Under R),
    ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
        WalkingParallelPair A →
      ∀ (pres : LimitPresentation WalkingParallelPair A)
        (hpres :
          ∀ (j : WalkingParallelPair),
            (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)),
        (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj WalkingParallelPair

Tactic:
refine ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso

Tactic:
have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
rw :
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder
        ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
            (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right)))).hom
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]

Premises used: RingHom.toMorphismProperty, CategoryTheory.MorphismProperty.underObj_iff, CategoryTheory.Iso.inv, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Under.w
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder
        ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
            (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right)))).hom

Tactic:
hQe _ _ (hpres .zero) (hpres .one)

Premises used: Set.Mem, CategoryTheory.Limits.WalkingParallelPair.one, RingHom.toMorphismProperty, RingHom.codRestrict, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder
        ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
            (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right)))).hom

Tactic:
exact hQe _ _ (hpres .zero) (hpres .one)

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
refine :
  (J : Type u) →
    Fintype J →
      CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
        (Discrete J)
        (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)

Tactic:
refine .mk' _ fun (J : Type u) _ ↦ ?_
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x : Fintype J
inst :
  ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (Discrete J)
⊢ CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (Discrete J)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)

Tactic:
apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed

Premises used: CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x : Fintype J
⊢ ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj

Tactic:
have := hQp.isClosedUnderLimitsOfShape hQi R
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x : Fintype J
this :
  ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (Discrete J)

Tactic:
inferInstanceAs <| (toMorphismProperty Q).underObj.IsClosedUnderLimitsOfShape _

Premises used: RingHom.HasFiniteProducts.createsFiniteProductsForget._proof_1
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x : Fintype J
this :
  ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (Discrete J)

Tactic:
exact inferInstanceAs <| (toMorphismProperty Q).underObj.IsClosedUnderLimitsOfShape _
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ Limits.HasFiniteProducts.{u, u + 1} ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.HasFiniteProducts.mk
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
refine :
  ∀ (n : ℕ) (D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R),
    HasLimit D
⊢ Limits.HasFiniteProducts.{u, u + 1} ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
n : ℕ
D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
have :
  ∀
    (this :
      CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
        (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)),
    HasLimit D
⊢ HasLimit D

Tactic:
have := hQp.createsFiniteProductsForget hQi R
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
n : ℕ
D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D

Tactic:
CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.MorphismProperty.Under.forget
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
n : ℕ
D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D

Tactic:
exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.MorphismProperty.Under.forget
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
have :
  ∀
    (this :
      CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
        (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)),
    PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
      (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
⊢ PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
have := hQp.createsFiniteProductsForget hQi R
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩

Premises used: CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
refine :
  ∀ (n : ℕ) {K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R},
    PreservesLimit K
      (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
⊢ PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
refine ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩