awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
    Eq (α := F.obj U) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x : F.obj U)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type (max v w)) ↦ X) (F.obj X)) → (fun (X : Type (max v w)) ↦ X) (F.obj U))
          x :
        (fun (X : Type (max v w)) ↦ X) (F.obj U))

Tactic:
⟨f.unop, rfl⟩

Premises used: Quiver.Hom.unop, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : X ⟶ U
⊢ ∃ (x_1 : Opposite.unop U ⟶ Opposite.unop X),
    Eq (α := F.obj U) ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1.op) : (a : F.obj X) → F.obj U) x : F.obj U)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type (max v w)) ↦ X) (F.obj X)) → (fun (X : Type (max v w)) ↦ X) (F.obj U))
          x :
        (fun (X : Type (max v w)) ↦ X) (F.obj U))

Tactic:
exact ⟨f.unop, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ Membership.mem (α := F.obj U) ((ofSection x).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj X) → F.obj U) x : F.obj U)

Tactic:
⟨f.op, rfl⟩

Premises used: Set.Mem, Quiver.Hom.op, setOf, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
f : Opposite.unop U ⟶ Opposite.unop X
⊢ Membership.mem (α := F.obj U) ((ofSection x).obj U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj X) → F.obj U) x : F.obj U)

Tactic:
exact ⟨f.op, rfl⟩
-- Module: Mathlib.CategoryTheory.Subfunctor.OfSection
Goal:
C : Type u
inst : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : C
f : Functor.obj yoneda X ⋙ uliftFunctor.{w, v} ⟶ F
rw :
  range f =
    range (F' := Functor.obj uliftYoneda.{w, v, u} (Opposite.unop (Opposite.op X)))
      ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (Opposite.op (Opposite.unop (Opposite.op X)))) →
            uliftYoneda.{w, v, u}.obj (Opposite.unop (Opposite.op X)) ⟶ F)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f))
rw₁ rw₂ : range f = range f
⊢ range f =
    ofSection (X := Opposite.op X)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X ⟶ F) → F.obj (Opposite.op X)) f)

Tactic:
rw [ofSection_eq_range', Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Subfunctor.ofSection_eq_range'
-- Module: Mathlib.CategoryTheory.Subfunctor.Sieves
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
V W : C
i : V ⟶ unop U
hi :
  Membership.mem (α := (fun (X : Type w) ↦ X) (F.obj (op V))) (γ := Set (F.obj (op V))) (G.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F.obj (op V)))
j : W ⟶ V
⊢ Membership.mem (α := (fun (X : Type w) ↦ X) (F.obj (op W))) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (j ≫ i).op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op W)))
        s :
      (fun (X : Type w) ↦ X) (F.obj (op W)))

Tactic:
simpa using G.map _ hi

Premises used: CategoryTheory.Subfunctor.map
-- Module: Mathlib.CategoryTheory.Subfunctor.Sieves
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₁ h₁) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₂ h₂) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))

Tactic:
Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Subfunctor.Sieves
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
refine :
  Eq.{w + 1} (α := F.obj (op Z))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
          (G.familyOfElementsOfSection s f₁ h₁)) :
      F.obj (op Z))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
          (G.familyOfElementsOfSection s f₂ h₂)) :
      F.obj (op Z))
⊢ Eq (α := (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₁ h₁) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
        (G.familyOfElementsOfSection s f₂ h₂) :
      (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Subfunctor.Sieves
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ unop U
f₂ : Y₂ ⟶ unop U
h₁ : (G.sieveOfSection s).arrows f₁
h₂ : (G.sieveOfSection s).arrows f₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
change :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₁))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₁)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₁))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op Y₂))) → (fun (X : Type w) ↦ X) (F.obj (op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y₂)))
            s :
          (fun (X : Type w) ↦ X) (F.obj (op Y₂))) :
      (fun (X : Type w) ↦ X) (F.obj (op Z)))
⊢ Eq.{w + 1} (α := F.obj (op Z))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₁.op) :
            (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₁))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
          (G.familyOfElementsOfSection s f₁ h₁)) :
      F.obj (op Z))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map g₂.op) :
            (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Y₂))) → (fun (X : Type w) ↦ X) (G.toFunctor.obj (op Z)))
          (G.familyOfElementsOfSection s f₂ h₂)) :
      F.obj (op Z))

Tactic:
change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : MonoOver F
f : X ⟶ Y
rw : range (Over.Hom.left f.hom ≫ Y.arrow) ≤ range Y.arrow
⊢ range X.arrow ≤ range Y.arrow

Tactic:
rw [← MonoOver.w f]

Premises used: CategoryTheory.MonoOver.w
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X Y : MonoOver F
f : X ⟶ Y
⊢ range (Over.Hom.left f.hom ≫ Y.arrow) ≤ range Y.arrow

Tactic:
apply range_comp_le

