awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type u₃
inst_2 : Category.{v₃, u₃} J
X : C
F : J ⥤ MonoOver.{v₁, u₁} X
inst_3 : HasLimit (F ⋙ ObjectProperty.ι (Over.isMono X))
⊢ HasLimit F

Tactic:
hasLimit_of_closedUnderLimits _ _ _

Premises used: CategoryTheory.Limits.hasLimit_of_closedUnderLimits
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : MonoOver.{v₁, u₁} Y
⊢ Mono (obj (forget Y) g).hom

Tactic:
haveI : Mono ((forget Y).obj g).hom := (inferInstance : Mono g.arrow)
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : MonoOver.{v₁, u₁} Y
this : Mono (obj (forget Y) g).hom
⊢ Mono ((Over.pullback f).obj (obj (forget Y) g)).hom

Tactic:
apply pullback.snd_of_mono

Premises used: CategoryTheory.Limits.pullback.snd_of_mono
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : MonoOver.{v₁, u₁} Y
⊢ ((pullback f).obj g).obj (P := Over.isMono X).left = Limits.pullback g.arrow f

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : MonoOver.{v₁, u₁} Y
⊢ ((pullback f).obj g).arrow = pullback.snd (obj (forget Y) g).hom f

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
g : MonoOver.{v₁, u₁} X
⊢ ((map f).obj g).obj (P := Over.isMono Y).left = g.obj (P := Over.isMono X).left

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
g : MonoOver.{v₁, u₁} X
⊢ ((map f).obj g).arrow = g.arrow ≫ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : X ⟶ Y
inst_2 : Mono f
g h : MonoOver.{v₁, u₁} X
e : (map f).obj g ⟶ (map f).obj h
⊢ ∃ (a : g ⟶ h), (map f).map a = e

Tactic:
⟨homMk e.hom.left ?_, rfl⟩

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.MonoOver.homMk, Exists.intro, CategoryTheory.InducedCategory.Hom.hom, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : X ⟶ Y
inst_2 : Mono f
g h : MonoOver.{v₁, u₁} X
e : (map f).obj g ⟶ (map f).obj h
refine : Over.Hom.left e.hom ≫ h.arrow = g.arrow
⊢ ∃ (a : g ⟶ h), (map f).map a = e

Tactic:
refine ⟨homMk e.hom.left ?_, rfl⟩
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : X ⟶ Y
inst_2 : Mono f
g h : MonoOver.{v₁, u₁} X
e : (map f).obj g ⟶ (map f).obj h
rw : Over.Hom.left e.hom ≫ h.arrow ≫ f = g.arrow ≫ f
⊢ Over.Hom.left e.hom ≫ h.arrow = g.arrow

