awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Small
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 :
  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.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)

Tactic:
simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure
-- Module: Mathlib.CategoryTheory.Filtered.Small
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
min₁ : m < 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

Tactic:
refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.min
-- Module: Mathlib.CategoryTheory.Filtered.Small
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
⊢ n < max n m + 1

Tactic:
apply Nat.lt_succ_of_le

Premises used: Nat.lt_succ_of_le
-- Module: Mathlib.CategoryTheory.Filtered.Small
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 : m ≤ max n m
⊢ m < max n m + 1

Tactic:
apply Nat.lt_succ_of_le

Premises used: Nat.lt_succ_of_le
-- Module: Mathlib.CategoryTheory.Filtered.Small
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

Tactic:
Nat.le_max_left _ _

Premises used: Nat.le_max_left
-- Module: Mathlib.CategoryTheory.Filtered.Small
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

Tactic:
Nat.le_max_right _ _

Premises used: Nat.le_max_right
-- Module: Mathlib.CategoryTheory.Filtered.Small
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

Tactic:
exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]

Premises used: Nat.le_max_right, Nat.le_max_left
-- Module: Mathlib.CategoryTheory.Filtered.Small
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 :
  (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)) =
    IsCofiltered.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)
⊢ 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)
          (IsCofiltered.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)

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization
-- Module: Mathlib.CategoryTheory.Filtered.Small
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 :
  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)
        ⋯ (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)) =
    IsCofiltered.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)
⊢ (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)) =
    IsCofiltered.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]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure
-- Module: Mathlib.CategoryTheory.Filtered.Small
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))
⊢ 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)
        ⋯ (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)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Filtered.Small
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)
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) (IsCofiltered.eq g g') ⋯).obj (P :=
          cofilteredClosure f)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
        cofilteredClosure f)

Tactic:
rcases ih with ⟨⟨n, x⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Filtered.Small
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'
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) (IsCofiltered.eq g g') ⋯).obj (P :=
          cofilteredClosure f)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
        cofilteredClosure f)

Tactic:
rcases ih' with ⟨⟨m, y⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Filtered.Small
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)

Tactic:
⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩

Premises used: Max.max, Exists.intro, Sigma.mk, Nat.succ