-- Mathlib/Topology/Sheaves/Sheaf.lean
lemma Presheaf.IsSheaf.section_ext {X : TopCat.{u}}
    {A : Type*} [Category.{u} A] {FC : A → A → Type*} {CC : A → Type u}
    [∀ X Y : A, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{u} A FC]
    [HasLimits A] [PreservesLimits (forget A)] [(forget A).ReflectsIsomorphisms]
    {F : TopCat.Presheaf A X} (hF : TopCat.Presheaf.IsSheaf F)
    {U : (Opens X)ᵒᵖ} {s t : ToType (F.obj U)}
    (hst : ∀ x ∈ U.unop, ∃ V, ∃ hV : V ≤ U.unop, x ∈ V ∧
      F.map (homOfLE hV).op s = F.map (homOfLE hV).op t) :
    s = t

Proof state:
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
⊢ s = t

Tactic:
have := (isSheaf_iff_isSheaf_of_type _ _).mp
  ((Presheaf.isSheaf_iff_isSheaf_forget (C := Opens X) (A' := A) _ F (forget _)).mp hF)

Result:
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
⊢ s = t

Proof state:
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
⊢ s = t

Tactic:
choose V hV hxV H using fun x : U.unop ↦ hst x.1 x.2

Result:
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ s = t