Tactic:
rw [← cancel_mono f, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
f : X ⟶ Y
inst_2 : Mono f
g h : MonoOver.{v₁, u₁} X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow ≫ f = g.arrow ≫ f

Tactic:
apply w e

Premises used: CategoryTheory.MonoOver.w
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.hom ≫ e.inv) = map (𝟙 A)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.inv ≫ e.hom) = map (𝟙 B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : MonoOver.{v₁, u₁} X
dsimp : Mono (e.functor.map f.obj (P := Over.isMono X).hom)
⊢ Mono (obj (Over.post e.functor) (obj (forget X) f)).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : MonoOver.{v₁, u₁} X
⊢ Mono (e.functor.map f.obj (P := Over.isMono X).hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : MonoOver.{v₂, u₂} (e.functor.obj X)
dsimp : Mono (e.inverse.map f.obj (P := Over.isMono (e.functor.obj X)).hom)
⊢ Mono (obj (Over.post e.inverse) (obj (forget (e.functor.obj X)) f)).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : MonoOver.{v₂, u₂} (e.functor.obj X)
⊢ Mono (e.inverse.map f.obj (P := Over.isMono (e.functor.obj X)).hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : HasImage f
⊢ (imageMonoOver f).arrow = image.ι f

Tactic:
rfl

Premises used: CategoryTheory.Limits.image.ι, rfl
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f g : Over.{v₁, u₁} X
k : f ⟶ g
apply : obj (forget X) (imageMonoOver f.hom) ⟶ obj (forget X) (imageMonoOver g.hom)
⊢ imageMonoOver f.hom ⟶ imageMonoOver g.hom

Tactic:
apply (forget X).preimage _

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.MonoOver.forget
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f g : Over.{v₁, u₁} X
k : f ⟶ g
apply : (obj (forget X) (imageMonoOver f.hom)).left ⟶ (obj (forget X) (imageMonoOver g.hom)).left
apply₁ :
  image.lift
        { I := Limits.image g.hom, m := (image.ι g.hom : Limits.image g.hom ⟶ X), m_mono := ⋯,
          e := (Over.Hom.left k ≫ factorThruImage g.hom : f.left ⟶ Limits.image g.hom), fac := ⋯ } ≫
      (obj (forget X) (imageMonoOver g.hom)).hom =
    (obj (forget X) (imageMonoOver f.hom)).hom
⊢ obj (forget X) (imageMonoOver f.hom) ⟶ obj (forget X) (imageMonoOver g.hom)

Tactic:
apply Over.homMk _ _

Premises used: CategoryTheory.Over.homMk
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f g : Over.{v₁, u₁} X
k : f ⟶ g
⊢ (obj (forget X) (imageMonoOver f.hom)).left ⟶ (obj (forget X) (imageMonoOver g.hom)).left

Tactic:
exact
        image.lift
          { I := Limits.image _
            m := image.ι g.hom
            e := k.left ≫ factorThruImage g.hom }

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Over.Hom.left, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.MonoFactorisation.mk, CategoryTheory.Limits.image, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.image.lift, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f g : Over.{v₁, u₁} X
k : f ⟶ g
⊢ image.lift
        { I := Limits.image g.hom, m := (image.ι g.hom : Limits.image g.hom ⟶ X), m_mono := ⋯,
          e := (Over.Hom.left k ≫ factorThruImage g.hom : f.left ⟶ Limits.image g.hom), fac := ⋯ } ≫
      (obj (forget X) (imageMonoOver g.hom)).hom =
    (obj (forget X) (imageMonoOver f.hom)).hom

Tactic:
apply image.lift_fac

Premises used: CategoryTheory.Limits.image.lift_fac
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : Over.{v₁, u₁} X
g : MonoOver.{v₁, u₁} X
k : obj image f ⟶ g
apply : (factorThruImage f.hom ≫ Over.Hom.left k.hom) ≫ g.obj (P := Over.isMono X).hom = f.hom
⊢ f ⟶ obj (forget X) g

Tactic:
apply Over.homMk (factorThruImage f.hom ≫ k.hom.left) _

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Over.Hom.left, CategoryTheory.Over.homMk, CategoryTheory.CategoryStruct.comp, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : Over.{v₁, u₁} X
g : MonoOver.{v₁, u₁} X
k : obj image f ⟶ g
rw : factorThruImage f.hom ≫ (obj image f).obj (P := Over.isMono X).hom = f.hom
⊢ (factorThruImage f.hom ≫ Over.Hom.left k.hom) ≫ g.obj (P := Over.isMono X).hom = f.hom

Tactic:
rw [assoc, Over.w k.hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.w, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : Over.{v₁, u₁} X
g : MonoOver.{v₁, u₁} X
k : obj image f ⟶ g
⊢ factorThruImage f.hom ≫ (obj image f).obj (P := Over.isMono X).hom = f.hom

Tactic:
apply image.fac

Premises used: CategoryTheory.Limits.image.fac
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : Over.{v₁, u₁} X
g : MonoOver.{v₁, u₁} X
k : f ⟶ obj (forget X) g
h :
  Over.Hom.left
      ((fun (k : obj image f ⟶ g) ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
        ((fun (k : f ⟶ obj (forget X) g) ↦
            (homMk
                (image.lift
                  { I := g.obj (P := Over.isMono X).left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ })
                ⋯ :
              obj image f ⟶ g))
          k)) =
    Over.Hom.left k
⊢ (fun (k : obj image f ⟶ g) ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
      ((fun (k : f ⟶ obj (forget X) g) ↦
          (homMk
              (image.lift
                { I := g.obj (P := Over.isMono X).left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ })
              ⋯ :
            obj image f ⟶ g))
        k) =
    k

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : Over.{v₁, u₁} X
g : MonoOver.{v₁, u₁} X
k : f ⟶ obj (forget X) g
⊢ Over.Hom.left
      ((fun (k : obj image f ⟶ g) ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) ⋯)
        ((fun (k : f ⟶ obj (forget X) g) ↦
            (homMk
                (image.lift
                  { I := g.obj (P := Over.isMono X).left, m := g.arrow, m_mono := ⋯, e := Over.Hom.left k, fac := ⋯ })
                ⋯ :
              obj image f ⟶ g))
          k)) =
    Over.Hom.left k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
⊢ IsRightAdjoint (C := Over.{v₁, u₁} X) (forget X)

Tactic:
⟨_, ⟨imageForgetAdj⟩⟩

Premises used: Nonempty.intro, CategoryTheory.MonoOver.imageForgetAdj, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
Z : MonoOver.{v₁, u₁} X
this : obj (forget Y) ((«exists» f).obj Z) ≅ obj (forget Y) ((map f).obj Z)
⊢ («exists» f).obj Z ≅ (map f).obj Z

Tactic:
apply (forget _).preimageIso this

Premises used: CategoryTheory.Functor.preimageIso, CategoryTheory.MonoOver.forget
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
Z : MonoOver.{v₁, u₁} X
suffices : obj (forget Y) ((«exists» f).obj Z) ≅ obj (forget Y) ((map f).obj Z)
⊢ («exists» f).obj Z ≅ (map f).obj Z

Tactic:
suffices (forget _).obj ((«exists» f).obj Z) ≅ (forget _).obj ((map f).obj Z) by
      apply (forget _).preimageIso this
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
Z : MonoOver.{v₁, u₁} X
apply : (obj (forget Y) ((«exists» f).obj Z)).left ≅ (obj (forget Y) ((map f).obj Z)).left
apply₁ :
  Iso.hom (imageMonoIsoSource (Z.arrow ≫ f)) ≫ (obj (forget Y) ((map f).obj Z)).hom =
    (obj (forget Y) ((«exists» f).obj Z)).hom
⊢ obj (forget Y) ((«exists» f).obj Z) ≅ obj (forget Y) ((map f).obj Z)

Tactic:
apply Over.isoMk _ _

Premises used: CategoryTheory.Over.isoMk
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
Z : MonoOver.{v₁, u₁} X
⊢ (obj (forget Y) ((«exists» f).obj Z)).left ≅ (obj (forget Y) ((map f).obj Z)).left

Tactic:
apply imageMonoIsoSource (Z.arrow ≫ f)

Premises used: CategoryTheory.Limits.imageMonoIsoSource, CategoryTheory.CategoryStruct.comp, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subobject.MonoOver
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasImages.{v₁, u₁} C
f : X ⟶ Y
inst_3 : Mono f
Z : MonoOver.{v₁, u₁} X
⊢ Iso.hom (imageMonoIsoSource (Z.arrow ≫ f)) ≫ (obj (forget Y) ((map f).obj Z)).hom =
    (obj (forget Y) ((«exists» f).obj Z)).hom

Tactic:
apply imageMonoIsoSource_hom_self

Premises used: CategoryTheory.Limits.imageMonoIsoSource_hom_self
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : IsNoetherianObject.{v, u} X
⊢ WellFoundedGT (Subobject.{v, u} X)

Tactic:
isNoetherianObject.prop_of_is X

Premises used: CategoryTheory.isNoetherianObject, CategoryTheory.ObjectProperty.prop_of_is
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
rw :
  isNoetherianObject.{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)
rw₁ :
  WellFoundedGT (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)
rw₂ rw₃ :
  (∀ (a : ℕ →o Subobject.{v, u} X),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := Subobject.{v, u} X) ((a : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
              ((a : (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)
⊢ ObjectProperty.Is.{v, u} isNoetherianObject 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:
rw [ObjectProperty.is_iff, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]

Premises used: CategoryTheory.ObjectProperty.is_iff, CategoryTheory.isNoetherianObject, wellFoundedGT_iff_monotone_chain_condition
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : IsNoetherianObject.{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:
(isNoetherianObject_iff_monotone_chain_condition X).1 inferInstance f

Premises used: inferInstance, CategoryTheory.isNoetherianObject_iff_monotone_chain_condition, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsNoetherianObject.{v, u} X ↔ ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f

Tactic:
⟨fun _ ↦ not_strictMono_of_wellFoundedGT, fun h ↦ ?_⟩

Premises used: not_strictMono_of_wellFoundedGT, Iff.intro
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
refine : ∀ (h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f), IsNoetherianObject.{v, u} X
⊢ IsNoetherianObject.{v, u} X ↔ ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f

Tactic:
refine ⟨fun _ ↦ not_strictMono_of_wellFoundedGT, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f
rw : IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x2 < x1)
⊢ ObjectProperty.Is.{v, u} isNoetherianObject X

Tactic:
rw [ObjectProperty.is_iff, isNoetherianObject, WellFoundedGT,
    isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]

Premises used: CategoryTheory.ObjectProperty.is_iff, WellFoundedGT, CategoryTheory.isNoetherianObject, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f
⊢ IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x2 < x1)

Tactic:
⟨fun f ↦ h f.toFun (fun a b h ↦ f.map_rel_iff.2 h)⟩

Premises used: Iff.mpr, RelEmbedding.toEmbedding, IsEmpty.mk, RelEmbedding.map_rel_iff, Function.Embedding.toFun
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f
⊢ IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x2 < x1)

Tactic:
exact ⟨fun f ↦ h f.toFun (fun a b h ↦ f.map_rel_iff.2 h)⟩
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : IsNoetherianObject.{v, u} X
f : ℕ → Subobject.{v, u} X
⊢ ¬StrictMono f

Tactic:
(isNoetherianObject_iff_not_strictMono X).1 inferInstance f

Premises used: inferInstance, Iff.mp, CategoryTheory.isNoetherianObject_iff_not_strictMono
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
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)) ↔
    ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
⊢ IsNoetherianObject.{v, u} X ↔ ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F

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
⊢ (∀ (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:
⟨fun h G ↦ ?_, fun h F ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Subobject.NoetherianObject
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.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
refine_1 :
  ∀ (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)),
    IsFiltered.IsEventuallyConstant G
⊢ IsFiltered.IsEventuallyConstant G

Tactic:
obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Subobject.equivMonoOver, CategoryTheory.Functor.toOrderHom, CategoryTheory.Equivalence.inverse
-- 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)
⊢ IsFiltered.IsEventuallyConstant G

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

Premises used: CategoryTheory.IsFiltered.IsEventuallyConstant.mk, Exists.intro