awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
R : Sieve U
hR : R ∈ (grothendieckTopology X : (a : Opens X) → Set (Sieve a)) U
hU : x ∈ U
V : Opens X
f : V ⟶ U
hf : R.arrows f
hV : x ∈ V
⊢ ∃ (Y : Opens X) (f : Y ⟶ U) (_ : R.arrows f) (y :
    Functor.obj
      { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
        map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
          ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
        map_id := ⋯, map_comp := ⋯ }
      Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              { obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                  ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦
                    { down := { down := ⋯ : PLift (x ∈ Y) } : ULift.{u, 0} (PLift (x ∈ Y)) },
                map_id := ⋯, map_comp := ⋯ : Opens X ⥤ Type u }
              f) :
          (a :
              (fun (X : Type u) ↦ X)
                ({ obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                      map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                        ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
                      map_id := ⋯, map_comp := ⋯ }.obj
                  Y)) →
            (fun (X : Type u) ↦ X)
              ({ obj := fun (U : Opens X) ↦ ULift.{u, 0} (PLift (x ∈ U)),
                    map := fun {X_1 Y : Opens X} (f : X_1 ⟶ Y) ↦
                      ↾fun (h : ULift.{u, 0} (PLift (x ∈ X_1))) ↦ { down := { down := ⋯ } },
                    map_id := ⋯, map_comp := ⋯ }.obj
                U))
        y =
      { down := { down := hU : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) }

Tactic:
exact ⟨_, _, hf, ⟨⟨hV⟩⟩, rfl⟩
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
S : Sieve U
hS :
  ∀
    (Φ :
      ObjectProperty.FullSubcategory (C := Point (C := Opens X) (grothendieckTopology X))
        (pointsGrothendieckTopology X))
    (x : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj U),
    ∃ (Y : Opens X) (g : Y ⟶ U) (_ : S.arrows g) (y : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsGrothendieckTopology X).fiber.map g) :
            (a : (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj U))
          y =
        x
x : X
hx : x ∈ U
obtain :
  ∀ (V : Opens X) (f : V ⟶ U) (hf : S.arrows f) (hV : x ∈ V),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map
                (Point.fiber
                  (ObjectProperty.FullSubcategory.obj (P := pointsGrothendieckTopology X)
                    (ObjectProperty.FullSubcategory.mk (P := pointsGrothendieckTopology X) (pointGrothendieckTopology x)
                      ⋯)))
                f) :
            (a : (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj V)) →
              (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj U))
          { down := { down := hV } } =
        { down := { down := hx : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) } →
      ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨V, f, hf, ⟨⟨hV⟩⟩, _⟩ := hS ⟨_, ⟨x⟩⟩ ⟨⟨hx⟩⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.ObjectProperty.ofObj.mk, PLift.up, ULift.up
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
S : Sieve U
hS :
  ∀
    (Φ :
      ObjectProperty.FullSubcategory (C := Point (C := Opens X) (grothendieckTopology X))
        (pointsGrothendieckTopology X))
    (x : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj U),
    ∃ (Y : Opens X) (g : Y ⟶ U) (_ : S.arrows g) (y : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsGrothendieckTopology X).fiber.map g) :
            (a : (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj U))
          y =
        x
x : X
hx : x ∈ U
V : Opens X
f : V ⟶ U
hf : S.arrows f
hV : x ∈ V
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (Point.fiber
              (ObjectProperty.FullSubcategory.obj (P := pointsGrothendieckTopology X)
                (ObjectProperty.FullSubcategory.mk (P := pointsGrothendieckTopology X) (pointGrothendieckTopology x)
                  ⋯)))
            f) :
        (a : (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj V)) →
          (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj U))
      { down := { down := hV } } =
    { down := { down := hx : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) }
⊢ ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1

