awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
w :
  ∀ (U : Opens (↑X : Type v)),
    Eq (α := (obj (pullback C f) ℱ).obj (op U) ⟶ (hf.functor.op ⋙ 𝒢).obj (op U))
      (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u ≫ Iso.hom (hf.pullbackObjIso 𝒢)) (op U))
      (NatTrans.app (Iso.hom (hf.pullbackObjIso ℱ) ≫ hf.functor.op.whiskerLeft u) (op U))
⊢ Eq (α := obj (pullback C f) ℱ ⟶ hf.functor.op ⋙ 𝒢)
    (CategoryTheory.Functor.map (pullback C f) u ≫ Iso.hom (hf.pullbackObjIso 𝒢))
    (Iso.hom (hf.pullbackObjIso ℱ) ≫ hf.functor.op.whiskerLeft u)

Tactic:
ext U
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
w :
  Eq (α := (obj (pullback C f) ℱ).obj (op U) ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U) ≫
      Iso.hom
        (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
          (Limits.colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))))
    (CategoryStruct.comp (Y := ℱ.obj (op (hf.functor.obj U)))
      (Iso.hom
          (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (Limits.colimitOfDiagramTerminal
              {
                lift :=
                  fun
                    (s :
                      Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                        (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))) :
        (obj (pullback C f) ℱ).obj (op U) ⟶ ℱ.obj (op (hf.functor.obj U)))
      (u.app (op (hf.functor.obj U)) : ℱ.obj (op (hf.functor.obj U)) ⟶ 𝒢.obj (op (hf.functor.obj U))))
⊢ Eq (α := (obj (pullback C f) ℱ).obj (op U) ⟶ (hf.functor.op ⋙ 𝒢).obj (op U))
    (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u ≫ Iso.hom (hf.pullbackObjIso 𝒢)) (op U))
    (NatTrans.app (Iso.hom (hf.pullbackObjIso ℱ) ≫ hf.functor.op.whiskerLeft u) (op U))

Tactic:
dsimp [pullbackObjIso, pullbackObjObjOfImageOpen]

Premises used: IsOpenMap.pullbackObjIso, TopCat.Presheaf.pullbackObjObjOfImageOpen
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
⊢ Eq (α := (obj (pullback C f) ℱ).obj (op U) ⟶ 𝒢.obj (op (hf.functor.obj U)))
    (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U) ≫
      Iso.hom
        (Limits.IsColimit.coconePointUniqueUpToIso
          ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
          (Limits.colimitOfDiagramTerminal
            {
              lift :=
                fun
                  (s :
                    Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                      (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
              fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))))
    (CategoryStruct.comp (Y := ℱ.obj (op (hf.functor.obj U)))
      (Iso.hom
          (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (Limits.colimitOfDiagramTerminal
              {
                lift :=
                  fun
                    (s :
                      Limits.Cone (C := CostructuredArrow (Opens.map f).op (op U))
                        (empty (CostructuredArrow (Opens.map f).op (op U)))) ↦
                  CostructuredArrow.homMk (homOfLE ⋯).op ⋯,
                fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))) :
        (obj (pullback C f) ℱ).obj (op U) ⟶ ℱ.obj (op (hf.functor.obj U)))
      (u.app (op (hf.functor.obj U)) : ℱ.obj (op (hf.functor.obj U)) ⟶ 𝒢.obj (op (hf.functor.obj U))))

Tactic:
((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U)).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 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
dsimp :
  (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op U) =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
⊢ Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)
        (NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)))
          j)
        (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U)) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)))
          j :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)

Tactic:
dsimp [pullback]

Premises used: TopCat.Presheaf.pullback
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
simp :
  NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
⊢ (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫ ((Opens.map f).op.leftKanExtension ℱ).map j.hom) ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op U) =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
simp only [Category.assoc, NatTrans.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
⊢ Eq (α :=
    (obj (𝟭 (CategoryTheory.Functor.{v, v, v, u} (Opens (↑Y : Type v))ᵒᵖ C)) ℱ).obj j.left ⟶
      (obj
            ((Opens.map f).op.lan ⋙
              obj (whiskeringLeft (Opens (↑Y : Type v))ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (Opens.map f).op)
            𝒢).obj
        j.left)
    (NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (CategoryTheory.Functor.{v, v, v, u} (Opens (↑Y : Type v))ᵒᵖ C)) u ≫
        NatTrans.app (Opens.map f).op.lanUnit 𝒢)
      j.left)
    (NatTrans.app
      (NatTrans.app (Opens.map f).op.lanUnit ℱ ≫
        CategoryTheory.Functor.map
          ((Opens.map f).op.lan ⋙
            obj (whiskeringLeft (Opens (↑Y : Type v))ᵒᵖ (Opens (↑X : Type v))ᵒᵖ C) (Opens.map f).op)
          u)
      j.left)

