-- Mathlib/Topology/Sheaves/LocalPredicate.lean
theorem stalkToFiber_injective (P : LocalPredicate T) (x : X)
    (w :
      ∀ (U V : OpenNhds x) (fU : ∀ y : U.1, T y) (_ : P.pred fU) (fV : ∀ y : V.1, T y)
        (_ : P.pred fV) (_ : fU ⟨x, U.2⟩ = fV ⟨x, V.2⟩),
        ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V), ∀ w : W.1,
          fU (iU w : U.1) = fV (iV w : V.1)) :
    Function.Injective (stalkToFiber P x) := fun tU tV h => by
  -- We promise to provide all the ingredients of the proof later:
  let Q :
    ∃ (W : (OpenNhds x)ᵒᵖ) (s : ∀ w : (unop W).1, T w) (hW : P.pred s),
      tU = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ ∧
        tV = (subsheafToTypes P).presheaf.germ _ x (unop W).2 ⟨s, hW⟩ :=
    ?_
  · choose W s hW e using Q
    exact e.1.trans e.2.symm
  -- Then use induction to pick particular representatives of `tU tV : stalk x`
  obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective'.{v, v} tU
  obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective'.{v, v} tV
  -- Decompose everything into its constituent parts:
  dsimp
  simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h
  specialize w (unop U) (unop V) fU hU fV hV h
  rcases w with ⟨W, iU, iV, w⟩
  -- and put it back together again in the correct order.
  refine ⟨op W, fun w => fU (iU w : (unop U).1), P.res ?_ _ hU, ?_⟩
  · rcases W with ⟨W, m⟩
    exact iU
  · exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩

Proof state:
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine_1.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
W : Opens ↑X
m : x ∈ W
iU : { obj := W, property := m } ⟶ unop U
iV : { obj := W, property := m } ⟶ unop V
w : ∀ (w : ↥{ obj := W, property := m }.obj), fU (iU w) = fV (iV w)
⊢ (unop (op { obj := W, property := m })).obj ⟶ (unop U).obj

Tactic:
exact iU

Result:
no goals

Proof state:
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h :
  stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (subsheafToTypes P).presheaf)
        U ⟨fU, hU⟩) =
    stalkToFiber P x
      (colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type v)).obj (OpenNhds.inclusion x).op).obj
          (subsheafToTypes P).presheaf)
        V ⟨fV, hV⟩)
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩ ∧
        colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩

Tactic:
simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h

Result:
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩ ∧
        colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩

Proof state:
case refine_1.intro.intro.mk.intro.intro.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
w : ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩ ∧
        colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩

Tactic:
rcases w with ⟨W, iU, iV, w⟩

Result:
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) U ⟨fU, hU⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩ ∧
        colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate) V ⟨fV, hV⟩ =
          (subpresheafToTypes P.toPrelocalPredicate).germ (unop W).obj x ⋯ ⟨s, hW⟩

Proof state:
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w : ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
⊢ (unop (op W)).obj ⟶ (unop U).obj

Tactic:
rcases W with ⟨W, m⟩

Result:
case refine_1.intro.intro.mk.intro.intro.mk.intro.intro.intro.refine_1.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T ↑x_1
hV : P.pred fV
h : fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩
W : Opens ↑X
m : x ∈ W
iU : { obj := W, property := m } ⟶ unop U
iV : { obj := W, property := m } ⟶ unop V
w : ∀ (w : ↥{ obj := W, property := m }.obj), fU (iU w) = fV (iV w)
⊢ (unop (op { obj := W, property := m })).obj ⟶ (unop U).obj

Proof state:
case refine_2
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥U.obj) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥V.obj) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥W.obj), fU (iU w) = fV (iV w)
tU tV : (subsheafToTypes P).presheaf.stalk x
h : stalkToFiber P x tU = stalkToFiber P x tV
W : (OpenNhds x)ᵒᵖ
s : (w : ↥(unop W).obj) → T ↑w
hW : P.pred s
e :
  tU = (subsheafToTypes P).presheaf.germ (unop W).obj x ⋯ ⟨s, hW⟩ ∧
    tV = (subsheafToTypes P).presheaf.germ (unop W).obj x ⋯ ⟨s, hW⟩
⊢ tU = tV

Tactic:
exact e.1.trans e.2.symm

Result:
no goals