awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf.{w, v, u} C Y
𝒢 : Presheaf.{w, v, u} C X
H₂ : ℱ ⟶ obj (pushforward C H₁.hom) 𝒢
U : (Opens (↑X : Type w))ᵒᵖ
⊢ (pushforwardToOfIso H₁ H₂).app U = H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom ⋯)

Tactic:
simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]

Premises used: TopCat.Presheaf.pushforwardToOfIso, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
g : s.pt.left ⟶ (Cone.pt (asEmptyCone x)).left
w :
  autoParam ((Opens.map f).op.map (id (homOfLE ⋯).op) ≫ (Cone.pt (asEmptyCone x)).hom = s.pt.hom)
    CostructuredArrow.homMk._auto_1
⊢ s.pt ⟶ Cone.pt (asEmptyCone x)

Tactic:
fapply CostructuredArrow.homMk

Premises used: CategoryTheory.CostructuredArrow.homMk
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
g :
  op (unop s.pt.1) ⟶
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H : Opens (↑Y : Type v) }
⊢ s.pt.left ⟶ (Cone.pt (asEmptyCone x)).left

Tactic:
change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)

Premises used: TopologicalSpace.Opens.mk, Opposite.op, Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
g :
  {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
            (a : (↑X : Type v)) → (↑Y : Type v)) ''
          (↑U : Set (↑X : Type v)),
      is_open' := H : Opens (↑Y : Type v) } ≤
    unop s.pt.1
⊢ op (unop s.pt.1) ⟶
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H : Opens (↑Y : Type v) }

Tactic:
refine (homOfLE ?_).op

Premises used: Quiver.Hom.op, CategoryTheory.homOfLE
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
g :
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑(unop ((Opens.map f).op.obj s.pt.left)) : Set (↑X : Type v)) ⊆
    (↑(unop s.pt.1) : Set (↑Y : Type v))
⊢ {
      carrier :=
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
            (a : (↑X : Type v)) → (↑Y : Type v)) ''
          (↑U : Set (↑X : Type v)),
      is_open' := H : Opens (↑Y : Type v) } ≤
    unop s.pt.1

Tactic:
apply (Set.image_mono s.pt.hom.unop.le).trans

Premises used: Quiver.Hom.le, Set.image_mono, Quiver.Hom.unop, CategoryTheory.CostructuredArrow.hom, HasSubset.Subset.trans, CategoryTheory.Limits.Cone.pt
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑(unop ((Opens.map f).op.obj s.pt.left)) : Set (↑X : Type v)) ⊆
    (↑(unop s.pt.1) : Set (↑Y : Type v))

Tactic:
Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)

Premises used: Set.Mem, setOf, Set.image_preimage, CategoryTheory.Limits.Cone.pt, SetLike.coe, Set.preimage, GaloisConnection.l_u_le, CategoryTheory.CostructuredArrow.left, Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑(unop ((Opens.map f).op.obj s.pt.left)) : Set (↑X : Type v)) ⊆
    (↑(unop s.pt.1) : Set (↑Y : Type v))

Tactic:
exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)

Premises used: Set.image_preimage, CategoryTheory.Limits.Cone.pt, SetLike.coe, GaloisConnection.l_u_le, CategoryTheory.CostructuredArrow.left, Opposite.unop
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
s : Cone (C := CostructuredArrow (Opens.map f).op (op U)) (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ autoParam ((Opens.map f).op.map (id (homOfLE ⋯).op) ≫ (Cone.pt (asEmptyCone x)).hom = s.pt.hom)
    CostructuredArrow.homMk._auto_1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
have :
  (hx : IsTerminal x) →
    (obj (pullback C f) ℱ).obj (op U) ≅
      ℱ.obj
        (op
          {
            carrier :=
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                      f) :
                  (a : (↑X : Type v)) → (↑Y : Type v)) ''
                (↑U : Set (↑X : Type v)),
            is_open' := H })
⊢ (obj (pullback C f) ℱ).obj (op U) ≅
    ℱ.obj
      (op
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    f) :
                (a : (↑X : Type v)) → (↑Y : Type v)) ''
              (↑U : Set (↑X : Type v)),
          is_open' := H })

