awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
refine_1 :
  ∀
    (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)ᵒᵖ), IsFiltered.IsEventuallyConstant G
refine_2 :
  ∀ (h : ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F) (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)ᵒᵈ)
⊢ (∀ (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)ᵒᵈ)) ↔
    ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F

Tactic:
refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵖ
refine_1 :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} X)ᵒᵈ)
            (({
                    toFun :=
                      (G ⋙
                          Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                            Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                    monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
                  (a : ℕ) → (Subobject X)ᵒᵈ)
                n :
              (Subobject.{v, u} X)ᵒᵈ)
            (({
                    toFun :=
                      (G ⋙
                          Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                            Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                    monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
                  (a : ℕ) → (Subobject X)ᵒᵈ)
                m :
              (Subobject.{v, u} X)ᵒᵈ)),
    IsFiltered.IsEventuallyConstant G
⊢ IsFiltered.IsEventuallyConstant G

Tactic:
obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙
      (orderDualEquivalence _).inverse).monotone⟩

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.comp, CategoryTheory.Subobject.equivMonoOver, CategoryTheory.Functor.monotone, OrderHom.mk, CategoryTheory.orderDualEquivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
⊢ IsFiltered.IsEventuallyConstant G

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

Premises used: CategoryTheory.IsFiltered.IsEventuallyConstant.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (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.ArtinianObject
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)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
m : ℕ
hm : n ⟶ m
refine_1 :
  Subobject.mk (Opposite.unop (G.obj m)).obj (P := Over.isMono X).hom =
    Subobject.mk (Opposite.unop (G.obj n)).obj (P := Over.isMono X).hom
⊢ IsIso (G.map hm)

Tactic:
rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]

Premises used: CategoryTheory.isIso_unop_iff, CategoryTheory.MonoOver.isIso_iff_subobjectMk_eq
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (Opposite.unop (G.obj m)).obj (P := Over.isMono X).hom =
    Subobject.mk (Opposite.unop (G.obj n)).obj (P := Over.isMono X).hom

Tactic:
(hn m (leOfHom hm)).symm

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.MonoOver.mk, CategoryTheory.CostructuredArrow, CategoryTheory.ThinSkeleton, CategoryTheory.Subobject.mk, Quotient, Quotient.mk', CategoryTheory.CostructuredArrow.mk, Eq.symm, CategoryTheory.leOfHom, CategoryTheory.Subobject
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            n :
          (Subobject.{v, u} X)ᵒᵈ)
        (({
                toFun :=
                  (G ⋙
                      Functor.op (Equivalence.inverse (Subobject.equivMonoOver X)) ⋙
                        Equivalence.inverse (orderDualEquivalence (Subobject.{v, u} X))).obj,
                monotone' := ⋯ : ℕ →o (Subobject.{v, u} X)ᵒᵈ } :
              (a : ℕ) → (Subobject X)ᵒᵈ)
            m :
          (Subobject.{v, u} X)ᵒᵈ)
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (Opposite.unop (G.obj m)).obj (P := Over.isMono X).hom =
    Subobject.mk (Opposite.unop (G.obj n)).obj (P := Over.isMono X).hom

Tactic:
exact (hn m (leOfHom hm)).symm

Premises used: Eq.symm, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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 ⋙
            Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
              Functor.op 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 ⋙ (orderDualEquivalence _).functor ⋙
      Subobject.representative.op)

Premises used: CategoryTheory.Functor.op, OrderHom.monotone, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, Monotone.functor, CategoryTheory.Subobject.representative, CategoryTheory.orderDualEquivalence
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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 ⋙
        Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
          Functor.op 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 ↦ Eq.symm ?_⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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 ⋙
        Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
          Functor.op Subobject.representative).IsEventuallyConstantFrom
    n
refine_2 :
  ∀ (m : ℕ) (hm : n ≤ m),
    Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
      ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (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 ↦ Eq.symm ?_⟩
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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 ⋙
        Equivalence.functor (orderDualEquivalence (Subobject.{v, u} X)) ⋙
          Functor.op Subobject.representative).IsEventuallyConstantFrom
    n
m : ℕ
hm : n ≤ m
⊢ Eq (α := (Subobject.{v, u} X)ᵒᵈ) ((F : (a : ℕ) → (Subobject X)ᵒᵈ) m : (Subobject.{v, u} X)ᵒᵈ)
    ((F : (a : ℕ) → (Subobject X)ᵒᵈ) n : (Subobject.{v, u} X)ᵒᵈ)

