awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 : Over.{v₁, u₁} X
h_1 : ObjectProperty.limitsOfShape (Over.isMono X) J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z_1 : C
g h : Z_1 ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj (WithTerminal.of j))
    (g ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
    (h ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
have of : Eq (α := Z_1 ⟶ X)
  ((g ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
        (WithTerminal.of j)) ≫
    (p.diag.obj j).hom)
  ((h ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
        (WithTerminal.of j)) ≫
    (p.diag.obj j).hom)
Tactic: rw [← cancel_mono ((p.diag.obj j).hom)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 : Over.{v₁, u₁} X
h_1 : ObjectProperty.limitsOfShape (Over.isMono X) J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z_1 : C
g h : Z_1 ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : WithTerminal J
⊢ g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j =
    h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j
have of : ∀ (j : J),
  Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj (WithTerminal.of j))
    (g ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
    (h ≫
      (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app (WithTerminal.of j))
Tactic: cases j with
    | of j => have := hp j; rw [← cancel_mono ((p.diag.obj j).hom)]; simpa
    | star => exact e
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 : Over.{v₁, u₁} X
h_1 : ObjectProperty.limitsOfShape (Over.isMono X) J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z_1 : C
g h : Z_1 ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : WithTerminal J
of :
  ∀ (j : J),
    Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj (WithTerminal.of j))
      (g ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j))
      (h ≫
        (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app
          (WithTerminal.of j))
⊢ g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j =
    h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app j
have star : Eq (α := Z_1 ⟶ (obj WithTerminal.liftFromOver p.diag).obj WithTerminal.star)
  (g ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
  (h ≫ (obj (Equivalence.functor WithTerminal.coneEquiv) { pt := F, π := p.π : Cone p.diag }).π.app WithTerminal.star)
Tactic: cases j with
    | of j => have := hp j; rw [← cancel_mono ((p.diag.obj j).hom)]; simpa
    | star => exact e
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (hypothesis)
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 ((Over.pullback f).obj (obj (forget Y) g)).hom
have this : Mono (obj (forget Y) g).hom
Tactic: haveI : Mono ((forget Y).obj g).hom := (inferInstance : Mono g.arrow)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
have refine : Over.Hom.left e.hom ≫ h.arrow = g.arrow
Tactic: refine ⟨homMk e.hom.left ?_, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 = g.arrow
have rw : Over.Hom.left e.hom ≫ h.arrow ≫ f = g.arrow ≫ f
Tactic: rw [← cancel_mono f, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 (obj (Over.post e.functor) (obj (forget X) f)).hom
have dsimp : Mono (e.functor.map f.obj (P := Over.isMono X).hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 (obj (Over.post e.inverse) (obj (forget (e.functor.obj X)) f)).hom
have dsimp : Mono (e.inverse.map f.obj (P := Over.isMono (e.functor.obj X)).hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ imageMonoOver f.hom ⟶ imageMonoOver g.hom
have apply : obj (forget X) (imageMonoOver f.hom) ⟶ obj (forget X) (imageMonoOver g.hom)
Tactic: apply (forget X).preimage _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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) ⟶ obj (forget X) (imageMonoOver g.hom)
have apply : (obj (forget X) (imageMonoOver f.hom)).left ⟶ (obj (forget X) (imageMonoOver g.hom)).left
Tactic: apply Over.homMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ obj (forget X) (imageMonoOver f.hom) ⟶ obj (forget X) (imageMonoOver g.hom)
have apply₁ : image.lift
      { I := Limits.image g.hom, m := (image.ι g.hom : Limits.image g.hom ⟶ X), m_mono := sorry,
        e := (Over.Hom.left k ≫ factorThruImage g.hom : f.left ⟶ Limits.image g.hom), fac := sorry } ≫
    (obj (forget X) (imageMonoOver g.hom)).hom =
  (obj (forget X) (imageMonoOver f.hom)).hom
Tactic: apply Over.homMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ f ⟶ obj (forget X) g
have apply : (factorThruImage f.hom ≫ Over.Hom.left k.hom) ≫ g.obj (P := Over.isMono X).hom = f.hom
Tactic: apply Over.homMk (factorThruImage f.hom ≫ k.hom.left) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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 ≫ Over.Hom.left k.hom) ≫ g.obj (P := Over.isMono X).hom = f.hom
have rw : factorThruImage f.hom ≫ (obj image f).obj (P := Over.isMono X).hom = f.hom
Tactic: rw [assoc, Over.w k.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ (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
have h : Over.Hom.left
    ((fun (k : obj image f ⟶ g) ↦ Over.homMk (factorThruImage f.hom ≫ Over.Hom.left k.hom) sorry)
      ((fun (k : f ⟶ obj (forget X) g) ↦
          (homMk
              (image.lift
                { I := g.obj (P := Over.isMono X).left, m := g.arrow, m_mono := sorry, e := Over.Hom.left k, fac := sorry })
              sorry :
            obj image f ⟶ g))
        k)) =
  Over.Hom.left k
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ («exists» f).obj Z ≅ (map f).obj Z
have suffices : obj (forget Y) ((«exists» f).obj Z) ≅ obj (forget Y) ((map f).obj Z)
Tactic: suffices (forget _).obj ((«exists» f).obj Z) ≅ (forget _).obj ((map f).obj Z) by
      apply (forget _).preimageIso this
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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) ≅ obj (forget Y) ((map f).obj Z)
have apply : (obj (forget Y) ((«exists» f).obj Z)).left ≅ (obj (forget Y) ((map f).obj Z)).left
Tactic: apply Over.isoMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.MonoOver (goal)
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
⊢ obj (forget Y) ((«exists» f).obj Z) ≅ obj (forget Y) ((map f).obj Z)
have apply₁ : Iso.hom (imageMonoIsoSource (Z.arrow ≫ f)) ≫ (obj (forget Y) ((map f).obj Z)).hom =
  (obj (forget Y) ((«exists» f).obj Z)).hom
Tactic: apply Over.isoMk _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ 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)
have 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)
Tactic: rw [ObjectProperty.is_iff, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
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)
⊢ 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)
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, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
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)
⊢ 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)
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, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsNoetherianObject.{v, u} X ↔ ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f
have refine : ∀ (h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f), IsNoetherianObject.{v, u} X
Tactic: refine ⟨fun _ ↦ not_strictMono_of_wellFoundedGT, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject.{v, u} X), ¬StrictMono f
⊢ ObjectProperty.Is.{v, u} isNoetherianObject X
have rw : IsEmpty ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : Subobject.{v, u} X) ↦ x2 < x1)
Tactic: rw [ObjectProperty.is_iff, isNoetherianObject, WellFoundedGT,
    isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ IsNoetherianObject.{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 [isNoetherianObject_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (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.NoetherianObject (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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
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
⊢ IsFiltered.IsEventuallyConstant G
have 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
Tactic: obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
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
have refine_1 : ∀ (m : ℕ) (hm : n ⟶ m), IsIso (G.map hm)
Tactic: refine ⟨n, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h :
  ∀ (f : ℕ →o Subobject.{v, u} X),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Subobject.{v, u} X) ((f : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
            ((f : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
G : ℕ ⥤ MonoOver.{v, u} X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) n :
          Subobject.{v, u} X)
        (((G ⋙ Equivalence.inverse (Subobject.equivMonoOver X)).toOrderHom : (a : ℕ) → Subobject X) m :
          Subobject.{v, u} X)
m : ℕ
hm : n ⟶ m
⊢ IsIso (G.map hm)
have refine_1 : Subobject.mk (G.obj n).obj (P := Over.isMono X).hom = Subobject.mk (G.obj m).obj (P := Over.isMono X).hom
Tactic: rw [MonoOver.isIso_iff_subobjectMk_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
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 : ℕ),
    ∀ (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 refine_2 : ∀ (n : ℕ) (hn : (sorry.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
Tactic: obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ Subobject.representative)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver.{v, u} X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject.{v, u} X
n : ℕ
hn : (⋯.functor ⋙ Subobject.representative).IsEventuallyConstantFrom n
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
          ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
have refine_2 : ∀ (m : ℕ) (hm : n ≤ m),
  Eq (α := Subobject.{v, u} X) ((F : (a : ℕ) → Subobject X) n : Subobject.{v, u} X)
    ((F : (a : ℕ) → Subobject X) m : Subobject.{v, u} X)
Tactic: refine ⟨n, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{v, u} X
⊢ IsNoetherianObject.{v, u} X
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)
Tactic: rw [isNoetherianObject_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
hX : IsZero.{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)
have this : Subsingleton (Subobject.{v, u} X)
Tactic: have := Subobject.subsingleton_of_isZero hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroObject.{v, u} C
⊢ isNoetherianObject.{v, u} (C := C) 0
have rw : ObjectProperty.Is.{v, u} (C := C) isNoetherianObject 0
Tactic: rw [← isNoetherianObject.is_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.NoetherianObject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst_1 : Mono i
inst_2 : IsNoetherianObject.{v, u} Y
⊢ IsNoetherianObject.{v, u} X
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)
Tactic: rw [isNoetherianObject_iff_monotone_chain_condition]