awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
u : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
refine_2 :
  Eq (α := (↑(F.obj (coeq u v)) : Type u_2))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
refine_2₁ :
  Eq (α :=
    { base := c, fiber := f : Grothendieck F } ⟶
      { base := coeq u v,
        fiber :=
          coeq (j :=
            Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
              ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
            (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
            (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })
    ({ base := u, fiber := x :
        { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
      { base := coeqHom u v,
        fiber :=
          coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
            (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })
    ({ base := v, fiber := y :
        { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
      { base := coeqHom u v,
        fiber :=
          coeqHom (eqToHom ⋯ ≫ Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) x)
            (Functor.map (Cat.Hom.toFunctor (F.map (coeqHom u v))) y) })
⊢ ∃ (Z : Grothendieck F) (h : { base := d, fiber := g : Grothendieck F } ⟶ Z),
    Eq (α := { base := c, fiber := f : Grothendieck F } ⟶ Z)
      ({ base := u, fiber := x :
          { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
        h)
      ({ base := v, fiber := y :
          { base := c, fiber := f : Grothendieck F }.Hom { base := d, fiber := g : Grothendieck F } } ≫
        h)

Tactic:
refine ⟨⟨coeq u v, coeq (eqToHom ?_ ≫
        (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y)⟩,
          ⟨coeqHom u v, coeqHom _ _⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
u : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
rw :
  Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
    ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber)
| Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
    ((F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber)

Tactic:
rw [← Cat.Hom.comp_obj, ← F.map_comp, coeq_condition, F.map_comp,
        Cat.Hom.comp_obj]

Premises used: CategoryTheory.Cat.Hom.comp_obj, CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFilteredOrEmpty.{v, u} C
inst_2 : ∀ (c : C), IsFilteredOrEmpty.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
d : C
g : (↑(F.obj d) : Type u_2)
u : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f : Grothendieck F }.base ⟶ { base := d, fiber := g : Grothendieck F }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber ⟶ { base := d, fiber := g }.fiber
conv_rhs :
  Eq (α := (↑(F.obj (coeq u v)) : Type u_2))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
refine_2 :
  Eq (α := (↑(F.obj (coeq u v)) : Type u_2))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
⊢ Eq (α := (↑(F.obj (coeq u v)) : Type u_2))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map v).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))
    (Functor.obj (Cat.Hom.toFunctor (F.map (coeqHom u v)))
      ((F.map u).toFunctor.obj { base := c, fiber := f : Grothendieck F }.fiber))

Tactic:
conv_rhs => rw [← Cat.Hom.comp_obj, ← F.map_comp, coeq_condition, F.map_comp,
        Cat.Hom.comp_obj]

Premises used: CategoryTheory.Cat.Hom.comp_obj, CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
⊢ Nonempty C

Tactic:
IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
obtain : ∀ (c : C), Nonempty (Grothendieck F)
⊢ Nonempty (Grothendieck F)

Tactic:
obtain ⟨c⟩ : Nonempty C := IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty, Nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
⊢ Nonempty.{u_2 + 1} (↑(F.obj c) : Type u_2)

Tactic:
IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
obtain : ∀ (f : (↑(F.obj c) : Type u_2)), Nonempty (Grothendieck F)
⊢ Nonempty (Grothendieck F)

Tactic:
obtain ⟨f⟩ : Nonempty (F.obj c) := IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty, CategoryTheory.Bundled.α, Nonempty, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
⊢ Nonempty (Grothendieck F)

Tactic:
⟨⟨c, f⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Grothendieck.mk
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
c : C
f : (↑(F.obj c) : Type u_2)
⊢ Nonempty (Grothendieck F)

Tactic:
exact ⟨⟨c, f⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
⊢ Nonempty (Grothendieck F)

Tactic:
have : Nonempty (Grothendieck F) := by
    obtain ⟨c⟩ : Nonempty C := IsFiltered.nonempty
    obtain ⟨f⟩ : Nonempty (F.obj c) := IsFiltered.nonempty
    exact ⟨⟨c, f⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
inst_1 : IsFiltered.{v, u} C
inst_2 : ∀ (c : C), IsFiltered.{u_1, u_2} (↑(F.obj c) : Type u_2)
this : Nonempty (Grothendieck F)
⊢ IsFiltered (Grothendieck F)

Tactic:
apply IsFiltered.mk

Premises used: CategoryTheory.IsFiltered.mk
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
α : Type w
f : α → C
⊢ EssentiallySmall.{max v w, v, u} (ObjectProperty.FullSubcategory.{v, u} (filteredClosure f))

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

Premises used: CategoryTheory.locallySmall_max, CategoryTheory.essentiallySmall_of_small_of_locallySmall, CategoryTheory.IsFiltered.small_fullSubcategory_filteredClosure, CategoryTheory.IsFiltered.filteredClosure, CategoryTheory.ObjectProperty.FullSubcategory
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
⊢ Functor.Faithful (C := SmallFilteredIntermediate F) (inclusion F)

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

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

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

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

Tactic:
IsFilteredOrEmpty.of_equivalence (equivSmallModel _)

Premises used: CategoryTheory.IsFilteredOrEmpty.of_equivalence, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
F : Functor.{v₁, v, u₁, u} D C
inst_3 : Nonempty D
⊢ IsFiltered (SmallFilteredIntermediate F)

Tactic:
{ (inferInstance : IsFilteredOrEmpty _) with
    nonempty := Nonempty.map (factoring F).obj inferInstance }

Premises used: CategoryTheory.IsFiltered.mk, inferInstance
-- Module: Mathlib.CategoryTheory.Filtered.Small
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
α : Type w
f : α → C
⊢ Small.{max v w, u} (ObjectProperty.FullSubcategory.{v, u} (cofilteredClosure f))

Tactic:
small_of_injective_of_exists
    (CofilteredClosureSmall.abstractCofilteredClosureRealization f)
    (fun _ _ => ObjectProperty.FullSubcategory.ext) ?_

Premises used: small_of_injective_of_exists, CategoryTheory.ObjectProperty.FullSubcategory.ext, _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
refine :
  ∀ (b : ObjectProperty.FullSubcategory.{v, u} (cofilteredClosure f)),
    ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
      CofilteredClosureSmall.abstractCofilteredClosureRealization f a = b.obj (P := cofilteredClosure f)
⊢ Small.{max v w, u} (ObjectProperty.FullSubcategory.{v, u} (cofilteredClosure f))

Tactic:
refine small_of_injective_of_exists
    (CofilteredClosureSmall.abstractCofilteredClosureRealization f)
    (fun _ _ => ObjectProperty.FullSubcategory.ext) ?_

Premises used: small_of_injective_of_exists, _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
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) ⋯)

Tactic:
⟨⟨0, ?_⟩,?_⟩

Premises used: Exists.intro, Sigma.mk, OfNat.ofNat
-- 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
x : α
base :
  (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f 0).fst (β := fun (t : Type (max v w)) ↦ t → C)
base₁ :
  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))
        0 (id { down := x : ULift.{v, w} α })) =
    ObjectProperty.FullSubcategory.obj (P := cofilteredClosure f)
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (f 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) ⋯)