Tactic:
simpa [isIso_op_iff, 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.homOfLE, CategoryTheory.isIso_op_iff
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : IsArtinianObject.{v, u} X
F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ
⊢ IsFiltered.IsEventuallyConstant F

Tactic:
(isArtinianObject_iff_isEventuallyConstant X).1 inferInstance F

Premises used: inferInstance, Iff.mp, CategoryTheory.isArtinianObject_iff_isEventuallyConstant
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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)ᵒᵈ)
⊢ IsArtinianObject.{v, u} X

Tactic:
rw [isArtinianObject_iff_antitone_chain_condition]

Premises used: CategoryTheory.isArtinianObject_iff_antitone_chain_condition
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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.ArtinianObject
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.ArtinianObject
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.ArtinianObject
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) isArtinianObject 0
⊢ isArtinianObject.{v, u} (C := C) 0

Tactic:
rw [← isArtinianObject.is_iff]

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

Tactic:
isArtinianObject_of_isZero (isZero_zero C)

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

Tactic:
exact isArtinianObject_of_isZero (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.isArtinianObject_of_isZero
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{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)ᵒᵈ)
⊢ IsArtinianObject.{v, u} X

Tactic:
rw [isArtinianObject_iff_antitone_chain_condition]

Premises used: CategoryTheory.isArtinianObject_iff_antitone_chain_condition
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{v, u} Y
f : ℕ →o (Subobject.{v, u} X)ᵒᵈ
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := (Subobject.{v, u} Y)ᵒᵈ)
            (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
                  (a : ℕ) → (Subobject Y)ᵒᵈ)
                n :
              (Subobject.{v, u} Y)ᵒᵈ)
            (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
                  (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⟩ := antitone_chain_condition_of_isArtinianObject
    ⟨fun n ↦ (Subobject.map i).obj (f n),
      fun _ _ h ↦ (Subobject.map i).monotone (f.2 h)⟩

Premises used: CategoryTheory.Subobject.map, CategoryTheory.Functor.monotone, CategoryTheory.antitone_chain_condition_of_isArtinianObject, OrderHom.mk, DFunLike.coe, CategoryTheory.Functor.obj, OrderHom.monotone'
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{v, u} Y
f : ℕ →o (Subobject.{v, u} X)ᵒᵈ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Subobject.{v, u} Y)ᵒᵈ)
        (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
              (a : ℕ) → (Subobject Y)ᵒᵈ)
            n :
          (Subobject.{v, u} Y)ᵒᵈ)
        (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
              (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.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsArtinianObject.{v, u} Y
f : ℕ →o (Subobject.{v, u} X)ᵒᵈ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Subobject.{v, u} Y)ᵒᵈ)
        (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
              (a : ℕ) → (Subobject Y)ᵒᵈ)
            n :
          (Subobject.{v, u} Y)ᵒᵈ)
        (({ toFun := fun (n : ℕ) ↦ (Subobject.map i).obj ((f : (a : ℕ) → (Subobject X)ᵒᵈ) n), monotone' := ⋯ } :
              (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.ArtinianObject
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 : isArtinianObject.{v, u} Y_1
rw : ∀ (hY : ObjectProperty.Is.{v, u} isArtinianObject Y_1), ObjectProperty.Is.{v, u} isArtinianObject X_1
⊢ isArtinianObject.{v, u} X_1

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

Premises used: CategoryTheory.ObjectProperty.is_iff, CategoryTheory.isArtinianObject
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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} isArtinianObject Y_1
⊢ ObjectProperty.Is.{v, u} isArtinianObject X_1

Tactic:
isArtinianObject_of_mono f

Premises used: CategoryTheory.isArtinianObject_of_mono
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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} isArtinianObject Y_1
⊢ ObjectProperty.Is.{v, u} isArtinianObject X_1

Tactic:
exact isArtinianObject_of_mono f

Premises used: CategoryTheory.isArtinianObject_of_mono
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
⊢ Nontrivial (Subobject.{v, u} X)

Tactic:
have : Nontrivial (Subobject X) := nontrivial_of_not_isZero h
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
this : Nontrivial (Subobject.{v, u} X)
obtain :
  ∀ (Y : Subobject.{v, u} X) (s : IsAtom Y ∧ Y ≤ ⊤),
    ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)
⊢ ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)

Tactic:
obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot

Premises used: IsAtomic.eq_bot_or_exists_atom_le, top_ne_bot, Or.resolve_left, Top.top
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsArtinianObject.{v, u} X
h : ¬IsZero.{v, u} X
this : Nontrivial (Subobject.{v, u} X)
Y : Subobject.{v, u} X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ (Y : Subobject.{v, u} X), Simple.{v, u} (Functor.obj underlying Y)

Tactic:
⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩

Premises used: Iff.mpr, CategoryTheory.subobject_simple_iff_isAtom, And.left, Exists.intro