-- Mathlib/Topology/Sheaves/Stalks.lean
theorem app_surjective_of_injective_of_locally_surjective {F G : Sheaf C X} (f : F ⟶ G)
    (U : Opens X) (hinj : ∀ x ∈ U, Function.Injective ((stalkFunctor C x).map f.1))
    (hsurj : ∀ (t x) (_ : x ∈ U), ∃ (V : Opens X) (_ : x ∈ V) (iVU : V ⟶ U)
    (s : ToType (F.1.obj (op V))), f.1.app (op V) s = G.1.map iVU.op t) :
    Function.Surjective (f.1.app (op U))

Proof state:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.val.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.val.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.val.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : ToType (F.val.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.val.map (iVU i).op)) s = sf i
⊢ (ConcreteCategory.hom (f.val.app (op U))) s = t

Tactic:
apply G.eq_of_locally_eq' V U iVU V_cover

Result:
case h.h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.val.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.val.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.val.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.val V sf
s : ToType (F.val.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.val.map (iVU i).op)) s = sf i
⊢ ∀ (i : ↥U),
    (ConcreteCategory.hom (G.val.map (iVU i).op)) ((ConcreteCategory.hom (f.val.app (op U))) s) =
      (ConcreteCategory.hom (G.val.map (iVU i).op)) t

Proof state:
case h.a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.val.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.val.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.val.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
z : ↑X
hz : z ∈ V x ⊓ V y
⊢ (ConcreteCategory.hom (G.val.map ((iVU x).op ≫ ((V x).infLELeft (V y)).op) ≫ germ G.val (V x ⊓ V y) z hz)) t =
    (ConcreteCategory.hom (G.val.map ((iVU y).op ≫ ((V x).infLERight (V y)).op) ≫ germ G.val (V x ⊓ V y) z hz)) t

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.val.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.val.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.val.map (iVU x).op)) t
V_cover : U ≤ iSup V
⊢ IsCompatible F.val V sf

Tactic:
intro x y

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.val.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.val.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.val.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
⊢ (ConcreteCategory.hom (F.val.map ((V x).infLELeft (V y)).op)) (sf x) =
    (ConcreteCategory.hom (F.val.map ((V x).infLERight (V y)).op)) (sf y)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.val.app (op U)))

Tactic:
intro t

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
hsurj :
  ∀ (t : CC (G.val.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t
t : CC (G.val.obj (op U))
⊢ ∃ a, (ConcreteCategory.hom (f.val.app (op U))) a = t