awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j j' : C
hj₂ : cofilteredClosure.{w, v, u} f j'
ih' :
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j' hj₂).obj (P := cofilteredClosure f)
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f)
            (min.{v, u}
              (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
                (Sigma.mk (β := fun (n : ℕ) ↦
                  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                    fun (t : Type (max v w)) ↦ t → C))
                  n x))
              j')
            ⋯).obj
        (P := cofilteredClosure f)
have min : ∀ (m : ℕ)
  (y :
    (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C))
  (hj₂ :
    cofilteredClosure.{w, v, u} f
      (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          m y))),
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f)
            (min.{v, u}
              (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
                (Sigma.mk (β := fun (n : ℕ) ↦
                  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                    fun (t : Type (max v w)) ↦ t → C))
                  n x))
              (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
                (Sigma.mk (β := fun (n : ℕ) ↦
                  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                    fun (t : Type (max v w)) ↦ t → C))
                  m y)))
            sorry).obj
        (P := cofilteredClosure f)
Tactic: rcases ih' with ⟨⟨m, y⟩, rfl⟩
Cleared hypotheses: j', hj₂, ih'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f)
            (min.{v, u}
              (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
                (Sigma.mk (β := fun (n : ℕ) ↦
                  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                    fun (t : Type (max v w)) ↦ t → C))
                  n x))
              (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
                (Sigma.mk (β := fun (n : ℕ) ↦
                  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                    fun (t : Type (max v w)) ↦ t → C))
                  m y)))
            ⋯).obj
        (P := cofilteredClosure f)
have min : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
  fun (t : Type (max v w)) ↦ t → C)
Tactic: refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
have min : CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
  CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
Tactic: simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
have min : n < max n m + 1
Tactic: refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
min : n < max n m + 1
⊢ CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
have min₁ : m < max n m + 1
Tactic: refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ n < max n m + 1
have min : n ≤ max n m
Tactic: apply Nat.lt_succ_of_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ m < max n m + 1
have min : m ≤ max n m
Tactic: apply Nat.lt_succ_of_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        (max n m).succ (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y))) =
    (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f)
          (min.{v, u}
            (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
              (Sigma.mk (β := fun (n : ℕ) ↦
                (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                  fun (t : Type (max v w)) ↦ t → C))
                n x))
            (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
              (Sigma.mk (β := fun (n : ℕ) ↦
                (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β :=
                  fun (t : Type (max v w)) ↦ t → C))
                m y)))
          ⋯).obj
      (P := cofilteredClosure f)
have min : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
    fun (t : Type (max v w)) ↦ t → C) (Eq.mpr sorry (CofilteredClosureSmall.InductiveStep.min sorry sorry x y)) =
  min.{v, u}
    ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).snd (β := fun (t : Type (max v w)) ↦ t → C)
      x)
    ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).snd (β := fun (t : Type (max v w)) ↦ t → C)
      y)
Tactic: simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
      fun (t : Type (max v w)) ↦ t → C) (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)) =
    min.{v, u}
      ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).snd (β := fun (t : Type (max v w)) ↦
        t → C) x)
      ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).snd (β := fun (t : Type (max v w)) ↦
        t → C) y)
have min : Sigma.snd (β := fun (t : Type (max v w)) ↦ t → C)
    (Sigma.mk (β := fun (t : Type (max v w)) ↦ t → C)
      (CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
      (CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1))
    (Eq.mpr (β :=
      CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
        CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
      sorry (CofilteredClosureSmall.InductiveStep.min sorry sorry x y)) =
  min.{v, u}
    ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).snd (β := fun (t : Type (max v w)) ↦ t → C)
      x)
    ((CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).snd (β := fun (t : Type (max v w)) ↦ t → C)
      y)
Tactic: rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j j_1 j' : C
hj₁ : cofilteredClosure.{w, v, u} f j_1
hj₂ : cofilteredClosure.{w, v, u} f j'
g g' : j_1 ⟶ j'
ih :
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j_1 hj₁).obj (P := cofilteredClosure f)
ih' :
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j' hj₂).obj (P := cofilteredClosure f)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') ⋯).obj (P := cofilteredClosure f)
have eq : ∀ (n : ℕ)
  (x :
    (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C))
  (hj₁ :
    cofilteredClosure.{w, v, u} f
      (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          n x)))
  (g g' :
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          n x) ⟶
      j'),
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') sorry).obj (P := cofilteredClosure f)
Tactic: rcases ih with ⟨⟨n, x⟩, rfl⟩
Cleared hypotheses: j_1, hj₁, g, g', ih
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j j' : C
hj₂ : cofilteredClosure.{w, v, u} f j'
ih' :
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j' hj₂).obj (P := cofilteredClosure f)
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    j'
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') ⋯).obj (P := cofilteredClosure f)
have eq : ∀ (m : ℕ)
  (y :
    (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C))
  (hj₂ :
    cofilteredClosure.{w, v, u} f
      (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          m y)))
  (g g' :
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          n x) ⟶
      CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
        (Sigma.mk (β := fun (n : ℕ) ↦
          (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
            t → C))
          m y)),
  ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') sorry).obj (P := cofilteredClosure f)
Tactic: rcases ih' with ⟨⟨m, y⟩, rfl⟩
Cleared hypotheses: j', hj₂, ih', g, g'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Small (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₁ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x))
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m).fst (β := fun (t : Type (max v w)) ↦ t → C)
hj₂ :
  cofilteredClosure.{w, v, u} f
    (CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y))
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        n x) ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization.{w, v, u} f
      (Sigma.mk (β := fun (n : ℕ) ↦
        (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f n).fst (β := fun (t : Type (max v w)) ↦
          t → C))
        m y)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (eq g g') ⋯).obj (P := cofilteredClosure f)
have eq : (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
  fun (t : Type (max v w)) ↦ t → C)
Tactic: refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