Premises used: CategoryTheory.Subfunctor.range_comp_le
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F
⊢ Functor.obj (𝟭 (Subfunctor F)) A =
    Functor.obj
      (Functor.comp (D := MonoOver F)
        { obj := fun (A : Subfunctor F) ↦ MonoOver.mk A.ι,
          map := fun {A B : Subfunctor F} (f : A ⟶ B) ↦ MonoOver.homMk (homOfLe ⋯) ⋯, map_id := ⋯, map_comp := ⋯ }
        { obj := fun (X : MonoOver F) ↦ range X.arrow, map := fun {X Y : MonoOver F} (f : X ⟶ Y) ↦ homOfLE ⋯,
          map_id := ⋯, map_comp := ⋯ })
      A

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F
⊢ range (Subobject.mk A.ι).arrow = A

Tactic:
(((equivalenceMonoOver F).trans
    (ThinSkeleton.equivalence _).symm).unitIso.app A).to_eq.symm

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.Equivalence.unitIso, CategoryTheory.MonoOver.mk, CategoryTheory.ThinSkeleton.equivalence, CategoryTheory.Subobject.mk, CategoryTheory.Subfunctor.equivalenceMonoOver, Quotient.mk', CategoryTheory.Subfunctor.range, CategoryTheory.Equivalence.trans, CategoryTheory.Iso.app, Eq.symm, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : Subobject F
⊢ Subobject.mk (range X.arrow).ι = X

Tactic:
(((equivalenceMonoOver F).trans
    (ThinSkeleton.equivalence _).symm).counitIso.app X).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.MonoOver.mk, CategoryTheory.ThinSkeleton.equivalence, CategoryTheory.Subobject.mk, CategoryTheory.Subfunctor.equivalenceMonoOver, Quotient.mk', CategoryTheory.Subfunctor.range, CategoryTheory.Equivalence.trans, CategoryTheory.Iso.app, CategoryTheory.Equivalence.symm, CategoryTheory.Subobject, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A : Subfunctor F
⊢ (fun (X : Subobject F) ↦ range X.arrow) ((fun (A : Subfunctor F) ↦ Subobject.mk A.ι) A) = A

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
X : Subobject F
⊢ (fun (A : Subfunctor F) ↦ Subobject.mk A.ι) ((fun (X : Subobject F) ↦ range X.arrow) X) = X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor F
mp :
  LE.le (α := Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          A :
        Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          B :
        Subobject F) →
    A ≤ B
mpr :
  A ≤ B →
    LE.le (α := Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          A :
        Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          B :
        Subobject F)
⊢ LE.le (α := Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          A :
        Subobject F)
      (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : Subfunctor F) → Subobject F)
          B :
        Subobject F) ↔
    A ≤ B

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor F
h :
  LE.le (α := Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        A :
      Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F)
⊢ range (Subobject.mk A.ι).arrow ≤ range (Subobject.mk B.ι).arrow

Tactic:
have : range (Subobject.mk A.ι).arrow ≤ range (Subobject.mk B.ι).arrow :=
        leOfHom (((equivalenceMonoOver F).trans
          (ThinSkeleton.equivalence _).symm).inverse.map (homOfLE h))
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor F
h :
  LE.le (α := Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        A :
      Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F)
this : range (Subobject.mk A.ι).arrow ≤ range (Subobject.mk B.ι).arrow
⊢ A ≤ B

Tactic:
simpa using this
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor F
h : A ≤ B
⊢ LE.le (α := Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        A :
      Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F)

Tactic:
leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE h))

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.ThinSkeleton.equivalence, CategoryTheory.Functor.map, CategoryTheory.Subfunctor.equivalenceMonoOver, CategoryTheory.homOfLE, CategoryTheory.Equivalence.trans, CategoryTheory.leOfHom, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Subfunctor.Subobject
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor F
h : A ≤ B
⊢ LE.le (α := Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        A :
      Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F)

Tactic:
exact leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE h))

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.ThinSkeleton.equivalence, CategoryTheory.Functor.map, CategoryTheory.Subfunctor.equivalenceMonoOver, CategoryTheory.homOfLE, CategoryTheory.Equivalence.trans, CategoryTheory.leOfHom, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : IsArtinianObject.{v, u} X
⊢ WellFoundedLT (Subobject.{v, u} X)

Tactic:
isArtinianObject.prop_of_is X

Premises used: CategoryTheory.isArtinianObject, CategoryTheory.ObjectProperty.prop_of_is
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
rw :
  isArtinianObject.{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₁ :
  WellFoundedLT (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₂ :
  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} isArtinianObject 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, isArtinianObject,
    ← wellFoundedGT_dual_iff,
    wellFoundedGT_iff_monotone_chain_condition]

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

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

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

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

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

Tactic:
rw [ObjectProperty.is_iff, isArtinianObject, WellFoundedLT,
    isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]

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

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.ArtinianObject
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictAnti f
⊢ IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x1 < x2)

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

Tactic:
(isArtinianObject_iff_not_strictAnti X).1 inferInstance f

Premises used: CategoryTheory.isArtinianObject_iff_not_strictAnti, inferInstance, Iff.mp
-- Module: Mathlib.CategoryTheory.Subobject.ArtinianObject
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
⊢ IsArtinianObject.{v, u} X ↔ ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F

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
⊢ (∀ (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