awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
G : ℕ ⥤ MonoOver.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) n :
          Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) m :
          Subobject.{v, u} X)
refine_1 : ∀ (m : ℕ) (hm : n ⟶ m), IsIso (G.map hm)
⊢ IsFiltered.IsEventuallyConstant G

Tactic:
refine ⟨n, fun m hm ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
G : ℕ ⥤ MonoOver.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) n :
          Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) m :
          Subobject.{v, u} X)
m : ℕ
hm : n ⟶ m
refine_1 : Subobject.mk (G.obj n).obj (P := Over.isMono X).hom = Subobject.mk (G.obj m).obj (P := Over.isMono X).hom
⊢ IsIso (G.map hm)

Tactic:
rw [MonoOver.isIso_iff_subobjectMk_eq]

Premises used: CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
G : ℕ ⥤ MonoOver.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) n :
          Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) m :
          Subobject.{v, u} X)
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (G.obj n).obj (P := Over.isMono X).hom = Subobject.mk (G.obj m).obj (P := Over.isMono X).hom

Tactic:
hn m (leOfHom hm)

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.MonoOver.mk, CategoryTheory.CostructuredArrow, CategoryTheory.Subobject.mk, Quotient.mk', CategoryTheory.CostructuredArrow.mk, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
G : ℕ ⥤ MonoOver.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) n :
          Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) m :
          Subobject.{v, u} X)
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (G.obj n).obj (P := Over.isMono X).hom = Subobject.mk (G.obj m).obj (P := Over.isMono X).hom

Tactic:
exact hn m (leOfHom hm)

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject.{v, u} X
refine_2 :
  ∀ (n : ℕ) (hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ Subobject.representative)

Premises used: OrderHom.monotone, CategoryTheory.Functor.comp, Monotone.functor, CategoryTheory.Subobject.representative
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject.{v, u} X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
⟨n, fun m hm ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject.{v, u} X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
refine_2 :
  ∀ (m : ℕ) (hm : n ≤ m),
    Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
      ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
refine ⟨n, fun m hm ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject.{v, u} X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
m : ℕ
hm : n ≤ m
⊢ Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
    ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
simpa [← MonoOver.isIso_iff_isIso_hom_left, isIso_iff_of_reflects_iso,
      PartialOrder.isIso_iff_eq] using hn (homOfLE hm)

Premises used: PartialOrder.isIso_iff_eq, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.MonoOver.isIso_iff_isIso_hom_left, CategoryTheory.homOfLE
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : IsNoetherianObject.{v, u} X
F : ℕ ⥤ MonoOver.{v, u} X
⊢ IsFiltered.IsEventuallyConstant F

Tactic:
(isNoetherianObject_iff_isEventuallyConstant X).1 inferInstance F

Premises used: inferInstance, Iff.mp, CategoryTheory.isNoetherianObject_iff_isEventuallyConstant
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
rw :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
⊢ IsNoetherianObject.{v, u} X

Tactic:
rw [isNoetherianObject_iff_monotone_chain_condition]

Premises used: CategoryTheory.isNoetherianObject_iff_monotone_chain_condition
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
⊢ Subsingleton (Subobject.{v, u} X)

Tactic:
have := Subobject.subsingleton_of_isZero hX
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
this : Subsingleton (Subobject.{v, u} X)
f : ℕ →o Subobject.{v, u} X
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
⟨0, fun m hm ↦ Subsingleton.elim _ _⟩

Premises used: Exists.intro, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
this : Subsingleton (Subobject.{v, u} X)
f : ℕ →o Subobject.{v, u} X
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
exact ⟨0, fun m hm ↦ Subsingleton.elim _ _⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroObject.{v, u} C
rw : ObjectProperty.Is.{v, u} (C := C) isNoetherianObject 0
⊢ isNoetherianObject.{v, u} (C := C) 0

Tactic:
rw [← isNoetherianObject.is_iff]

Premises used: CategoryTheory.ObjectProperty.is_iff, CategoryTheory.isNoetherianObject
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroObject.{v, u} C
⊢ ObjectProperty.Is.{v, u} (C := C) isNoetherianObject 0

