J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
⊢ _root_.Nonempty ((toPreimages F s).obj j)
simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]
case inl
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
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 J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
ji : j ⟶ i
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)
no goals
case inl
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
h : IsEmpty (j ⟶ i)
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
exact ⟨(hFn j).some, fun ji => h.elim ji⟩
case inr.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.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
case inr.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
hs : Set.Nonempty s
j : J
ji : j ⟶ i
⊢ ∃ x, ∀ (i_1 : j ⟶ i), F.map i_1 x ∈ s
obtain ⟨y, ys⟩ := hs
case inr.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.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
case inr.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.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
obtain ⟨x, rfl⟩ := Fsur ji y
no goals
case inr.intro.intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j✝ k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), _root_.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
exact ⟨x, fun ji' => (F.thin_diagram_of_surjective Fsur ji' ji).symm ▸ ys⟩