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

Proof state:
case mk.max.intro.mk.intro.mk.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ m < n ⊔ m + 1

Tactic:
apply Nat.lt_succ_of_le

Result:
case mk.max.intro.mk.intro.mk.refine_2.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ m ≤ n ⊔ m

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ ∀ (b : FullSubcategory (FilteredClosure f)),
    ∃ a, CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a = b.obj

Tactic:
rintro ⟨j, h⟩

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
h : FilteredClosure f j
⊢ ∃ a,
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a =
      { obj := j, property := h }.obj

Proof state:
case mk.coeq.intro.mk.intro.mk.refine_1.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ n ≤ n ⊔ m

case mk.coeq.intro.mk.intro.mk.refine_2.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ m ≤ n ⊔ m

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

Result:
no goals

Proof state:
case mk.max.intro.mk.intro.mk.refine_1.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ n ≤ n ⊔ m

case mk.max.intro.mk.intro.mk.refine_2.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ m ≤ n ⊔ m

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

Result:
no goals

Proof state:
case mk.coeq.intro.mk.intro.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ ∃ a,
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a =
      { obj := coeq g g', property := ⋯ }.obj

Tactic:
refine ⟨⟨(Max.max n m).succ, FilteredClosureSmall.InductiveStep.coeq ?_ ?_ x y g g'⟩, rfl⟩

Result:
case mk.coeq.intro.mk.intro.mk.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ n < n ⊔ m + 1

case mk.coeq.intro.mk.intro.mk.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CategoryTheory.IsFiltered.FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : FilteredClosure f (CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ m < n ⊔ m + 1

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ Small.{max v w, u} (FullSubcategory (FilteredClosure f))

Tactic:
refine small_of_injective_of_exists (FilteredClosureSmall.abstractFilteredClosureRealization f)
  (fun _ _ => FullSubcategory.ext) ?_

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
⊢ ∀ (b : FullSubcategory (FilteredClosure f)),
    ∃ a, CategoryTheory.IsFiltered.FilteredClosureSmall.abstractFilteredClosureRealization f a = b.obj