-- 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
h : cofilteredClosure.{w, v, u} f j
base :
  ∀ (x : α),
    ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
      CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
        ObjectProperty.FullSubcategory.obj (P := cofilteredClosure f)
          (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (f x) ⋯)
min :
  ∀ {j j' : C} (hj₁ : cofilteredClosure.{w, v, u} f j) (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))
    (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) (IsCofiltered.min.{v, u} j j') ⋯).obj (P :=
          cofilteredClosure f)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) j h).obj (P := cofilteredClosure f)
have eq : ∀ {j j' : C} (hj₁ : cofilteredClosure.{w, v, u} f j) (hj₂ : cofilteredClosure.{w, v, u} f j') (g g' : j ⟶ 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))
  (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') sorry).obj (P := cofilteredClosure f)
Tactic: induction h with
  | base x =>
    refine ⟨⟨0, ?_⟩,?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      exact ULift.up x
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | min hj₁ hj₂ ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
  | eq hj₁ hj₂ g g' ih ih' =>
    rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl
Cleared hypotheses: h