awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
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.{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))
have 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)))
Tactic: change F.map g₁.op (F.map f₁.op s) = F.map g₂.op (F.map f₂.op s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
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) (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)))
have rw : Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op ≫ F.map g₁.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    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)))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp, ← op_comp, ← op_comp, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
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₂
rw :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op ≫ F.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      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 (α := (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)))
have rw₁ : Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    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)))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp, ← op_comp, ← op_comp, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Sieves (goal)
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₂
rw :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁.op ≫ F.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      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)))
rw₁ :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
          (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
        s :
      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 (α := (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)))
have rw₂ : Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₁.op ≫ g₁.op)) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    F.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂.op ≫ F.map g₂.op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → F.obj (op Z))
      s :
    F.obj (op Z))
Tactic: rw [← comp_apply, ← Functor.map_comp, ← comp_apply, ← Functor.map_comp, ← op_comp, ← op_comp, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Subobject (goal)
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 X.arrow ≤ range Y.arrow
have rw : range (Over.Hom.left f.hom ≫ Y.arrow) ≤ range Y.arrow
Tactic: rw [← MonoOver.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w, u, w + 1} C (Type w)
A B : Subfunctor 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
have mp : LE.le (α := Subobject F)
    (({ toFun := fun (A : Subfunctor F) ↦ Subobject.mk A.ι, invFun := fun (X : Subobject F) ↦ range X.arrow,
            left_inv := sorry, right_inv := sorry } :
          (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 := sorry, right_inv := sorry } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F) →
  A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Subobject (goal)
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
⊢ 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
have 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 := sorry, right_inv := sorry } :
          (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 := sorry, right_inv := sorry } :
          (a : Subfunctor F) → Subobject F)
        B :
      Subobject F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subfunctor.Subobject (hypothesis)
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)
⊢ A ≤ B
have this : 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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ 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)ᵒᵈ)
have 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)ᵒᵈ)
Tactic: rw [ObjectProperty.is_iff, isArtinianObject,
    ← wellFoundedGT_dual_iff,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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)ᵒᵈ)
⊢ 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)ᵒᵈ)
have 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)ᵒᵈ)
Tactic: rw [ObjectProperty.is_iff, isArtinianObject,
    ← wellFoundedGT_dual_iff,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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)ᵒᵈ)
⊢ 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)ᵒᵈ)
have 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)ᵒᵈ)
Tactic: rw [ObjectProperty.is_iff, isArtinianObject,
    ← wellFoundedGT_dual_iff,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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)ᵒᵈ)
⊢ 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)ᵒᵈ)
have 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)ᵒᵈ)
Tactic: rw [ObjectProperty.is_iff, isArtinianObject,
    ← wellFoundedGT_dual_iff,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsArtinianObject.{v, u} X ↔ ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictAnti f
have refine : ∀ (h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictAnti f), IsArtinianObject.{v, u} X
Tactic: refine ⟨fun _ ↦ not_strictAnti_of_wellFoundedLT, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictAnti f
⊢ ObjectProperty.Is.{v, u} isArtinianObject X
have rw : IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x1 < x2)
Tactic: rw [ObjectProperty.is_iff, isArtinianObject, WellFoundedLT,
    isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsArtinianObject.{v, u} X ↔ ∀ (F : ℕ ⥤ (MonoOver.{v, u} X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
have 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
Tactic: rw [isArtinianObject_iff_antitone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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
have 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
Tactic: refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.ArtinianObject (goal)
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
⊢ (∀ (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
have 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)ᵒᵈ)
Tactic: refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