Tactic:
⟨V, f, hf, hV⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
U : Opens X
S : Sieve U
hS :
  ∀
    (Φ :
      ObjectProperty.FullSubcategory (C := Point (C := Opens X) (grothendieckTopology X))
        (pointsGrothendieckTopology X))
    (x : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj U),
    ∃ (Y : Opens X) (g : Y ⟶ U) (_ : S.arrows g) (y : Φ.obj (P := pointsGrothendieckTopology X).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsGrothendieckTopology X).fiber.map g) :
            (a : (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type u) ↦ X) (Φ.obj.fiber.obj U))
          y =
        x
x : X
hx : x ∈ U
V : Opens X
f : V ⟶ U
hf : S.arrows f
hV : x ∈ V
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (Point.fiber
              (ObjectProperty.FullSubcategory.obj (P := pointsGrothendieckTopology X)
                (ObjectProperty.FullSubcategory.mk (P := pointsGrothendieckTopology X) (pointGrothendieckTopology x)
                  ⋯)))
            f) :
        (a : (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj V)) →
          (fun (X : Type u) ↦ X) ({ obj := pointGrothendieckTopology x, property := ⋯ }.obj.fiber.obj U))
      { down := { down := hV } } =
    { down := { down := hx : PLift (x ∈ U) } : ULift.{u, 0} (PLift (x ∈ U)) }
⊢ ∃ (U_1 : Opens X) (f : U_1 ⟶ U), S.arrows f ∧ x ∈ U_1

Tactic:
exact ⟨V, f, hf, hV⟩
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
U : Opens X
Φ : Point (C := Opens X) (grothendieckTopology X)
⊢ Subsingleton.{u + 1} (Φ.fiber.obj U)

Tactic:
Φ.subsingleton_fiber_obj (homOfLE le_top) Limits.isTerminalTop

Premises used: CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj, le_top, CategoryTheory.homOfLE, CategoryTheory.Limits.isTerminalTop
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 x_2 : Point (C := Opens X) (grothendieckTopology X)
x_3 x_4 : x_1 ⟶ x_2
h :
  ∀ (x : Opens X) (x_5 : x_2.fiber.obj x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_3.hom.app x)).toFun x_5 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (x_4.hom.app x)).toFun x_5
⊢ x_3 = x_4

Tactic:
ext
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 x_2 : Point (C := Opens X) (grothendieckTopology X)
x_3 x_4 : x_1 ⟶ x_2
x_5 : Opens X
x_6 : x_2.fiber.obj x_5
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (x_3.hom.app x_5)).toFun x_6 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_4.hom.app x_5)).toFun x_6

Tactic:
subsingleton
-- Module: Mathlib.Topology.Sheaves.Points
Goal:
X : Type u
inst : TopologicalSpace X
x_1 x y : X
x_2 :
  Quiver.Hom (V := Point (C := Opens X) (grothendieckTopology X)) (pointGrothendieckTopology x)
    (pointGrothendieckTopology y)
⊢ (fun (s : x ⤳ y) ↦
        {
          hom :=
            {
              app := fun (U : Opens X) ↦
                ↾fun (hU : Functor.obj (Point.fiber (pointGrothendieckTopology y)) U) ↦ { down := { down := ⋯ } },
              naturality := ⋯ } :
          Point.Hom (C := Opens X) (pointGrothendieckTopology x) (pointGrothendieckTopology y) })
      ⋯ =
    x_2

Tactic:
subsingleton
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
U : (Opens (↑X : Type w))ᵒᵖ
P Q R : Presheaf.{w, v, u} C X
f : P ⟶ Q
g : Q ⟶ R
⊢ (f ≫ g).app U = f.app U ≫ g.app U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
app : f.app = g.app
⊢ f = g

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
app : ∀ (U : (Opens (↑X : Type w))ᵒᵖ), f.app U = g.app U
⊢ f.app = g.app

Tactic:
ext U
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
U : Opens (↑X : Type w)
⊢ Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))

Tactic:
?_
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
U : (Opens (↑X : Type w))ᵒᵖ
app : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
⊢ f.app U = g.app U