Tactic:
have := NatTrans.congr_app ((Opens.map f).op.lanUnit.naturality u) j.left
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
this :
  Eq (α := ℱ.obj j.left ⟶ (obj (Opens.map f).op.lan 𝒢).obj (op ((Opens.map f).obj (unop j.left))))
    (u.app j.left ≫ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left)
    (CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
      (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
      (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left)))))
rw :
  NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
      (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
      (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        ((Opens.map f).op.leftKanExtension 𝒢).map j.hom)
⊢ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    u.app j.left ≫
      NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
rw [reassoc_of% this]
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
this :
  Eq (α := ℱ.obj j.left ⟶ (obj (Opens.map f).op.lan 𝒢).obj (op ((Opens.map f).obj (unop j.left))))
    (u.app j.left ≫ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit 𝒢) j.left)
    (CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
      (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
      (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left)))))
⊢ NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left ≫
      NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        (obj (Opens.map f).op.lan 𝒢).map j.hom =
    CategoryStruct.comp (Y := (obj (Opens.map f).op.lan ℱ).obj (op ((Opens.map f).obj (unop j.left))))
      (NatTrans.app ((Opens.map f).op.leftKanExtensionUnit ℱ) j.left)
      (NatTrans.app (CategoryTheory.Functor.map (Opens.map f).op.lan u) (op ((Opens.map f).obj (unop j.left))) ≫
        ((Opens.map f).op.leftKanExtension 𝒢).map j.hom)

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Limits.HasColimits.{v, u} C
X Y : TopCat
f : X ⟶ Y
hf :
  IsOpenMap (X := (↑X : Type v)) (Y := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens (↑X : Type v)
j : CostructuredArrow (Opens.map f).op (op U)
⊢ Eq (α := obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)
        (NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)))
          j)
        (NatTrans.app (CategoryTheory.Functor.map (pullback C f) u) (op U)) :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶ (obj (pullback C f) 𝒢).obj (op U))
    (NatTrans.app (whiskerLeft (CostructuredArrow.proj (Opens.map f).op (op U)) u) j ≫
        NatTrans.app
          (Limits.Cocone.ι
            ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)))
          j :
      obj (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ) j ⟶
        obj
          (obj (const (CostructuredArrow (Opens.map f).op (op U)))
            (Limits.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))))
          j)

Tactic:
have eq : ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt (op U)).ι.app j
      ≫ ((pullback C f).map u).app (op U) = NatTrans.app (Functor.whiskerLeft _ u) j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢)
      ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt (op U)).ι.app j := by
    dsimp [pullback]
    simp only [Category.assoc, NatTrans.naturality]
    have := NatTrans.congr_app ((Opens.map f).op.lanUnit.naturality u) j.left
    dsimp [lanUnit] at this
    rw [reassoc_of% this]
    rfl
