-- Mathlib/CategoryTheory/Filtered/Small.lean
theorem small_fullSubcategory_cofilteredClosure :
    Small.{max v w} (FullSubcategory (CofilteredClosure f))

Proof state:
case mk.eq.intro.mk.intro.mk.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ n < n ⊔ m + 1

case mk.eq.intro.mk.intro.mk.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ m < n ⊔ m + 1

Tactic:
all_goals apply Nat.lt_succ_of_le

Result:
case mk.eq.intro.mk.intro.mk.refine_1.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ n ≤ n ⊔ m

case mk.eq.intro.mk.intro.mk.refine_2.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ m ≤ n ⊔ m

Proof state:
case mk.min.intro.mk.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      {
          obj :=
            min (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
              (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
          property := ⋯ }.obj

Tactic:
refine ⟨⟨(Max.max n m).succ, CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y⟩, rfl⟩

Result:
case mk.min.intro.mk.intro.mk.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ n < n ⊔ m + 1

case mk.min.intro.mk.intro.mk.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ m < n ⊔ m + 1

Proof state:
case mk.eq
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j j✝ j'✝ : C
hj₁ : CofilteredClosure f j✝
hj₂ : CofilteredClosure f j'✝
g g' : j✝ ⟶ j'✝
ih :
  ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      { obj := j✝, property := hj₁ }.obj
ih' :
  ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      { obj := j'✝, property := hj₂ }.obj
⊢ ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      { obj := eq g g', property := ⋯ }.obj

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

Result:
case mk.eq.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j j'✝ : C
hj₂ : CofilteredClosure f j'✝
ih' :
  ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      { obj := j'✝, property := hj₂ }.obj
n : ℕ
x : (CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ :
  CofilteredClosure f (CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
g g' : CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶ j'✝
⊢ ∃ a,
    CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      { obj := eq g g', property := ⋯ }.obj