Tactic:
induction U with | _ U => ?_
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
P Q : Presheaf.{w, v, u} C X
f g : P ⟶ Q
w : ∀ (U : Opens (↑X : Type w)), Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))
U : Opens (↑X : Type w)
⊢ Eq (α := P.obj (op U) ⟶ Q.obj (op U)) (f.app (op U)) (g.app (op U))

Tactic:
apply w
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : Type u_1
inst_1 : CompleteLattice X
v : ℕ → X
w x y z : X
e : v 0 = v 1
h : v 1 = v 2
h₀ : v 1 ≤ x
h_1 : x ≤ z ⊓ w
h₂ : x ≤ y ⊓ z
⊢ v 0 ≤ y

Tactic:
restrict_tac
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U V W : Opens (↑X : Type w)
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op W))
delta :
  Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₁).op) : (a : CC (F.obj (op V))) → CC (F.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₂).op) :
              (a : CC (F.obj (op W))) → CC (F.obj (op V)))
            x :
          CC (F.obj (op V))) :
      CC (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))
⊢ restrictOpen (FC := FC) (CC := CC) (restrictOpen (FC := FC) (CC := CC) x V e₂) U e₁ =
    restrictOpen (FC := FC) (CC := CC) x U ⋯

Tactic:
delta restrictOpen restrict

Premises used: TopCat.Presheaf.restrict, TopCat.Presheaf.restrictOpen
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U V W : Opens (↑X : Type w)
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op W))
rw :
  Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op)) :
          (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))
⊢ Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₁).op) : (a : CC (F.obj (op V))) → CC (F.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE e₂).op) :
              (a : CC (F.obj (op W))) → CC (F.obj (op V)))
            x :
          CC (F.obj (op V))) :
      CC (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))

Tactic:
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U V W : Opens (↑X : Type w)
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op W))
⊢ Eq (α := ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op)) :
          (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE ⋯).op) : (a : CC (F.obj (op W))) → CC (F.obj (op U)))
        x :
      CC (F.obj (op U)))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf.{w, v, u} C X
e : F ⟶ G
U V : Opens (↑X : Type w)
h : U ≤ V
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op V))
delta :
  Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE h).op) :
              (a : CC (F.obj (op V))) → CC (F.obj (op U)))
            x :
          CC (F.obj (op U))) :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))
⊢ Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
        (restrictOpen (FC := FC) (CC := CC) x U h) :
      CC (G.obj (op U)))
    (restrictOpen (FC := FC) (CC := CC)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x) U
        h :
      ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (G.obj (op U)))

Tactic:
delta restrictOpen restrict

Premises used: TopCat.Presheaf.restrict, TopCat.Presheaf.restrictOpen
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F G : Presheaf.{w, v, u} C X
e : F ⟶ G
U V : Opens (↑X : Type w)
h : U ≤ V
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op V))
rw :
  Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE h).op ≫ e.app (op U)) :
          (a : CC (F.obj (op V))) → CC (G.obj (op U)))
        x :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))
rw₁ :
  Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V) ≫ G.map (homOfLE h).op) :
          (a : CC (F.obj (op V))) → CC (G.obj (op U)))
        x :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))
rw₂ rw₃ :
  Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))
⊢ Eq (α := CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op U)) : (a : CC (F.obj (op U))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map (homOfLE h).op) :
              (a : CC (F.obj (op V))) → CC (F.obj (op U)))
            x :
          CC (F.obj (op U))) :
      CC (G.obj (op U)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (G.map (homOfLE h).op) : (a : CC (G.obj (op V))) → CC (G.obj (op U)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (e.app (op V)) : (a : CC (F.obj (op V))) → CC (G.obj (op V))) x :
          CC (G.obj (op V))) :
      CC (G.obj (op U)))

Tactic:
rw [← ConcreteCategory.comp_apply, NatTrans.naturality, ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst_1 : (X Y : C) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_2, v, u, u_1} C FC (CC := CC)
F : Presheaf.{w, v, u} C X
U : Opens (↑X : Type w)
x : ToType.{u_2, v, u, u_1} (FC := FC) (CC := CC) (F.obj (op U))
⊢ restrictOpen (FC := FC) (CC := CC) x U ⋯ = x