Tactic:
refine ⟨⟨0, ?_⟩,?_⟩
-- 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
x : α
base : ULift.{v, w} α
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure.{w, v, u} f 0).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
x : α
⊢ ULift.{v, w} α

Tactic:
exact ULift.up x

Premises used: ULift.up
-- 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
x : α
base : (f ∘ ULift.down) (id { down := x : ULift.{v, w} α }) = f 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))
        0 (id { down := x : ULift.{v, w} α })) =
    ObjectProperty.FullSubcategory.obj (P := cofilteredClosure f)
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f) (f x) ⋯)

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization,
        CofilteredClosureSmall.bundledAbstractCofilteredClosure]

Premises used: _private.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure, _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
x : α
⊢ (f ∘ ULift.down) (id { down := x : ULift.{v, w} α }) = f x

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
j j_1 j' : C
hj₁ : cofilteredClosure.{w, v, u} f j_1
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_1 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)
min :
  ∀ (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))),
    ∃ (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))
                j')
              ⋯).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_1 j') ⋯).obj (P :=
        cofilteredClosure f)

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

Premises used: 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
j j' : C
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)
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))
min :
  ∀ (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))),
    ∃ (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)
⊢ ∃ (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))
              j')
            ⋯).obj
        (P := cofilteredClosure f)

Tactic:
rcases ih' with ⟨⟨m, y⟩, rfl⟩

Premises used: 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
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))
⊢ ∃ (a : CofilteredClosureSmall.AbstractCofilteredClosure.{w, v, u} f),
    CofilteredClosureSmall.abstractCofilteredClosureRealization f a =
      (ObjectProperty.FullSubcategory.mk (P := cofilteredClosure f)
            (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)

Tactic:
⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩

Premises used: Max.max, Exists.intro, Sigma.mk, Nat.succ