awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
J' : Type u_1
inst_2 : Category.{v_1, u_1} J'
inst_3 : FinallySmall.{w, v, u} J
inst_4 : FinallySmall.{w', v_1, u_1} J'
⊢ FinallySmall (J × J')

Tactic:
finallySmall_of_final_of_essentiallySmall
    ((fromFinalModel.{w} J).prod (fromFinalModel.{w'} J'))

Premises used: CategoryTheory.Functor.prod, CategoryTheory.fromFinalModel, CategoryTheory.finallySmall_of_final_of_essentiallySmall
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
S : Type w
inst_1 : SmallCategory S
F : Functor.{w, v, w, u} S J
inst_2 : F.Initial
⊢ InitiallySmall.{w, v, u} J

Tactic:
⟨S, _, F, inferInstance⟩

Premises used: inferInstance, CategoryTheory.InitiallySmall.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
⊢ Initial.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J)

Tactic:
Classical.choose_spec (Classical.choose_spec (Classical.choose_spec
    (@InitiallySmall.initial_smallCategory J _ _)))

Premises used: CategoryTheory.InitialModel, CategoryTheory.fromInitialModel, Classical.choose_spec, CategoryTheory.InitiallySmall.initial_smallCategory
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : EssentiallySmall.{w, v, u} J
⊢ InitiallySmall.{w, v, u} J

Tactic:
InitiallySmall.mk' (equivSmallModel.{w} J).inverse

Premises used: CategoryTheory.InitiallySmall.mk', CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : InitiallySmall.{w, v₁, u₁} K
F : Functor.{v₁, v, u₁, u} K J
inst_3 : F.Initial
⊢ InitiallySmall.{w, v, u} J

Tactic:
suffices Initial ((fromInitialModel K) ⋙ F) from .mk' ((fromInitialModel K) ⋙ F)
  initial_comp _ _

Premises used: CategoryTheory.Functor.initial_comp, CategoryTheory.Functor.comp, CategoryTheory.fromInitialModel, CategoryTheory.InitiallySmall.mk'
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : EssentiallySmall.{w, v₁, u₁} K
F : Functor.{v₁, v, u₁, u} K J
inst_3 : F.Initial
⊢ InitiallySmall.{w, v, u} J

Tactic:
have := initiallySmall_of_essentiallySmall K
  initiallySmall_of_initial_of_initiallySmall F

Premises used: CategoryTheory.initiallySmall_of_initial_of_initiallySmall, CategoryTheory.initiallySmall_of_essentiallySmall
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : Limits.HasInitial.{v, u} J
⊢ InitiallySmall.{w, v, u} J

Tactic:
have := Functor.initial_const_initial (C := PUnit.{w + 1}) (D := J)
  .mk' ((Functor.const PUnit.{w + 1}).obj (⊥_ J))

Premises used: CategoryTheory.Functor.initial_const_initial, CategoryTheory.InitiallySmall.mk', PUnit, CategoryTheory.Functor.const, CategoryTheory.Limits.initial, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : LocallySmall.{w, v, u} J
inst_3 : InitiallySmall.{w, v, u} J
X : J
⊢ InitiallySmall (CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) X)

Tactic:
have : InitiallySmall.{w} (CostructuredArrow (fromInitialModel.{w} J) X) :=
    initiallySmall_of_essentiallySmall _
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : LocallySmall.{w, v, u} J
inst_3 : InitiallySmall.{w, v, u} J
X : J
this : InitiallySmall (CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) X)
⊢ InitiallySmall (Over.{v, u} X)

Tactic:
initiallySmall_of_initial_of_initiallySmall
    (CostructuredArrow.toOver (fromInitialModel.{w} J) X)

Premises used: CategoryTheory.initiallySmall_of_initial_of_initiallySmall, CategoryTheory.fromInitialModel, CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : LocallySmall.{w, v, u} J
inst_3 : InitiallySmall.{w, v, u} J
X : J
this : InitiallySmall (CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) X)
⊢ InitiallySmall (Over.{v, u} X)

Tactic:
exact initiallySmall_of_initial_of_initiallySmall
    (CostructuredArrow.toOver (fromInitialModel.{w} J) X)
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
J' : Type u_1
inst_2 : Category.{v_1, u_1} J'
inst_3 : InitiallySmall.{w, v, u} J
inst_4 : InitiallySmall.{w', v_1, u_1} J'
⊢ InitiallySmall (J × J')

Tactic:
initiallySmall_of_initial_of_essentiallySmall
    ((fromInitialModel.{w} J).prod (fromInitialModel.{w'} J'))

Premises used: CategoryTheory.fromInitialModel, CategoryTheory.Functor.prod, CategoryTheory.initiallySmall_of_initial_of_essentiallySmall
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
⊢ ∃ (s : Set J) (_ : Small.{w, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)

Tactic:
⟨Set.range (fromFinalModel J).obj, inferInstance, fun i => ?_⟩

Premises used: inferInstance, CategoryTheory.fromFinalModel, Exists.intro, Set.range, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
refine :
  ∀ (i : J), ∃ j ∈ Set.range.{u, w + 1} (ι := FinalModel.{w, v, u} J) (obj (fromFinalModel J)), Nonempty.{v + 1} (i ⟶ j)
⊢ ∃ (s : Set J) (_ : Small.{w, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)

Tactic:
refine ⟨Set.range (fromFinalModel J).obj, inferInstance, fun i => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
i : J
⊢ Nonempty (StructuredArrow.{w, v, w, u} (C := FinalModel.{w, v, u} J) i (fromFinalModel J))

Tactic:
IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
i : J
obtain :
  ∀ (f : StructuredArrow.{w, v, w, u} (C := FinalModel.{w, v, u} J) i (fromFinalModel J)),
    ∃ j ∈ Set.range.{u, w + 1} (ι := FinalModel.{w, v, u} J) (obj (fromFinalModel J)), Nonempty.{v + 1} (i ⟶ j)
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := FinalModel.{w, v, u} J) (obj (fromFinalModel J)), Nonempty.{v + 1} (i ⟶ j)

Tactic:
obtain ⟨f⟩ : Nonempty (StructuredArrow i (fromFinalModel J)) := IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty, CategoryTheory.fromFinalModel, Nonempty, CategoryTheory.StructuredArrow
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
i : J
f : StructuredArrow.{w, v, w, u} (C := FinalModel.{w, v, u} J) i (fromFinalModel J)
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := FinalModel.{w, v, u} J) (obj (fromFinalModel J)), Nonempty.{v + 1} (i ⟶ j)

Tactic:
⟨(fromFinalModel J).obj f.right, Set.mem_range_self _, ⟨f.hom⟩⟩

Premises used: Set.mem_range_self, CategoryTheory.StructuredArrow.hom, Nonempty.intro, CategoryTheory.fromFinalModel, And.intro, Exists.intro, CategoryTheory.StructuredArrow.right, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
i : J
f : StructuredArrow.{w, v, w, u} (C := FinalModel.{w, v, u} J) i (fromFinalModel J)
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := FinalModel.{w, v, u} J) (obj (fromFinalModel J)), Nonempty.{v + 1} (i ⟶ j)

Tactic:
exact ⟨(fromFinalModel J).obj f.right, Set.mem_range_self _, ⟨f.hom⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
suffices :
  Final.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)
⊢ FinallySmall.{v, v, u} J

Tactic:
suffices Functor.Final (ObjectProperty.ι (· ∈ s)) from
    finallySmall_of_final_of_essentiallySmall (ObjectProperty.ι (· ∈ s))
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
⊢ Final.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)

Tactic:
Functor.final_of_exists_of_isFiltered_of_fullyFaithful _ (fun i => ?_)

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
refine :
  ∀ (i : J),
    ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
      Nonempty.{v + 1} (i ⟶ obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c)
⊢ Final.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)

Tactic:
refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful _ (fun i => ?_)

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
i : J
obtain :
  ∀ (j : J) (hj₁ : j ∈ s) (hj₂ : Nonempty.{v + 1} (i ⟶ j)),
    ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
      Nonempty.{v + 1} (i ⟶ obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (i ⟶ obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c)

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hs i
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty.{v + 1} (i ⟶ j)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (i ⟶ obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c)

Tactic:
⟨⟨j, hj₁⟩, hj₂⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty.{v + 1} (i ⟶ j)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (i ⟶ obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c)

Tactic:
exact ⟨⟨j, hj₁⟩, hj₂⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
⊢ FinallySmall.{v, v, u} J ↔
    ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)

Tactic:
⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩

Premises used: CategoryTheory.FinallySmall.exists_small_weakly_terminal_set, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
refine :
  ∀ (h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)),
    FinallySmall.{v, v, u} J
⊢ FinallySmall.{v, v, u} J ↔
    ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)

Tactic:
refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
rcases :
  ∀ (s : Set J) (hs : Small.{v, u} (↑s : Type u)) (hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)),
    FinallySmall.{v, v, u} J
⊢ FinallySmall.{v, v, u} J

Tactic:
rcases h with ⟨s, hs, hs'⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
hs : Small.{v, u} (↑s : Type u)
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
⊢ FinallySmall.{v, v, u} J

Tactic:
finallySmall_of_small_weakly_terminal_set s hs'

Premises used: CategoryTheory.finallySmall_of_small_weakly_terminal_set
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFilteredOrEmpty.{v, u} J
s : Set J
hs : Small.{v, u} (↑s : Type u)
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (i ⟶ j)
⊢ FinallySmall.{v, v, u} J

Tactic:
exact finallySmall_of_small_weakly_terminal_set s hs'

Premises used: CategoryTheory.finallySmall_of_small_weakly_terminal_set
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
⊢ ∃ (s : Set J) (_ : Small.{w, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)

Tactic:
⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩

Premises used: inferInstance, CategoryTheory.fromInitialModel, Exists.intro, Set.range, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
refine :
  ∀ (i : J),
    ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)
⊢ ∃ (s : Set J) (_ : Small.{w, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)

Tactic:
refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
i : J
⊢ Nonempty (CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) i)

Tactic:
IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
i : J
obtain :
  ∀ (f : CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) i),
    ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)

Tactic:
obtain ⟨f⟩ : Nonempty (CostructuredArrow (fromInitialModel J) i) := IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty, CategoryTheory.CostructuredArrow, CategoryTheory.fromInitialModel, Nonempty
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
i : J
f : CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) i
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)

Tactic:
⟨(fromInitialModel J).obj f.left, Set.mem_range_self _, ⟨f.hom⟩⟩

Premises used: Set.mem_range_self, CategoryTheory.CostructuredArrow.hom, CategoryTheory.fromInitialModel, Nonempty.intro, And.intro, Exists.intro, CategoryTheory.CostructuredArrow.left, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
i : J
f : CostructuredArrow.{w, v, w, u} (C := InitialModel.{w, v, u} J) (fromInitialModel J) i
⊢ ∃ j ∈ Set.range.{u, w + 1} (ι := InitialModel.{w, v, u} J) (obj (fromInitialModel J)), Nonempty.{v + 1} (j ⟶ i)

Tactic:
exact ⟨(fromInitialModel J).obj f.left, Set.mem_range_self _, ⟨f.hom⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
suffices :
  Initial.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)
⊢ InitiallySmall.{v, v, u} J

Tactic:
suffices Functor.Initial (ObjectProperty.ι (· ∈ s)) from
    initiallySmall_of_initial_of_essentiallySmall (ObjectProperty.ι (· ∈ s))
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ Initial.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)

Tactic:
Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
refine :
  ∀ (i : J),
    ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
      Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)
⊢ Initial.{v, v, u, u} (C := ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s)
    (ObjectProperty.ι fun (x : J) ↦ x ∈ s)

Tactic:
refine Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful _ (fun i => ?_)

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
i : J
obtain :
  ∀ (j : J) (hj₁ : j ∈ s) (hj₂ : Nonempty.{v + 1} (j ⟶ i)),
    ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
      Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hs i
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty.{v + 1} (j ⟶ i)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)

Tactic:
⟨⟨j, hj₁⟩, hj₂⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
inst_2 : Small.{v, u} (↑s : Type u)
hs : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty.{v + 1} (j ⟶ i)
⊢ ∃ (c : ObjectProperty.FullSubcategory.{v, u} (C := J) fun (x : J) ↦ x ∈ s),
    Nonempty.{v + 1} (obj (ObjectProperty.ι fun (x : J) ↦ x ∈ s) c ⟶ i)

Tactic:
exact ⟨⟨j, hj₁⟩, hj₂⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
⊢ InitiallySmall.{v, v, u} J ↔
    ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)

Tactic:
⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩

Premises used: CategoryTheory.InitiallySmall.exists_small_weakly_initial_set, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
refine :
  ∀ (h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)),
    InitiallySmall.{v, v, u} J
⊢ InitiallySmall.{v, v, u} J ↔
    ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)

Tactic:
refine ⟨fun _ => InitiallySmall.exists_small_weakly_initial_set _, fun h => ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
h : ∃ (s : Set J) (_ : Small.{v, u} (↑s : Type u)), ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
rcases :
  ∀ (s : Set J) (hs : Small.{v, u} (↑s : Type u)) (hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)),
    InitiallySmall.{v, v, u} J
⊢ InitiallySmall.{v, v, u} J

Tactic:
rcases h with ⟨s, hs, hs'⟩
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
hs : Small.{v, u} (↑s : Type u)
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ InitiallySmall.{v, v, u} J

Tactic:
initiallySmall_of_small_weakly_initial_set s hs'

Premises used: CategoryTheory.initiallySmall_of_small_weakly_initial_set
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsCofilteredOrEmpty.{v, u} J
s : Set J
hs : Small.{v, u} (↑s : Type u)
hs' : ∀ (i : J), ∃ j ∈ s, Nonempty.{v + 1} (j ⟶ i)
⊢ InitiallySmall.{v, v, u} J

Tactic:
exact initiallySmall_of_small_weakly_initial_set s hs'

Premises used: CategoryTheory.initiallySmall_of_small_weakly_initial_set
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
C : Type u₁
inst_2 : Category.{v₁, u₁} C
inst_3 : HasColimitsOfSize.{w, w, v₁, u₁} C
⊢ HasColimitsOfShape.{v, u, v₁, u₁} J C

Tactic:
Final.hasColimitsOfShape_of_final (fromFinalModel J)

Premises used: CategoryTheory.Functor.Final.hasColimitsOfShape_of_final, CategoryTheory.fromFinalModel
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : InitiallySmall.{w, v, u} J
C : Type u₁
inst_2 : Category.{v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
⊢ HasLimitsOfShape.{v, u, v₁, u₁} J C

Tactic:
Initial.hasLimitsOfShape_of_initial (fromInitialModel J)

Premises used: CategoryTheory.fromInitialModel, CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type
inst : SmallCategory J
K : J ⥤ FintypeCat
j : J
simp : Finite.{u + 1} (K.obj j).obj
⊢ Finite.{u + 1} ((K ⋙ FintypeCat.incl).obj j)

Tactic:
simp only [comp_obj, FintypeCat.incl_obj]

Premises used: CategoryTheory.Functor.comp_obj, FintypeCat.incl_obj
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type
inst : SmallCategory J
K : J ⥤ FintypeCat
j : J
⊢ Finite.{u + 1} (K.obj j).obj

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u_1
inst_2 : ∀ (j : J), Finite.{u_1 + 1} (K.obj j)
have : (this : Fintype (↑K.sections : Type u_1)) → Fintype (limit K)
⊢ Fintype (limit K)

Tactic:
have : Fintype (sections K) := Fintype.ofFinite (sections K)
-- Module: Mathlib.CategoryTheory.Limits.FintypeCat
Goal:
J : Type
inst : SmallCategory J
inst_1 : FinCategory J
K : J ⥤ Type u_1
inst_2 : ∀ (j : J), Finite.{u_1 + 1} (K.obj j)
this : Fintype (↑K.sections : Type u_1)
⊢ Fintype (limit K)

Tactic:
exact Fintype.ofEquiv (sections K) (Types.limitEquivSections K).symm

Premises used: Set.Elem, Fintype.ofEquiv, CategoryTheory.Limits.Types.limitEquivSections, Equiv.symm, CategoryTheory.Functor.sections