Tactic:
isNoetherianObject_of_isZero (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.isNoetherianObject_of_isZero
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroObject.{v, u} C
⊢ ObjectProperty.Is.{v, u} (C := C) isNoetherianObject 0

Tactic:
exact isNoetherianObject_of_isZero (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.isNoetherianObject_of_isZero
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
rw :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
⊢ IsNoetherianObject.{v, u} X

Tactic:
rw [isNoetherianObject_iff_monotone_chain_condition]

Premises used: CategoryTheory.isNoetherianObject_iff_monotone_chain_condition
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
f : ℕ →o Subobject.{v, u} X
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} Y)
            (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
                  (a : ℕ) → Subobject Y)
                n :
              Subobject.{v, u} Y)
            (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
                  (a : ℕ) → Subobject Y)
                m :
              Subobject.{v, u} Y)),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
obtain ⟨n, hn⟩ := monotone_chain_condition_of_isNoetherianObject
    ⟨_, (Subobject.map i).monotone.comp f.2⟩

Premises used: CategoryTheory.Subobject.map, Monotone.comp, CategoryTheory.Functor.monotone, CategoryTheory.monotone_chain_condition_of_isNoetherianObject, OrderHom.mk, OrderHom.monotone'
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
f : ℕ →o Subobject.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} Y)
        (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
              (a : ℕ) → Subobject Y)
            n :
          Subobject.{v, u} Y)
        (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
              (a : ℕ) → Subobject Y)
            m :
          Subobject.{v, u} Y)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

Premises used: Exists.intro, CategoryTheory.Subobject.map_obj_injective
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
f : ℕ →o Subobject.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} Y)
        (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
              (a : ℕ) → Subobject Y)
            n :
          Subobject.{v, u} Y)
        (({ toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ : ℕ →o Subobject.{v, u} Y } :
              (a : ℕ) → Subobject Y)
            m :
          Subobject.{v, u} Y)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)

Tactic:
exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
hY : isNoetherianObject.{v, u} Y_1
rw : ∀ (hY : ObjectProperty.Is.{v, u} isNoetherianObject Y_1), ObjectProperty.Is.{v, u} isNoetherianObject X_1
⊢ isNoetherianObject.{v, u} X_1

Tactic:
rw [← isNoetherianObject.is_iff] at hY ⊢

Premises used: CategoryTheory.ObjectProperty.is_iff, CategoryTheory.isNoetherianObject
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
hY : ObjectProperty.Is.{v, u} isNoetherianObject Y_1
⊢ ObjectProperty.Is.{v, u} isNoetherianObject X_1

Tactic:
isNoetherianObject_of_mono f

Premises used: CategoryTheory.isNoetherianObject_of_mono
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
hY : ObjectProperty.Is.{v, u} isNoetherianObject Y_1
⊢ ObjectProperty.Is.{v, u} isNoetherianObject X_1

Tactic:
exact isNoetherianObject_of_mono f

Premises used: CategoryTheory.isNoetherianObject_of_mono
-- Module: Mathlib.CategoryTheory.Subobject.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
x : Cᵒᵖ
h :
  ∀ (x_1 : Subobject.{v, u} (Opposite.unop x)),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))))) x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Subobject.{v, u} (Opposite.unop x)))).toFun x_1
⊢ ↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))) = 𝟙 (Subobject.{v, u} (Opposite.unop x))

Tactic:
ext : 3
-- Module: Mathlib.CategoryTheory.Subobject.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
x : Cᵒᵖ
x_1 : Subobject.{v, u} (Opposite.unop x)
⊢ TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (↾Functor.obj (pullback (Quiver.Hom.unop (𝟙 x))))) x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Subobject.{v, u} (Opposite.unop x)))).toFun x_1

Tactic:
simp [pullback_id]

Premises used: CategoryTheory.Subobject.pullback_id
-- Module: Mathlib.CategoryTheory.Subobject.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
X Y Z : Cᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  ∀ (x_2 : Subobject.{v, u} (Opposite.unop X)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback (x ≫ x_1).unop).obj)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj)).toFun x_2
⊢ ↾(pullback (x ≫ x_1).unop).obj = ↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj

