-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eval_section_surjective_of_surjective (i : J) :
    (fun s : F.sections => s.val i).Surjective := fun x => by
  let s : Set (F.obj i) := {x}
  haveI := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)
  obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)
  refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using h jk⟩, ?_⟩
  · have := (sec i).prop
    simp only [mem_iInter, mem_preimage, mem_singleton_iff] at this
    have := this (𝟙 i)
    rwa [map_id_apply] at this

Proof state:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
⊢ ∃ a, (fun s => ↑s i) a = x

Tactic:
haveI := F.toPreimages_nonempty_of_surjective s Fsur (singleton_nonempty x)

Result:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
⊢ ∃ a, (fun s => ↑s i) a = x

Proof state:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this : ↑(sec i) ∈ ⋂ f, F.map f ⁻¹' s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Tactic:
simp only [mem_iInter, mem_preimage, mem_singleton_iff] at this

Result:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this : ∀ (i_1 : i ⟶ i), F.map i_1 ↑(sec i) ∈ s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Proof state:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Tactic:
have := (sec i).prop

Result:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this : ↑(sec i) ∈ ⋂ f, F.map f ⁻¹' s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Proof state:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
⊢ ∃ a, (fun s => ↑s i) a = x

Tactic:
refine ⟨⟨fun j => (sec j).val, fun jk => by simpa [Subtype.ext_iff] using h jk⟩, ?_⟩

Result:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Proof state:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
⊢ ∃ a, (fun s => ↑s i) a = x

Tactic:
obtain ⟨sec, h⟩ := nonempty_sections_of_finite_cofiltered_system (F.toPreimages s)

Result:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
⊢ ∃ a, (fun s => ↑s i) a = x

Proof state:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
⊢ ∃ a, (fun s => ↑s i) a = x

Tactic:
let s : Set (F.obj i) := {x}

Result:
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
⊢ ∃ a, (fun s => ↑s i) a = x

Proof state:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝¹ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this✝ : ∀ (i_1 : i ⟶ i), F.map i_1 ↑(sec i) ∈ s
this : F.map (𝟙 i) ↑(sec i) ∈ s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Tactic:
rwa [map_id_apply] at this

Result:
no goals

Proof state:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this : ∀ (i_1 : i ⟶ i), F.map i_1 ↑(sec i) ∈ s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x

Tactic:
have := this (𝟙 i)

Result:
case intro
J : Type u
inst✝³ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this✝¹ : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
this✝ : ∀ (i_1 : i ⟶ i), F.map i_1 ↑(sec i) ∈ s
this : F.map (𝟙 i) ↑(sec i) ∈ s
⊢ (fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x