Tactic:
have hx : IsTerminal x :=
    { lift := fun s ↦ by
        fapply CostructuredArrow.homMk
        · change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_mono s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
        · simp [eq_iff_true_of_subsingleton] }
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
X_1 : TopCat
C : Type u
inst_1 : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_2 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_3 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
inst_4 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens (↑X : Type v)
H :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
x : CostructuredArrow (Opens.map f).op (op U) :=
  CostructuredArrow.mk (Y :=
    op
      {
        carrier :=
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
              (a : (↑X : Type v)) → (↑Y : Type v)) ''
            (↑U : Set (↑X : Type v)),
        is_open' := H })
    (Quiver.Hom.op (homOfLE ⋯))
hx : IsTerminal x
⊢ (obj (pullback C f) ℱ).obj (op U) ≅
    ℱ.obj
      (op
        {
          carrier :=
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    f) :
                (a : (↑X : Type v)) → (↑Y : Type v)) ''
              (↑U : Set (↑X : Type v)),
          is_open' := H })

Tactic:
exact IsColimit.coconePointUniqueUpToIso
    ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
    (colimitOfDiagramTerminal hx _)

Premises used: CategoryTheory.Functor.op, Opposite.op, TopologicalSpace.Opens.map, CategoryTheory.Limits.colimitOfDiagramTerminal, CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens (↑X : Type v)
HU :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
HV :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑V : Set (↑X : Type v)))
le : U ≤ V
dsimp :
  (obj (pullback C f) ℱ).map (homOfLE le).op ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
          (colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ :
              IsLimit (C := CostructuredArrow (Opens.map f).op (op U))
                (asEmptyCone
                  (CostructuredArrow.mk (Y :=
                    op
                      {
                        carrier :=
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
                                  (CC := carrier) f) :
                              (a : (↑X : Type v)) → (↑Y : Type v)) ''
                            (↑U : Set (↑X : Type v)),
                        is_open' := HU : Opens (↑Y : Type v) })
                    (homOfLE ⋯).op)) }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))) =
    Iso.hom
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
          (colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Cone (C := CostructuredArrow (Opens.map f).op (op V))
                      (empty (CostructuredArrow (Opens.map f).op (op V)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op
⊢ (obj (pullback C f) ℱ).map (homOfLE le).op ≫ Iso.hom (pullbackObjObjOfImageOpen f ℱ U HU) =
    Iso.hom (pullbackObjObjOfImageOpen f ℱ V HV) ≫ ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
dsimp [pullbackObjObjOfImageOpen]

Premises used: TopCat.Presheaf.pullbackObjObjOfImageOpen
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens (↑X : Type v)
HU :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
HV :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑V : Set (↑X : Type v)))
le : U ≤ V
⊢ (obj (pullback C f) ℱ).map (homOfLE le).op ≫
      Iso.hom
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
          (colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ :
              IsLimit (C := CostructuredArrow (Opens.map f).op (op U))
                (asEmptyCone
                  (CostructuredArrow.mk (Y :=
                    op
                      {
                        carrier :=
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
                                  (CC := carrier) f) :
                              (a : (↑X : Type v)) → (↑Y : Type v)) ''
                            (↑U : Set (↑X : Type v)),
                        is_open' := HU : Opens (↑Y : Type v) })
                    (homOfLE ⋯).op)) }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))) =
    Iso.hom
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
          (colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Cone (C := CostructuredArrow (Opens.map f).op (op V))
                      (empty (CostructuredArrow (Opens.map f).op (op V)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V)).hom_ext
    (fun j ↦ ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.IsColimit.hom_ext, Opposite.op, TopologicalSpace.Opens.map, CategoryTheory.Functor.isPointwiseLeftKanExtensionLeftKanExtensionUnit
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens (↑X : Type v)
HU :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑U : Set (↑X : Type v)))
HV :
  IsOpen (X := (↑Y : Type v))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v)) ''
      (↑V : Set (↑X : Type v)))
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
⊢ Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ) j ⟶ (obj (pullback C f) ℱ).obj (op U))
    (NatTrans.app
          (Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)))
          j ≫
        (obj (pullback C f) ℱ).map (homOfLE le).op :
      obj (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ) j ⟶ (obj (pullback C f) ℱ).obj (op U))
    (NatTrans.app
        (Cocone.ι
          ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)))
        (obj (CostructuredArrow.map (homOfLE le).op) j) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) (obj (CostructuredArrow.map (homOfLE le).op) j) ⟶
        obj
          (obj (Functor.const (CostructuredArrow (Opens.map f).op (op U)))
            (Cocone.pt (J := CostructuredArrow (Opens.map f).op (op U))
              ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
                    ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
                (op U))))
          (obj (CostructuredArrow.map (homOfLE le).op) j))

Tactic:
have eq : ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op V)).ι.app j ≫ ((pullback C f).obj ℱ).map (homOfLE le).op =
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op U)).ι.app ((CostructuredArrow.map (homOfLE le).op).obj j) := by cat_disch