awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  Function.Surjective (α := (↑P : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) π) :
      (a : (↑P : Type u)) → (↑S : Type u))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : (r : ↥s) → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' :
  ∀ (r : ↥s),
    Eq (α := (↑(F.obj (i' r)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map (hi' r)) :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj (i' r)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj (i' r)) : Type u))
      (0 : (↑(F.obj (i' r)) : Type u))
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
r : (↑P : Type u)
hr : r ∈ (↑s : Set (↑P : Type u))
⊢ r ∈
    (↑(ker (F := (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u)) (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)))) :
      Set (↑P : Type u))
have refine_1 : r ∈
  (↑(ker
        (CommRingCat.Hom.hom
          (g' ≫
            F.map
              ((WidePushoutShape.wideSpan i i' hi').map
                  (WidePushoutShape.Hom.init (Subtype.mk (p := fun (x : (↑P : Type u)) ↦ x ∈ s) r hr)) ≫
                c'.ι.app (some (Subtype.mk (p := fun (x : (↑P : Type u)) ↦ x ∈ s) r hr)))))) :
    Set (↑P : Type u))
Tactic: rw [← c'.w (.init ⟨r, hr⟩)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
⊢ PreservesColimit F (Functor.obj coyoneda (Opposite.op S))
have preserves : ∀ {c : Cocone F} (hc : IsColimit c),
  Nonempty
    (IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
⊢ Nonempty
    (IsColimit (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c))
have preserves : ∀
  (x :
    Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
      (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi
Tactic: refine ⟨Types.FilteredColimit.isColimitOf _ _ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi
have preserves : ∀ (i : J) (g : S.right ⟶ (F ⋙ Under.forget R).obj i)
  (h₁ : S.hom ≫ g = NatTrans.app { app := fun (i : J) ↦ (F.obj i).hom, naturality := sorry } i)
  (h₂ : Under.Hom.right f = g ≫ NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget R) c)) i),
  ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi
Tactic: obtain ⟨i, g, h₁, h₂⟩ := RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit
       R (F ⋙ Under.forget R) { app i := (F.obj i).hom } S.hom ((Under.forget R).mapCocone c)
      (PreservesColimit.preserves hc).some hS f.right (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ IsFinitelyPresentable S
have rw : PreservesFilteredColimits (Functor.obj coyoneda (Opposite.op S))
Tactic: rw [isFinitelyPresentable_iff_preservesFilteredColimits]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Instances (goal)
Goal:
R : CommRingCat
⊢ IsIso.{u_1, u_1 + 1} (X := R) (Y := CommRingCat.of (Localization.Away (M := (↑R : Type u_1)) 1))
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away (M := (↑R : Type u_1)) 1)))
have of : ∀ (carrier : Type u_1) [commRing : CommRing carrier],
  IsIso.{u_1, u_1 + 1} (X := CommRingCat.of carrier) (Y :=
    CommRingCat.of (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1))
    (CommRingCat.ofHom
      (algebraMap (↑(CommRingCat.of carrier) : Type u_1)
        (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1)))
Tactic: cases R
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Instances (goal)
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u_1)
⊢ Epi.{u_1, u_1 + 1} (X := R) (Y := CommRingCat.of (Localization M))
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization M)))
have rcases : ∀ (α : Type u_1) [commRing : CommRing α] (M : Submonoid (↑(CommRingCat.of α) : Type u_1)),
  Epi.{u_1, u_1 + 1} (X := CommRingCat.of α) (Y := CommRingCat.of (Localization M))
    (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of α) : Type u_1) (Localization M)))
Tactic: rcases R with ⟨α, str⟩
Cleared hypotheses: R, M
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Instances (goal)
Goal:
R S : CommRingCat
f : R ≅ S
a : (↑R : Type u_1)
ha :
  IsUnit (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
⊢ IsUnit a
have h : a =
  (CommRingCat.Hom.hom f.inv : (a : (↑S : Type u_1)) → (↑R : Type u_1))
    ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
Tactic: convert! f.inv.hom.isUnit_map ha
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    Functor.obj.{w, u, v, u + 1}
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        f ≫
      ofHom (limitπRingHom F x_1))
    (ofHom (limitπRingHom F x) ≫ F.map f)
have hf : ∀
  (x_2 :
    (↑(Functor.obj.{w, u, v, u + 1}
          (Functor.obj (Functor.const J)
            (of
              (Types.Small.limitCone
                  (F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier))).pt))
          x) :
      Type u)),
  Eq (α := (↑(F.obj x_1) : Type u))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of
                    (Types.Small.limitCone
                        (F ⋙
                          forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := carrier))).pt))
                f ≫
              ofHom (limitπRingHom F x_1)) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))
    ((Hom.hom (ofHom (limitπRingHom F x) ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ IsLimit (limitCone F)
have refine_1 : ∀ (s : Cone F),
  EquivLike.coe (E :=
      (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)) ≃
        Shrink.{u, max u v}
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
      (equivShrink
        (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).obj
                j) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier))
                      s))
                  j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
            1)
        sorry) =
    1
Tactic: refine IsLimit.ofFaithful (forget SemiRingCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_ })
    (fun s => rfl)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P
have 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
Tactic: obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
have refine : ∀ (S : CommRingCat.{u}) (hS : P S), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
Tactic: refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have obtain : ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType),
  ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
Tactic: obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: wlog hR' : Q' R generalizing R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have wlog : ∀ (R : CommRingCat.{u}) (hR : Q R) (φ : R ⟶ S) (hφ : (Hom.hom φ).FiniteType) (hR' : Q' R),
  ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
Tactic: wlog hR' : Q' R generalizing R
Cleared hypotheses: R, hR, φ, hφ
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have inr : ∀ (R' : CommRingCat.{u}) (hR' : Q' R') (e : R ≅ R'), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
Tactic: obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR