-- 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).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
min₁ :
  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)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (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:
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