-- Mathlib/CategoryTheory/Filtered/OfColimitCommutesFiniteLimit.lean
theorem isFiltered_of_nonempty_limit_colimit_to_colimit_limit
    (h : ∀ {J : Type v} [SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
      Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))) : IsFiltered K

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some

Result:
case intro.intro
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
X : K
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
⊢ IsFiltered K

Tactic:
refine IsFiltered.iff_nonempty_limit.2 (fun {J} _ _ F => ?_)

Result:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
suffices Nonempty (limit (colimit (F.op ⋙ coyoneda).flip)) by
  obtain ⟨X, y, -⟩ := Types.jointly_surjective' (this.map (h (F.op ⋙ coyoneda)).some).some
  exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

Result:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))

Proof state:
case intro.intro
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
this : Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))
X : K
y : (limit (F.op ⋙ coyoneda)).obj X
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
exact ⟨X, ⟨(limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) _).hom y⟩⟩

Result:
no goals

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝² : SmallCategory J
x✝¹ : FinCategory J
F : J ⥤ K
x✝ : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun j =>
    (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j ≪≫
          Coyoneda.colimitCoyonedaIso (F.op.obj j)).toEquiv.unique
⊢ Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))

Tactic:
exact ⟨Types.Limit.mk (colimit (F.op ⋙ coyoneda).flip) (fun j => default) (by subsingleton)⟩

Result:
no goals

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))

Tactic:
let _ (j : Jᵒᵖ) : Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  ((colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip _ ≪≫
    Coyoneda.colimitCoyonedaIso _)).toEquiv.unique

Result:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝² : SmallCategory J
x✝¹ : FinCategory J
F : J ⥤ K
x✝ : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun j =>
    (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j ≪≫
          Coyoneda.colimitCoyonedaIso (F.op.obj j)).toEquiv.unique
⊢ Nonempty (limit (colimit (F.op ⋙ coyoneda).flip))

Proof state:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝² : SmallCategory J
x✝¹ : FinCategory J
F : J ⥤ K
x✝ : (j : Jᵒᵖ) → Unique ((colimit (F.op ⋙ coyoneda).flip).obj j) :=
  fun j =>
    (colimitObjIsoColimitCompEvaluation (F.op ⋙ coyoneda).flip j ≪≫
          Coyoneda.colimitCoyonedaIso (F.op.obj j)).toEquiv.unique
⊢ ∀ (j j' : Jᵒᵖ) (f : j ⟶ j'), (colimit (F.op ⋙ coyoneda).flip).map f ((fun j => default) j) = (fun j => default) j'

Tactic:
subsingleton

Result:
no goals