-- Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
lemma isFiltered_of_isCardinalDirected (J : Type u) [Category.{v} J]
    (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] :
    IsFiltered J

Proof state:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0

Tactic:
simp only [hasCardinalLT_aleph0_iff]

Result:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Finite (Arrow A)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∀ {J_1 : Type w} [inst : SmallCategory J_1] [inst_1 : FinCategory J_1] (F : J_1 ⥤ J), Nonempty (Cocone F)

Tactic:
intro A _ _ F

Result:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Nonempty (Cocone F)

Proof state:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Nonempty (Cocone F)

Tactic:
have hA : HasCardinalLT (Arrow A) κ := by
  refine HasCardinalLT.of_le ?_ hκ.out.aleph0_le
  simp only [hasCardinalLT_aleph0_iff]
  infer_instance

Result:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Proof state:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨cocone F hA⟩

Result:
no goals

Proof state:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ HasCardinalLT (Arrow A) κ

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

Result:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ IsFiltered J

Tactic:
rw [IsFiltered.iff_cocone_nonempty.{w}]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
⊢ ∀ {J_1 : Type w} [inst : SmallCategory J_1] [inst_1 : FinCategory J_1] (F : J_1 ⥤ J), Nonempty (Cocone F)

Proof state:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Finite (Arrow A)

Tactic:
infer_instance

Result:
no goals