-- Mathlib/Topology/Sheaves/Stalks.lean
@[ext]
lemma pullback_obj_obj_ext {Z : C} {f : X ⟶ Y} {F : Y.Presheaf C} (U : (Opens X)ᵒᵖ)
    {φ ψ : ((pullback C f).obj F).obj U ⟶ Z}
    (h : ∀ (V : Opens Y) (hV : U.unop ≤ (Opens.map f).obj V),
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
        ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
        ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ) : φ = ψ

Proof state:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ φ = ψ

Tactic:
apply ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F _).hom_ext

Result:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ ∀ (j : CostructuredArrow (Opens.map f).op (op U)),
    ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                (op U)).ι.app
          j ≫
        φ =
      ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F)
                    ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                (op U)).ι.app
          j ≫
        ψ

Proof state:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ ∀ (j : CostructuredArrow (Opens.map f).op (op U)),
    ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                (op U)).ι.app
          j ≫
        φ =
      ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F)
                    ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                (op U)).ι.app
          j ≫
        ψ

Tactic:
rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩

Result:
case op.mk.op.mk.op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
V : Opens ↑Y
as✝ : PUnit.{1}
b : unop ((Functor.fromPUnit (op U)).obj { as := as✝ }) ⟶ unop ((Opens.map f).op.obj (op V))
⊢ ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
              (op U)).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      φ =
    ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
              (op U)).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      ψ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : (Opens ↑X)ᵒᵖ
φ ψ : ((pullback C f).obj F).obj U ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop U ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ φ = ψ

Tactic:
obtain ⟨U⟩ := U

Result:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ φ = ψ

Proof state:
case op.mk.op.mk.op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
φ ψ : ((pullback C f).obj F).obj (op U) ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop (op U) ≤ (Opens.map f).obj V),
    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
V : Opens ↑Y
as✝ : PUnit.{1}
b : unop ((Functor.fromPUnit (op U)).obj { as := as✝ }) ⟶ unop ((Opens.map f).op.obj (op V))
⊢ ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
              (op U)).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      φ =
    ((Functor.LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
              (op U)).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      ψ

Tactic:
simpa [pushforwardPullbackAdjunction, Functor.lanAdjunction_unit]
  using h V (leOfHom b)

Result:
no goals