-- 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 :
  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
⊢ ∃ (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)
have 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 sorry (CofilteredClosureSmall.InductiveStep.min sorry sorry 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)))
        sorry).obj
    (P := cofilteredClosure f)
Tactic: refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