-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem toPreimages_nonempty_of_surjective [hFn : ∀ j : J, Nonempty (F.obj j)]
    (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) (hs : s.Nonempty) (j) :
    Nonempty ((F.toPreimages s).obj j)

Proof state:
case inl
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
h : IsEmpty (j ⟶ i)
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Tactic:
exact ⟨(hFn j).some, fun ji => h.elim ji⟩

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
⊢ Nonempty ((F.toPreimages s).obj j)

Tactic:
simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]

Result:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Tactic:
obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)

Result:
case inl
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
h : IsEmpty (j ⟶ i)
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

case inr.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
ji : j ⟶ i
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Proof state:
case inr.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j : J
ji : j ⟶ i
y : F.obj i
ys : y ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Tactic:
obtain ⟨x, rfl⟩ := Fsur ji y

Result:
case inr.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j : J
ji : j ⟶ i
x : F.obj j
ys : F.map ji x ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Proof state:
case inr.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : s.Nonempty
j : J
ji : j ⟶ i
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Tactic:
obtain ⟨y, ys⟩ := hs

Result:
case inr.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j : J
ji : j ⟶ i
y : F.obj i
ys : y ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Proof state:
case inr.intro.intro.intro
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
j : J
ji : j ⟶ i
x : F.obj j
ys : F.map ji x ∈ s
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s

Tactic:
exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩

Result:
no goals