Tactic:
simp [restrictOpen, restrict]

Premises used: TopCat.Presheaf.restrict, TopCat.Presheaf.restrictOpen
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
ℱ 𝒢 : Presheaf.{w, v, u} C X
α : ℱ ⟶ 𝒢
U : (Opens (↑Y : Type w))ᵒᵖ
⊢ Eq (α := (obj (pushforward C f) ℱ).obj U ⟶ (obj (pushforward C f) 𝒢).obj U)
    (NatTrans.app (CategoryTheory.Functor.map (pushforward C f) α) U) (α.app (op ((Opens.map f).obj (unop U))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
⊢ Eq (α := Presheaf.{w, v, u} C X ⥤ Presheaf.{w, v, u} C X) (pushforward C (𝟙 X)) (𝟭 (Presheaf.{w, v, u} C X))

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, setOf, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.whiskerLeft, TopCat.Presheaf, Set.preimage, TopCat.Presheaf.pushforward, rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ℱ : Presheaf.{w, v, u} C X
U : (Opens (↑X : Type w))ᵒᵖ
⊢ (id ℱ).hom.app U = 𝟙 ((obj (pushforward C (𝟙 X)) ℱ).obj U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ℱ : Presheaf.{w, v, u} C X
U : (Opens (↑X : Type w))ᵒᵖ
⊢ (id ℱ).inv.app U = 𝟙 (ℱ.obj U)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X : TopCat
ℱ : Presheaf.{w, v, u} C X
⊢ obj (pushforward C (𝟙 X)) ℱ = ℱ

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, setOf, CategoryTheory.Functor.comp, TopCat.Presheaf, Set.preimage, rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
ℱ : Presheaf.{w, v, u} C X
⊢ obj (pushforward C (f ≫ g)) ℱ = obj (pushforward C g) (obj (pushforward C f) ℱ)

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Set.Mem, setOf, CategoryTheory.Functor.comp, Set.preimage, TopologicalSpace.Opens.map, rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
ℱ : Presheaf.{w, v, u} C X
U : (Opens (↑Z : Type w))ᵒᵖ
⊢ (comp f g ℱ).hom.app U = 𝟙 ((obj (pushforward C (f ≫ g)) ℱ).obj U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
ℱ : Presheaf.{w, v, u} C X
U : (Opens (↑Z : Type w))ᵒᵖ
⊢ (comp f g ℱ).inv.app U = 𝟙 ((obj (pushforward C g) (obj (pushforward C f) ℱ)).obj U)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf.{w, v, u} C X
rw rw₁ : obj (pushforward C g) ℱ = obj (pushforward C g) ℱ
⊢ obj (pushforward C f) ℱ = obj (pushforward C g) ℱ

Tactic:
rw [h]
-- Module: Mathlib.Topology.Sheaves.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf.{w, v, u} C X
U : (Opens (↑Y : Type w))ᵒᵖ
⊢ (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom ⋯)

Tactic:
simp [pushforwardEq]

Premises used: TopCat.Presheaf.pushforwardEq
-- 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)
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf.{w, v, u} C X
𝒢 : Presheaf.{w, v, u} C Y
H₂ : obj (pushforward C H₁.hom) ℱ ⟶ 𝒢
U : (Opens (↑X : Type w))ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [Opens.map, Set.preimage_preimage]

Premises used: Set.preimage_preimage, TopologicalSpace.Opens.map
-- 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 X
𝒢 : Presheaf.{w, v, u} C Y
H₂ : obj (pushforward C H₁.hom) ℱ ⟶ 𝒢
U : (Opens (↑X : Type w))ᵒᵖ
⊢ (toPushforwardOfIso H₁ H₂).app U = ℱ.map (eqToHom ⋯) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [toPushforwardOfIso, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, TopCat.Presheaf.toPushforwardOfIso
-- 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)
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))ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U))) = U

Tactic:
simp [Opens.map, Set.preimage_preimage]

Premises used: Set.preimage_preimage, TopologicalSpace.Opens.map