-- Module: Mathlib.Topology.Sheaves.PresheafOfFunctions
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
U : (Opens (↑X : Type u_2))ᵒᵖ
⊢ (X.presheafToTypes T).obj U = ((x : ↥(unop U)) → T (↑x : (↑X : Type u_2)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.PresheafOfFunctions
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
U V : (Opens (↑X : Type u_2))ᵒᵖ
i : U ⟶ V
f : (fun (X : Type (max u_1 u_2)) ↦ X) ((X.presheafToTypes T).obj U)
⊢ Eq (α := (x : ↥(unop V)) → T (↑x : (↑X : Type u_2)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X.presheafToTypes T).map i) :
          (a : (x : ↥(unop U)) → T (↑x : (↑X : Type u_2))) → (x : ↥(unop V)) → T (↑x : (↑X : Type u_2)))
        f :
      (x : ↥(unop V)) → T (↑x : (↑X : Type u_2)))
    fun (x : ↥(unop V)) ↦
    (f ((i.unop : (a : ↥(unop V)) → ↥(unop U)) x) : T (↑((i.unop : (a : ↥(unop V)) → ↥(unop U)) x) : (↑X : Type u_2)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.PresheafOfFunctions
Goal:
X : TopCat
T : Type u_1
U : (Opens (↑X : Type u_2))ᵒᵖ
⊢ (X.presheafToType T).obj U = (↥(unop U) → T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.PresheafOfFunctions
Goal:
X : TopCat
T : Type u_1
U V : (Opens (↑X : Type u_2))ᵒᵖ
i : U ⟶ V
f : (fun (X : Type (max u_1 u_2)) ↦ X) ((X.presheafToType T).obj U)
⊢ Eq (α := ↥(unop V) → T)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((X.presheafToType T).map i) : (a : ↥(unop U) → T) → ↥(unop V) → T) f :
      ↥(unop V) → T)
    (f ∘ (⇑i.unop : (a : ↥(unop V)) → ↥(unop U)) : ↥(unop V) → T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.PresheafOfFunctions
Goal:
X T : TopCat
U : (Opens (↑X : Type u_1))ᵒᵖ
⊢ (X.presheafToTop T).obj U = ((Opens.toTopCat X).obj (unop U) ⟶ T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
F : Presheaf (Discrete Unit) X
x_1 : Discrete Unit
U : Opens (↑X : Type w)
S : Sieve U
h : S ∈ (Opens.grothendieckTopology (↑X : Type w) : (a : Opens (↑X : Type w)) → Set (Sieve a)) U
x : Presieve.FamilyOfElements (F ⋙ Functor.obj coyoneda (op x_1)) S.arrows
h_1 : x.Compatible (R := S.arrows)
x_2 : (F ⋙ Functor.obj coyoneda (op x_1)).obj (op U)
cat_disch cat_disch₁ :
  (fun (t : (F ⋙ Functor.obj coyoneda (op x_1)).obj (op U)) ↦ x.IsAmalgamation (R := S.arrows) t) x_2 → x_2 = eqToHom ⋯
cat_disch₂ cat_disch₃ : x.IsAmalgamation (R := S.arrows) x_2 → x_2 = eqToHom ⋯
⊢ (fun (t : (F ⋙ Functor.obj coyoneda (op x_1)).obj (op U)) ↦ x.IsAmalgamation (R := S.arrows) t) x_2 → x_2 = eqToHom ⋯

Tactic:
cat_disch
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
F G : Presheaf.{w, v, u} C X
α : F ≅ G
⊢ F.IsSheaf ↔ G.IsSheaf

Tactic:
Presheaf.isSheaf_of_iso_iff α

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, TopCat.Presheaf.IsSheaf
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
F G : Presheaf.{w, v, u} C X
α : F ≅ G
h : F.IsSheaf
⊢ G.IsSheaf

Tactic:
(isSheaf_iso_iff α).1 h

Premises used: Iff.mp, TopCat.Presheaf.isSheaf_iso_iff
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
F : Sheaf.{w, v, u} C X
t : (Opens (↑X : Type w))ᵒᵖ
⊢ (InducedCategory.Hom.hom (𝟙 F)).app t =
    𝟙 (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj t)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
F G H : Sheaf.{w, v, u} C X
f : F ⟶ G
g : G ⟶ H
t : (Opens (↑X : Type w))ᵒᵖ
⊢ (f ≫ g).hom.app t = f.hom.app t ≫ g.hom.app t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
⊢ Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))

Tactic:
have := (isSheaf_iff_isSheaf_of_type _ _).mp
    ((Presheaf.isSheaf_iff_isSheaf_forget (C := Opens X) (A' := A) _ F (forget _)).mp hF)
-- Module: Mathlib.Topology.Sheaves.Sheaf
Goal:
X : TopCat
A : Type u_1
inst : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u + 1, u + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory A FC (CC := CC)
inst_3 : HasLimits.{u, u_1} A
inst_4 : PreservesLimits (forget A (FC := FC) (CC := CC))
inst_5 : Functor.ReflectsIsomorphisms (forget A (FC := FC) (CC := CC))
F : Presheaf A X
hF : F.IsSheaf
U : (Opens (↑X : Type u))ᵒᵖ
s t : ToType (FC := FC) (CC := CC) (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ (V : Opens (↑X : Type u)) (hV : V ≤ unop U),
      x ∈ V ∧
        Eq (α := CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              s :
            CC (F.obj (op V)))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE hV).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op V)))
              t :
            CC (F.obj (op V)))
this : Presieve.IsSheaf (Opens.grothendieckTopology (↑X : Type u)) (F ⋙ forget A (FC := FC) (CC := CC))
choose :
  ∀ (V : (x : ↥(unop U)) → Opens (↑X : Type u)) (hV : ∀ (x : ↥(unop U)), V x ≤ unop U)
    (hxV : ∀ (x : ↥(unop U)), (↑x : (↑X : Type u)) ∈ V x)
    (H :
      ∀ (x : ↥(unop U)),
        Eq (α := CC (F.obj (op (V x))))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
              s :
            CC (F.obj (op (V x))))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) :
                (a : CC (F.obj (op (unop U)))) → CC (F.obj (op (V x))))
              t :
            CC (F.obj (op (V x))))),
    s = t
⊢ s = t

Tactic:
choose V hV hxV H using fun x : U.unop ↦ hst x.1 x.2

Premises used: Subtype.val, Subtype.property