-- Mathlib/Topology/Sheaves/Stalks.lean
theorem app_surjective_of_stalkFunctor_map_bijective {F G : Sheaf C X} (f : F ⟶ G) (U : Opens X)
    (h : ∀ x ∈ U, Function.Bijective ((stalkFunctor C x).map f.1)) :
    Function.Surjective (f.1.app (op U))

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
V₂ : Opens ↑X
hxV₂ : x ∈ V₂
iV₂V₁ : V₂ ⟶ V₁
iV₂U : V₂ ⟶ U
heq :
  (ConcreteCategory.hom (G.presheaf.map iV₂V₁.op)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.map iV₂U.op)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t

Tactic:
use V₂, hxV₂, iV₂U, F.1.map iV₂V₁.op s₁

Result:
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
V₂ : Opens ↑X
hxV₂ : x ∈ V₂
iV₂V₁ : V₂ ⟶ V₁
iV₂U : V₂ ⟶ U
heq :
  (ConcreteCategory.hom (G.presheaf.map iV₂V₁.op)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.map iV₂U.op)) t
⊢ (ConcreteCategory.hom (f.val.app (op V₂))) ((ConcreteCategory.hom (F.val.map iV₂V₁.op)) s₁) =
    (ConcreteCategory.hom (G.val.map iV₂U.op)) t

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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
V₂ : Opens ↑X
hxV₂ : x ∈ V₂
iV₂V₁ : V₂ ⟶ V₁
iV₂U : V₂ ⟶ U
heq :
  (ConcreteCategory.hom (G.presheaf.map iV₂V₁.op)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.map iV₂U.op)) t
⊢ (ConcreteCategory.hom (f.val.app (op V₂))) ((ConcreteCategory.hom (F.val.map iV₂V₁.op)) s₁) =
    (ConcreteCategory.hom (G.val.map iV₂U.op)) t

Tactic:
rw [← ConcreteCategory.comp_apply, f.1.naturality, ConcreteCategory.comp_apply, heq]

Result:
no goals

Proof state:
case intro.intro.intro.intro
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom ((stalkFunctor C x).map f.val)) ((ConcreteCategory.hom (F.presheaf.germ V₁ x hxV₁)) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t

Tactic:
rw [stalkFunctor_map_germ_apply V₁ x hxV₁ f.1 s₁] at hs₁

Result:
case intro.intro.intro.intro
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t

Proof state:
case intro.intro.intro.intro
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t

Tactic:
obtain ⟨V₂, hxV₂, iV₂V₁, iV₂U, heq⟩ := G.presheaf.germ_eq x hxV₁ hx _ _ hs₁

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
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
h : ∀ x ∈ U, Function.Bijective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.val))
t : CC (G.val.obj (op U))
x : ↑X
hx : x ∈ U
V₁ : Opens ↑X
hxV₁ : x ∈ V₁
s₁ : ToType (F.presheaf.obj (op V₁))
hs₁ :
  (ConcreteCategory.hom (germ G.val V₁ x hxV₁)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.germ U x hx)) t
V₂ : Opens ↑X
hxV₂ : x ∈ V₂
iV₂V₁ : V₂ ⟶ V₁
iV₂U : V₂ ⟶ U
heq :
  (ConcreteCategory.hom (G.presheaf.map iV₂V₁.op)) ((ConcreteCategory.hom (f.val.app (op V₁))) s₁) =
    (ConcreteCategory.hom (G.presheaf.map iV₂U.op)) t
⊢ ∃ V, ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.val.app (op V))) s = (ConcreteCategory.hom (G.val.map iVU.op)) t