-- Mathlib/Topology/Sheaves/Sheafify.lean
theorem stalkToFiber_injective (x : X) : Function.Injective (F.stalkToFiber x)

Proof state:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Injective (F.stalkToFiber x)

Tactic:
apply TopCat.stalkToFiber_injective

Result:
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → F.stalk ↑y),
    (Sheafify.isLocallyGerm F).pred fU →
      ∀ (fV : (y : ↥V.obj) → F.stalk ↑y),
        (Sheafify.isLocallyGerm F).pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Proof state:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
⊢ ∀ (w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj),
    fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
      fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)

Tactic:
intro w

Result:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj
⊢ fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
    fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)

Proof state:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj
wU : (fun x_1 => fU (iU x_1)) ⟨↑w, ⋯⟩ = F.germ U' ↑⟨↑w, ⋯⟩ ⋯ gU
wV : (fun x_1 => fV (iV x_1)) ⟨↑w, ⋯⟩ = F.germ V' ↑⟨↑w, ⋯⟩ ⋯ gV
⊢ fU ((id (W.infLERight (U' ⊓ V') ≫ U'.infLELeft V' ≫ iU)) w) =
    fV ((id (W.infLERight (U' ⊓ V') ≫ U'.infLERight V' ≫ iV)) w)

Tactic:
refine wU.trans <| .trans ?_ wV.symm

Result:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj
wU : (fun x_1 => fU (iU x_1)) ⟨↑w, ⋯⟩ = F.germ U' ↑⟨↑w, ⋯⟩ ⋯ gU
wV : (fun x_1 => fV (iV x_1)) ⟨↑w, ⋯⟩ = F.germ V' ↑⟨↑w, ⋯⟩ ⋯ gV
⊢ F.germ U' ↑⟨↑w, ⋯⟩ ⋯ gU = F.germ V' ↑⟨↑w, ⋯⟩ ⋯ gV

Proof state:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
wVx : fV ⟨x, ⋯⟩ = F.germ V' x ⋯ gV
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Tactic:
clear wVx

Result:
case w.intro.intro.intro.intro.intro.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 => fU (iU x_2)) x_1 = F.germ U' ↑x_1 ⋯ gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
wV : ∀ (x_1 : ↥V'), (fun x_2 => fV (iV x_2)) x_1 = F.germ V' ↑x_1 ⋯ gV
⊢ ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)

Proof state:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥U.obj) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥V.obj) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ U.obj
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ V.obj
gV : F.obj (op V')
e : F.germ U' x ⋯ gU = F.germ V' x ⋯ gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : F.map iU'.op gU = F.map iV'.op gV
w : ↥{ obj := W ⊓ (U' ⊓ V'), property := ⋯ }.obj
wU : (fun x_1 => fU (iU x_1)) ⟨↑w, ⋯⟩ = F.germ U' ↑⟨↑w, ⋯⟩ ⋯ gU
wV : (fun x_1 => fV (iV x_1)) ⟨↑w, ⋯⟩ = F.germ V' ↑⟨↑w, ⋯⟩ ⋯ gV
⊢ F.germ U' ↑⟨↑w, ⋯⟩ ⋯ gU = F.germ V' ↑⟨↑w, ⋯⟩ ⋯ gV

Tactic:
rw [← F.germ_res iU' w w.2.1, ← F.germ_res iV' w w.2.1,
  CategoryTheory.types_comp_apply, CategoryTheory.types_comp_apply, e']

Result:
no goals