Tactic:
ext : 3
-- Module: Mathlib.CategoryTheory.Subobject.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasPullbacks.{v, u} C
X Y Z : Cᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
x_2 : Subobject.{v, u} (Opposite.unop X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback (x ≫ x_1).unop).obj)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾(pullback x.unop).obj ≫ ↾(pullback x_1.unop).obj)).toFun x_2

Tactic:
simp [pullback_comp]

Premises used: CategoryTheory.Subobject.pullback_comp
-- Module: Mathlib.CategoryTheory.Subobject.Types
Goal:
α : Type u
s : Set α
⊢ Mono.{u, u + 1} (X := { x : α // x ∈ s }) (↾Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
(mono_iff_injective _).mpr Subtype.val_injective

Premises used: Iff.mpr, Subtype.val_injective, CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Subobject.Types
Goal:
α : Type u
f g : MonoOver α
t : f ⟶ g
x : f.obj (P := Over.isMono α).left
⊢ Membership.mem (α := α) (γ := Set α)
    (Set.range (ι := (fun (X : Type u) ↦ X) g.obj (P := Over.isMono α).left)
      (⇑(hom (FC := TypeCat.Fun) g.obj (P := Over.isMono α).hom) :
        (a : (fun (X : Type u) ↦ X) g.obj.left) → (fun (X : Type u) ↦ X) α))
    ((hom (FC := TypeCat.Fun) f.obj (P := Over.isMono α).hom :
          (a : (fun (X : Type u) ↦ X) f.obj.left) → (fun (X : Type u) ↦ X) α)
        x :
      (fun (X : Type u) ↦ X) α)

Tactic:
⟨t.hom.1 x, congr_hom t.hom.w x⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, CategoryTheory.CommaMorphism.left, Exists.intro, Set.range, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Subobject.Types
Goal:
α : Type u
f g : MonoOver α
t : f ⟶ g
x : f.obj (P := Over.isMono α).left
⊢ Membership.mem (α := α) (γ := Set α)
    (Set.range (ι := (fun (X : Type u) ↦ X) g.obj (P := Over.isMono α).left)
      (⇑(hom (FC := TypeCat.Fun) g.obj (P := Over.isMono α).hom) :
        (a : (fun (X : Type u) ↦ X) g.obj.left) → (fun (X : Type u) ↦ X) α))
    ((hom (FC := TypeCat.Fun) f.obj (P := Over.isMono α).hom :
          (a : (fun (X : Type u) ↦ X) f.obj.left) → (fun (X : Type u) ↦ X) α)
        x :
      (fun (X : Type u) ↦ X) α)

Tactic:
exact ⟨t.hom.1 x, congr_hom t.hom.w x⟩
-- Module: Mathlib.CategoryTheory.Subobject.Types
Goal:
⊢ WellPowered.{u, u, u + 1} (Type u)

Tactic:
wellPowered_of_essentiallySmall_monoOver fun α =>
    EssentiallySmall.mk' (Types.monoOverEquivalenceSet α)

Premises used: CategoryTheory.EssentiallySmall.mk', Types.monoOverEquivalenceSet, CategoryTheory.wellPowered_of_essentiallySmall_monoOver
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
inst_1 : LocallySmall.{w, v, u₁} C
inst_2 : WellPowered.{w, v, u₁} C
X : C
⊢ Small.{w, max u₁ v} (Subobject.{v, u₁} X)

Tactic:
WellPowered.subobject_small X

Premises used: CategoryTheory.WellPowered.subobject_small
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : C
⊢ EssentiallySmall.{w, v, max u₁ v} (MonoOver.{v, u₁} X) ↔ Small.{w, max u₁ v} (Subobject.{v, u₁} X)

Tactic:
essentiallySmall_iff_of_thin

Premises used: CategoryTheory.ThinSkeleton, CategoryTheory.InducedCategory, CategoryTheory.Subobject, CategoryTheory.Skeleton, CategoryTheory.essentiallySmall_iff_of_thin
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
inst_1 : LocallySmall.{w, v, u₁} C
h : ∀ (X : C), EssentiallySmall.{w, v, max u₁ v} (MonoOver.{v, u₁} X)
⊢ WellPowered.{w, v, u₁} C

Tactic:
{ subobject_small := fun X => (essentiallySmall_monoOver_iff_small_subobject X).mp (h X) }

Premises used: CategoryTheory.WellPowered.mk, Iff.mp, CategoryTheory.essentiallySmall_monoOver_iff_small_subobject
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
inst_1 : LocallySmall.{w, v, u₁} C
inst_2 : WellPowered.{w, v, u₁} C
X : C
⊢ EssentiallySmall.{w, v, max u₁ v} (MonoOver.{v, u₁} X)

Tactic:
(essentiallySmall_monoOver_iff_small_subobject X).mpr (WellPowered.subobject_small X)

Premises used: Iff.mpr, CategoryTheory.WellPowered.subobject_small, CategoryTheory.essentiallySmall_monoOver_iff_small_subobject
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v, v₂, u₁, u₂} C D
inst_2 : LocallySmall.{w, v, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
inst_4 : WellPowered.{w, v, u₁} C
X : D
⊢ EssentiallySmall.{w, v, max u₁ v} (MonoOver.{v, u₁} (e.symm.functor.obj X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v, v₂, u₁, u₂} C D
inst_2 : LocallySmall.{w, v, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ WellPowered.{w, v, u₁} C ↔ WellPowered.{w, v₂, u₂} D

Tactic:
⟨fun _ => wellPowered_of_equiv e, fun _ => wellPowered_of_equiv e.symm⟩

Premises used: CategoryTheory.wellPowered_of_equiv, Iff.intro, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Subobject.WellPowered
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v, u₁} C
inst_3 : WellPowered.{w, v, u₁} C
⊢ WellPowered.{w, w, u₁} (ShrinkHoms.{u₁} C)

Tactic:
wellPowered_of_equiv.{w} (ShrinkHoms.equivalence.{w} C)

Premises used: CategoryTheory.wellPowered_of_equiv, CategoryTheory.ShrinkHoms.equivalence
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
⊢ IsSubterminal.{v₁, u₁} A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.IsSubterminal
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
hA : IsSubterminal.{v₁, u₁} A
T : C
hT : IsTerminal.{v₁, u₁} T
⊢ Mono (hT.from A)

Tactic:
{ right_cancellation := fun _ _ _ => hA _ _ }

Premises used: CategoryTheory.Mono.mk
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
hA : IsSubterminal.{v₁, u₁} A
⊢ Mono.{v₁, u₁} (Y := terminal.{v₁, u₁} C) (terminal.from A)

Tactic:
hA.mono_isTerminal_from terminalIsTerminal

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.IsSubterminal.mono_isTerminal_from, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A T : C
hT : IsTerminal.{v₁, u₁} T
inst_1 : Mono (hT.from A)
Z : C
f g : Z ⟶ A
rw : f ≫ hT.from A = g ≫ hT.from A
⊢ f = g

Tactic:
rw [← cancel_mono (hT.from A)]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A T : C
hT : IsTerminal.{v₁, u₁} T
inst_1 : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ hT.from A = g ≫ hT.from A

Tactic:
apply hT.hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
inst_2 : Mono.{v₁, u₁} (Y := terminal.{v₁, u₁} C) (terminal.from A)
Z : C
f g : Z ⟶ A
rw : Eq (α := Z ⟶ terminal.{v₁, u₁} C) (f ≫ terminal.from A) (g ≫ terminal.from A)
⊢ f = g

Tactic:
rw [← cancel_mono (terminal.from A)]

Premises used: CategoryTheory.Limits.terminal.from, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
inst_2 : Mono.{v₁, u₁} (Y := terminal.{v₁, u₁} C) (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ Eq (α := Z ⟶ terminal.{v₁, u₁} C) (f ≫ terminal.from A) (g ≫ terminal.from A)

Tactic:
subsingleton