awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
      (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))

Tactic:
RingCat.forget₂SemiRing_preservesLimitsOfSize.{u, u}

Premises used: RingCat.forget₂SemiRing_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
h : Small.{u, max u v}
  (↑((F ⋙
            forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier)) ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier)).sections :
    Type (max u v)) :=
  ⋯
⊢ IsLimit (F :=
    F ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) AddCommGrpCat
        (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) AddCommGrpCat
        (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))
      (limitCone F))

Tactic:
apply AddCommGrpCat.limitConeIsLimit.{v, u} _
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) AddCommGrpCat
      (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))

Tactic:
RingCat.forget₂AddCommGroup_preservesLimitsOfSize.{u, u}

Premises used: RingCat.forget₂AddCommGroup_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ PreservesLimits (forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
RingCat.forget_preservesLimitsOfSize.{u, u}

Premises used: RingCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  hasLimit_of_created F (forget₂ CommRingCat.{u} RingCat.{u})

Premises used: CategoryTheory.hasLimit_of_created, CommRingCat, RingCat, CategoryTheory.forget₂, CommRingCat.instCreatesLimitRingCatForget₂RingHomCarrierCarrier._proof_1
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimits CommRingCat

Tactic:
CommRingCat.hasLimitsOfSize.{u, u}

Premises used: CommRingCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) RingCat
      (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := RingCat.carrier))

Tactic:
CommRingCat.forget₂Ring_preservesLimitsOfSize.{u, u}

Premises used: CommRingCat.forget₂Ring_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
h : Small.{u, max u v}
  (↑((F ⋙
            forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              CommSemiRingCat (FD := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              CommSemiRingCat.carrier)) ⋙
          forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommSemiRingCat.carrier)).sections :
    Type (max u v)) :=
  ⋯
⊢ IsLimit (F :=
    F ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
        CommSemiRingCat (FD := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        CommSemiRingCat.carrier))
    (Functor.mapCone
      (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
        CommSemiRingCat (FD := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        CommSemiRingCat.carrier))
      (limitCone F))

Tactic:
apply CommSemiRingCat.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRingCat.{u})
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
      CommSemiRingCat (FD := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
      CommSemiRingCat.carrier))

Tactic:
CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize.{u, u}

Premises used: CommRingCat.forget₂CommSemiRing_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
CommRingCat.forget_preservesLimitsOfSize.{u, u}

Premises used: CommRingCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.LinearAlgebra
Goal:
A B C D : CommRingCat
hA : IsField.{u} (↑A : Type u)
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst : Nontrivial.{u} (↑B : Type u)
inst_1 : Nontrivial.{u} (↑C : Type u)
h : IsPushout f g inl inr
this : Field (↑A : Type u) := hA.toField
algInst : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑A : Type u) (↑C : Type u) := (Hom.hom g).toAlgebra
e : D ≅ of ((↑B : Type u) ⊗[(↑A : Type u)] (↑C : Type u)) :=
  h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit (↑A : Type u) (↑B : Type u) (↑C : Type u))
e' : (↑D : Type u) ≃ (↑B : Type u) ⊗[(↑A : Type u)] (↑C : Type u) := e.commRingCatIsoToRingEquiv.toEquiv
⊢ Nontrivial.{u} (↑D : Type u)

Tactic:
e'.nontrivial

Premises used: Equiv.nontrivial
-- Module: Mathlib.Algebra.Category.Ring.LinearAlgebra
Goal:
A B C D : CommRingCat
hA : IsField.{u} (↑A : Type u)
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst : Nontrivial.{u} (↑B : Type u)
inst_1 : Nontrivial.{u} (↑C : Type u)
h : IsPushout f g inl inr
this : Field (↑A : Type u) := hA.toField
algInst : Algebra (↑A : Type u) (↑B : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑A : Type u) (↑C : Type u) := (Hom.hom g).toAlgebra
e : D ≅ of ((↑B : Type u) ⊗[(↑A : Type u)] (↑C : Type u)) :=
  h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit (↑A : Type u) (↑B : Type u) (↑C : Type u))
e' : (↑D : Type u) ≃ (↑B : Type u) ⊗[(↑A : Type u)] (↑C : Type u) := e.commRingCatIsoToRingEquiv.toEquiv
⊢ Nontrivial.{u} (↑D : Type u)

Tactic:
exact e'.nontrivial

Premises used: Equiv.nontrivial
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
obtain :
  ∀ (Q' : ObjectProperty CommRingCat),
    ObjectProperty.Small.{u, u, u + 1} Q' →
      ∀ (hQ'Q : Q' ≤ Q) (hQQ' : Q ≤ Q'.isoClosure), ObjectProperty.EssentiallySmall.{u, u, u + 1} P
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, inferInstance, Exists.intro, CategoryTheory.ObjectProperty.EssentiallySmall.mk
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
refine : ∀ (S : CommRingCat.{u}) (hS : P S), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
obtain :
  ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
inr :
  ∀
    (this :
      ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
        ObjectProperty.isoClosure (ObjectProperty.ofObj f) S)
    (hR' : ¬Q' R), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
wlog :
  ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
wlog hR' : Q' R generalizing R
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
this :
  ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hR' : ¬Q' R
inr : ∀ (R' : CommRingCat.{u}) (hR' : Q' R') (e : R ≅ R'), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
this :
  ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hR'_1 : ¬Q' R
R' : CommRingCat
hR' : Q' R'
e : R ≅ R'
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
this R' (hQ'Q _ hR') (e.inv ≫ φ)
      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingHom.Finite.finiteType, RingEquiv.finite, RingHom.FiniteType.comp, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
this :
  ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hR'_1 : ¬Q' R
R' : CommRingCat
hR' : Q' R'
e : R ≅ R'
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
exact this R' (hQ'Q _ hR') (e.inv ≫ φ)
      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingHom.Finite.finiteType, RingEquiv.finite, RingHom.FiniteType.comp, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv