awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
obtain :
  ∀ (j : J) (q : Under.mk p ⟶ (Under.lift D s).obj j)
    (hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯),
    ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
obtain ⟨j, q, hq⟩ := exists_hom_of_isColimit (X := Under.mk p) hc' (Under.homMk f rfl)

Premises used: CategoryTheory.Under.homMk, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : Functor.obj (Functor.const J) X ⟶ D
inst_3 : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
j : J
q : Under.mk p ⟶ (Under.lift D s).obj j
hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯
w : J
w₁ : A ⟶ D.obj j
left : p ≫ Under.Hom.right q = s.app j
right : Under.Hom.right q ≫ c.ι.app j = f
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
use j, q.right, Under.w q, congr($(hq).right)

Premises used: CategoryTheory.Under.Hom.right, CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
⊢ HasCardinalFilteredColimits.{w, v, u} C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C

Tactic:
⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩

Premises used: _private.0.CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize.match_2, _private.0.CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize.match_1, Cardinal.aleph0, CategoryTheory.HasCardinalFilteredColimits.mk, CategoryTheory.Limits.HasFilteredColimitsOfSize.mk, Iff.intro, CategoryTheory.HasCardinalFilteredColimits, CategoryTheory.Limits.HasFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
refine_1 :
  HasCardinalFilteredColimits.{w, v, u} C ℵ₀ →
    ∀ (H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C)
      (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
refine_2 :
  HasFilteredColimitsOfSize.{w, w, v, u} C →
    ∀ (H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C) (J : Type w)
      [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C
⊢ HasCardinalFilteredColimits.{w, v, u} C ℵ₀ ↔ HasFilteredColimitsOfSize.{w, w, v, u} C

Tactic:
refine ⟨fun ⟨H⟩ ↦ ⟨?_⟩, fun ⟨H⟩ ↦ ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasCardinalFilteredColimits.{w, v, u} C ℵ₀
H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C
⊢ ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C

Tactic:
simp only [isCardinalFiltered_aleph0_iff] at *

Premises used: CategoryTheory.isCardinalFiltered_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
refine_2 : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C
⊢ ∀ (J : Type w) [inst_1 : SmallCategory J] [IsCardinalFiltered J ℵ₀], HasColimitsOfShape.{w, w, v, u} J C

Tactic:
simp only [isCardinalFiltered_aleph0_iff] at *

Premises used: CategoryTheory.isCardinalFiltered_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasCardinalFilteredColimits.{w, v, u} C ℵ₀
H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C
⊢ ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C

Tactic:
H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasCardinalFilteredColimits.{w, v, u} C ℵ₀
H : ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C
⊢ ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
⊢ ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C

Tactic:
H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
h : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst_1 : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape.{w, w, v, u} I C
⊢ ∀ (J : Type w) [inst_1 : SmallCategory J] [IsFiltered J], HasColimitsOfShape.{w, w, v, u} J C

Tactic:
exact H
-- Module: Mathlib.CategoryTheory.Presentable.Finite
Goal:
C : Type u
inst : Category.{v, u} C
⊢ HasCardinalFilteredColimits C ℵ₀ ↔ HasFilteredColimits.{v, u} C

Tactic:
HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize

Premises used: CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
T : Type u
κ : Cardinal.{w}
hT : HasCardinalLT T κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT.{w, u} (Arrow (WalkingParallelFamily T)) κ

Tactic:
simpa only [hasCardinalLT_iff_of_equiv (WalkingParallelFamily.arrowEquiv T),
    hasCardinalLT_option_iff _ _ hκ] using hT

Premises used: CategoryTheory.Limits.WalkingParallelFamily.arrowEquiv, hasCardinalLT_option_iff, hasCardinalLT_iff_of_equiv
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
⊢ Small.{w, max u' v'} (Arrow.{u', v'} A)

Tactic:
have := hA.small
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this : Small.{w, max u' v'} (Arrow.{u', v'} A)
⊢ Small.{w, v'} A

Tactic:
have := small_of_small_arrow.{w} A
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this_1 : Small.{w, max u' v'} (Arrow.{u', v'} A)
this : Small.{w, v'} A
⊢ LocallySmall.{w, u', v'} A

Tactic:
have := locallySmall_of_small_arrow.{w} A
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this_1 : Small.{w, max u' v'} (Arrow.{u', v'} A)
this_2 : Small.{w, v'} A
this : LocallySmall.{w, u', v'} A
e : Equivalence.{u', w, v', w} A (ShrinkHoms.{w} (Shrink.{w, v'} A)) :=
  Equivalence.trans (Shrink.equivalence A) (ShrinkHoms.equivalence (Shrink.{w, v'} A))
⊢ HasCardinalLT (Arrow (ShrinkHoms.{w} (Shrink.{w, v'} A))) κ

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type v'
inst_2 : Category.{u', v'} A
F : Functor.{u', v, v', u} A J
hA : HasCardinalLT (Arrow.{u', v'} A) κ
this_1 : Small.{w, max u' v'} (Arrow.{u', v'} A)
this_2 : Small.{w, v'} A
this : LocallySmall.{w, u', v'} A
e : Equivalence.{u', w, v', w} A (ShrinkHoms.{w} (Shrink.{w, v'} A)) :=
  Equivalence.trans (Shrink.equivalence A) (ShrinkHoms.equivalence (Shrink.{w, v'} A))
⊢ Cocone F

Tactic:
exact (Cocone.equivalenceOfReindexing e.symm (Iso.refl _)).inverse.obj
    (nonempty_cocone (κ := κ) (e.inverse ⋙ F) (by simpa)).some

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, Nonempty.some, CategoryTheory.IsCardinalFiltered.nonempty_cocone, CategoryTheory.Limits.Cocone.equivalenceOfReindexing, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
K : Type u'
S : K → J
hS : HasCardinalLT K κ
⊢ HasCardinalLT.{w, u'} (Arrow (Discrete K)) κ

Tactic:
simpa using hS
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
K : Type u'
S : K → J
hS : HasCardinalLT K κ
k : K
⊢ HasCardinalLT.{w, u'} (Arrow (Discrete K)) κ

Tactic:
simpa using hS
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
K : Type v'
j j' : J
f : K → (j ⟶ j')
hK : HasCardinalLT K κ
k : K
⊢ Eq (α := j ⟶ coeq f hK) (f k ≫ coeqHom f hK) (toCoeq f hK)

Tactic:
(cocone (parallelFamily f)
    (hasCardinalLT_arrow_walkingParallelFamily hK hκ.out.aleph0_le)).w
    (.line k)

Premises used: CategoryTheory.IsCardinalFiltered.cocone, CategoryTheory.IsCardinalFiltered.toCoeq, CategoryTheory.Limits.WalkingParallelFamily.Hom.line, CategoryTheory.ShrinkHoms.toShrinkHoms, Cardinal.IsRegular.aleph0_le, CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily, CategoryTheory.Limits.parallelFamily, CategoryTheory.ShrinkHoms.fromShrinkHoms, CategoryTheory.Limits.Cocone.w, CategoryTheory.IsCardinalFiltered.coeqHom, CategoryTheory.IsCardinalFiltered.coeq, CategoryTheory.ShrinkHoms, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
φ : (i : ι) → j ⟶ max.{w, v, v', u} k hι := fun (i : ι) ↦ f i ≫ toMax k hι i
⊢ ∀ (i : ι),
    Eq (α := j ⟶ coeq φ hι) (f i ≫ (fun (i : ι) ↦ (toMax k hι i ≫ coeqHom φ hι : k i ⟶ coeq φ hι)) i) (toCoeq φ hι)

Tactic:
simpa [φ] using coeq_condition φ hι

Premises used: CategoryTheory.IsCardinalFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
ι : Type v'
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
φ : (i : ι) → j ⟶ max.{w, v, v', u} k hι := fun (i : ι) ↦ f i ≫ toMax k hι i
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b

Tactic:
exact ⟨coeq φ hι, fun i ↦ toMax k hι i ≫ coeqHom φ hι,
    toCoeq φ hι, by simpa [φ] using coeq_condition φ hι⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
rw :
  ∀ {J_1 : Type w} [inst_2 : SmallCategory J_1] [FinCategory J_1] (F : Functor.{w, v, w, u} J_1 J), Nonempty (Cocone F)
⊢ IsFiltered.{v, u} J

Tactic:
rw [IsFiltered.iff_cocone_nonempty.{w}]
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
_ : ∀ [inst_2 : SmallCategory A] [FinCategory A] (F : Functor.{w, v, w, u} A J), Nonempty (Cocone F)
⊢ ∀ [inst_2 : SmallCategory A] [FinCategory A] (F : Functor.{w, v, w, u} A J), Nonempty (Cocone F)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
_ : ∀ [FinCategory A] (F : Functor.{w, v, w, u} A J), Nonempty (Cocone F)
⊢ ∀ [FinCategory A] (F : Functor.{w, v, w, u} A J), Nonempty (Cocone F)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ HasCardinalLT (Arrow A) κ

Tactic:
HasCardinalLT.of_le ?_ hκ.out.aleph0_le

Premises used: Cardinal.IsRegular.aleph0_le, HasCardinalLT.of_le, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
refine : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ HasCardinalLT (Arrow A) κ

Tactic:
refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le

Premises used: Cardinal.IsRegular.aleph0_le, HasCardinalLT.of_le, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
simp : Finite.{w + 1} (Arrow A)
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0

Tactic:
simp only [hasCardinalLT_aleph0_iff]

Premises used: hasCardinalLT_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ Finite.{w + 1} (Arrow A)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
⊢ HasCardinalLT (Arrow A) κ

Tactic:
have hA : HasCardinalLT (Arrow A) κ := by
    refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
    simp only [hasCardinalLT_aleph0_iff]
    infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
⟨cocone F hA⟩

Premises used: CategoryTheory.IsCardinalFiltered.cocone, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
A : Type w
inst_2 : SmallCategory A
inst_3 : FinCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨cocone F hA⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst_1 : IsCardinalFiltered.{w, v, u} J κ
⊢ Nonempty J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
  IsFiltered.nonempty

Premises used: CategoryTheory.isFiltered_of_isCardinalFiltered, CategoryTheory.IsFiltered.nonempty
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
mp : IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 → IsFiltered.{v, u} J
mpr : IsFiltered.{v, u} J → IsCardinalFiltered.{w, v, u} J Cardinal.aleph0
⊢ IsCardinalFiltered.{w, v, u} J Cardinal.aleph0 ↔ IsFiltered.{v, u} J

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsCardinalFiltered.{w, v, u} J Cardinal.aleph0
⊢ IsFiltered.{v, u} J

Tactic:
isFiltered_of_isCardinalFiltered J Cardinal.aleph0

Premises used: CategoryTheory.isFiltered_of_isCardinalFiltered, Cardinal.aleph0
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsCardinalFiltered.{w, v, u} J Cardinal.aleph0
⊢ IsFiltered.{v, u} J

Tactic:
exact isFiltered_of_isCardinalFiltered J Cardinal.aleph0

Premises used: CategoryTheory.isFiltered_of_isCardinalFiltered, Cardinal.aleph0
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
mpr :
  ∀ {A : Type w} [inst_1 : SmallCategory A] (F : Functor.{w, v, w, u} A J)
    (hA : HasCardinalLT (Arrow A) Cardinal.aleph0), Nonempty (Cocone F)
⊢ IsCardinalFiltered.{w, v, u} J Cardinal.aleph0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
mpr :
  ∀ [inst_1 : SmallCategory A] (F : Functor.{w, v, w, u} A J) (hA : HasCardinalLT (Arrow A) Cardinal.aleph0),
    Nonempty (Cocone F)
⊢ ∀ [inst_1 : SmallCategory A] (F : Functor.{w, v, w, u} A J) (hA : HasCardinalLT (Arrow A) Cardinal.aleph0),
    Nonempty (Cocone F)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) Cardinal.aleph0
⊢ Finite.{w + 1} (Arrow A)

Tactic:
rw [hasCardinalLT_aleph0_iff] at hA

Premises used: hasCardinalLT_aleph0_iff
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : Finite.{w + 1} (Arrow A)
mpr : ∀ (this : FinCategory A), Nonempty (Cocone F)
⊢ Nonempty (Cocone F)

Tactic:
have := ((Arrow.finite_iff A).1 hA).some
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : Finite.{w + 1} (Arrow A)
this : FinCategory A
⊢ Nonempty (Cocone F)

Tactic:
⟨IsFiltered.cocone F⟩

Premises used: CategoryTheory.IsFiltered.cocone, Nonempty.intro
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
h : IsFiltered.{v, u} J
A : Type w
inst_1 : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : Finite.{w + 1} (Arrow A)
this : FinCategory A
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨IsFiltered.cocone F⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type w
inst : Preorder J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j
A : Type w
x : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Cardinal.mk A < κ

Tactic:
simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
        hasCardinalLT_of_hasCardinalLT_arrow hA

Premises used: hasCardinalLT_iff_cardinal_mk_lt, CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type w
inst : Preorder J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j
A : Type w
x : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
obtain : ∀ (j : J) (hj : ∀ (k : A), F.obj k ≤ j), Nonempty.{w + 1} (Cocone F)
⊢ Nonempty.{w + 1} (Cocone F)

Tactic:
obtain ⟨j, hj⟩ := h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
        hasCardinalLT_of_hasCardinalLT_arrow hA)

Premises used: CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type w
inst : Preorder J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j
A : Type w
x : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (k : A), F.obj k ≤ j
⊢ Nonempty.{w + 1} (Cocone F)

Tactic:
⟨Cocone.mk j
      { app a := homOfLE (hj a)
        naturality _ _ _ := rfl }⟩

Premises used: CategoryTheory.Limits.Cocone.mk, Nonempty.intro, CategoryTheory.NatTrans.mk, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type w
inst : Preorder J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ (j : J), ∀ (k : K), s k ≤ j
A : Type w
x : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (k : A), F.obj k ≤ j
⊢ Nonempty.{w + 1} (Cocone F)

Tactic:
exact ⟨Cocone.mk j
      { app a := homOfLE (hj a)
        naturality _ _ _ := rfl }⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
x : { x : κ.ord.ToType // x ∈ Set.range f }
⊢ ∃ (a : ι),
    (fun (i : ι) ↦
          (Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯ :
            { x : κ.ord.ToType // x ∈ Set.range f }))
        a =
      x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
⊢ Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯

Tactic:
have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
hs : Cardinal.mk ι < κ
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
contrapose! : ∀ (hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k), κ ≤ Cardinal.mk ι
⊢ ∃ (j : κ.ord.ToType), ∀ (k : ι), f k ≤ j

Tactic:
contrapose! hs
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
rw : Order.cof κ.ord.ToType ≤ Cardinal.mk ι
⊢ κ ≤ Cardinal.mk ι

Tactic:
rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]

Premises used: Cardinal.IsRegular.cof_ord, Ordinal.cof_toType, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι

Tactic:
(Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)

Premises used: Cardinal.mk_le_of_surjective, Order.cof_le, LE.le.trans