Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tV : (subpresheafToTypes P.toPrelocalPredicate).stalk x
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T ↑x_1
hU : P.pred fU
h :
  (ConcreteCategory.hom (stalkToFiber P x))
      ((ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩) =
    (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                U))
            ⟨fU, hU⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        tV = (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩

Tactic:
obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), 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 :
  (ConcreteCategory.hom (stalkToFiber P x))
      ((ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            U))
        ⟨fU, hU⟩) =
    (ConcreteCategory.hom (stalkToFiber P x))
      ((ConcreteCategory.hom
          (colimit.ι
            (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
              (subpresheafToTypes P.toPrelocalPredicate))
            V))
        ⟨fV, hV⟩)
⊢ ∃ W s,
    ∃ (hW : P.pred s),
      (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                U))
            ⟨fU, hU⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩ ∧
        (ConcreteCategory.hom
              (colimit.ι
                (((Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ (Type u_1)).obj (OpenNhds.inclusion x).op).obj
                  (subpresheafToTypes P.toPrelocalPredicate))
                V))
            ⟨fV, hV⟩ =
          (ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ (↑(unop W)) x ⋯)) ⟨s, hW⟩