awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
g g' :
  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)
eq :
  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)
eq₁ :
  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.eq ⋯ ⋯ x y g g'))) =
    (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
      cofilteredClosure f)
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
        cofilteredClosure f)

Tactic:
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
-- 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))
g g' :
  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)
eq :
  CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).fst (β :=
    fun (t : Type (max v w)) ↦ t → C)

Tactic:
simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure
-- 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))
g g' :
  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)
eq : n < max n m + 1
eq₁ : m < max n m + 1
⊢ CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
    CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1

Tactic:
refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq
-- 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))
g g' :
  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)
eq : n ≤ max n m
⊢ n < max n m + 1

Tactic:
apply Nat.lt_succ_of_le

Premises used: Nat.lt_succ_of_le
-- 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))
g g' :
  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)
eq : m ≤ max n m
⊢ m < max n m + 1

Tactic:
apply Nat.lt_succ_of_le

Premises used: Nat.lt_succ_of_le
-- 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))
g g' :
  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)
⊢ n ≤ max n m

Tactic:
Nat.le_max_left _ _

Premises used: Nat.le_max_left
-- 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))
g g' :
  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)
⊢ m ≤ max n m

Tactic:
Nat.le_max_right _ _

Premises used: Nat.le_max_right
-- 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))
g g' :
  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)
⊢ n ≤ max n m

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

Premises used: Nat.le_max_right, Nat.le_max_left
-- 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))
g g' :
  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)
eq :
  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
      fun (t : Type (max v w)) ↦ t → C) (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    IsCofiltered.eq g g'
⊢ 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.eq ⋯ ⋯ x y g g'))) =
    (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (IsCofiltered.eq g g') ⋯).obj (P :=
      cofilteredClosure f)

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.abstractCofilteredClosureRealization
-- 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))
g g' :
  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)
eq :
  Sigma.snd (β := fun (t : Type (max v w)) ↦ t → C)
      (Sigma.mk (β := fun (t : Type (max v w)) ↦ t → C)
        (CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
        (CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1))
      (Eq.mpr (β :=
        CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
        ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    IsCofiltered.eq g g'
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f (max n m).succ).snd (β :=
      fun (t : Type (max v w)) ↦ t → C) (Eq.mpr ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    IsCofiltered.eq g g'

Tactic:
rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure
-- 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))
g g' :
  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)
⊢ Sigma.snd (β := fun (t : Type (max v w)) ↦ t → C)
      (Sigma.mk (β := fun (t : Type (max v w)) ↦ t → C)
        (CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
        (CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1))
      (Eq.mpr (β :=
        CofilteredClosureSmall.InductiveStep.{w, v, u} (C := C) (max n m + 1) fun (m_1 : ℕ) (x : m_1 < max n m + 1) ↦
          CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f m_1)
        ⋯ (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    eq g g'

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
⊢ EssentiallySmall.{max v w, v, u} (ObjectProperty.FullSubcategory.{v, u} (cofilteredClosure f))

Tactic:
have : LocallySmall.{max v w} (cofilteredClosure f).FullSubcategory :=
    locallySmall_max.{w, v, u}
  have := small_fullSubcategory_cofilteredClosure f
  essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.locallySmall_max, CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure, CategoryTheory.essentiallySmall_of_small_of_locallySmall, CategoryTheory.IsCofiltered.cofilteredClosure, CategoryTheory.ObjectProperty.FullSubcategory
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
⊢ Functor.Faithful (C := SmallCofilteredIntermediate F) (inclusion F)

Tactic:
inferInstanceAs ((equivSmallModel _).inverse ⋙ ObjectProperty.ι _).Faithful

Premises used: _private.0.CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFaithfulInclusion._proof_1
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
⊢ Functor.Full (C := SmallCofilteredIntermediate F) (inclusion F)

Tactic:
inferInstanceAs ((equivSmallModel _).inverse ⋙ ObjectProperty.ι _).Full

Premises used: _private.0.CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullInclusion._proof_1
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
⊢ IsCofilteredOrEmpty (SmallCofilteredIntermediate F)

Tactic:
IsCofilteredOrEmpty.of_equivalence (equivSmallModel _)

Premises used: CategoryTheory.IsCofilteredOrEmpty.of_equivalence, CategoryTheory.equivSmallModel