awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this_2 :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  Eq (α :=
    (obj (Presheaf.pushforward C (X.ofRestrict hf).base) (X.restrict hf).presheaf).obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C g₁.base) Z.presheaf).obj
        (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯))
⊢ (X.restrict hf).presheaf.map (Quiver.Hom.op (eqToHom hV)) ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    (X.restrict hf).presheaf.map (Quiver.Hom.op (eqToHom hV)) ≫
      g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)

Tactic:
have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this_2 :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  Eq (α :=
    (obj (Presheaf.pushforward C (X.ofRestrict hf).base) (X.restrict hf).presheaf).obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C g₁.base) Z.presheaf).obj
        (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯))
h :
  (X.restrict hf).presheaf.map (Quiver.Hom.op (eqToHom hV)) ≫
      g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    (X.restrict hf).presheaf.map (Quiver.Hom.op (eqToHom hV)) ≫
      g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ g₁.c.app (op V) ≫ (obj (Presheaf.pushforward C g₁.base) Z.presheaf).map (Quiver.Hom.op (eqToHom hV)) =
    g₂.c.app (op V) ≫
      (obj (Presheaf.pushforward C g₂.base) Z.presheaf).map (Quiver.Hom.op (eqToHom hV)) ≫ Z.presheaf.map (eqToHom ⋯)

Tactic:
simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h

Premises used: CategoryTheory.NatTrans.naturality, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this_2 :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  Eq (α :=
    (obj (Presheaf.pushforward C (X.ofRestrict hf).base) (X.restrict hf).presheaf).obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C g₁.base) Z.presheaf).obj
        (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯))
h :
  g₁.c.app (op V) ≫ (obj (Presheaf.pushforward C g₁.base) Z.presheaf).map (Quiver.Hom.op (eqToHom hV)) =
    g₂.c.app (op V) ≫
      (obj (Presheaf.pushforward C g₂.base) Z.presheaf).map (Quiver.Hom.op (eqToHom hV)) ≫ Z.presheaf.map (eqToHom ⋯)
⊢ Eq (α := (X.restrict hf).presheaf.obj (op V) ⟶ (obj (Presheaf.pushforward C g₂.base) Z.presheaf).obj (op V))
    (g₁.c.app (op V) ≫ eqToHom ⋯) (g₂.c.app (op V))

Tactic:
simp only [eqToHom_op, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_op, CategoryTheory.inv_eqToHom, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace.{v_1, u_1, u_2} C
f : U ⟶ (↑X : TopCat)
hf :
  IsOpenEmbedding (X := (↑U : Type u_2)) (Y := (↑(↑X : TopCat) : Type u_2))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
          TopCat.carrier) f) :
      (a : (↑U : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
this_1 : Mono f
Z : PresheafedSpace.{v_1, u_1, u_2} C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens (↑(↑(X.restrict hf) : TopCat) : Type u_2)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this_2 :
  IsIso (X := (Opens.map f ⋙ ⋯.functor).obj (unop (op (hf.functor.obj V))))
    (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  Eq (α :=
    (obj (Presheaf.pushforward C (X.ofRestrict hf).base) (X.restrict hf).presheaf).obj (op (hf.functor.obj V)) ⟶
      (obj (Presheaf.pushforward C g₁.base) Z.presheaf).obj
        (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))))
    (g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯))
h :
  Eq (α := (X.restrict hf).presheaf.obj (op V) ⟶ (obj (Presheaf.pushforward C g₂.base) Z.presheaf).obj (op V))
    (g₁.c.app (op V) ≫ eqToHom ⋯) (g₂.c.app (op V))
⊢ Eq (α := (X.restrict hf).presheaf.obj (op V) ⟶ ((Opens.map g₂.base).op ⋙ Z.presheaf).obj (op V))
    ((g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V)) (g₂.c.app (op V))

Tactic:
simpa using h
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
rw :
  Functor.op (Opens.map (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)))) ⋙ X.presheaf =
    obj (Presheaf.pushforward C (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)))) X.presheaf
⊢ Functor.op (IsOpenEmbedding.functor ⋯) ⋙ X.presheaf =
    obj (Presheaf.pushforward C (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)))) X.presheaf

Tactic:
rw [Opens.inclusion'_top_functor X.carrier]

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, TopologicalSpace.Opens.inclusion'_top_functor
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
⊢ Functor.op (Opens.map (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)))) ⋙ X.presheaf =
    obj (Presheaf.pushforward C (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)))) X.presheaf

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
rw :
  X.presheaf =
    obj (Presheaf.pushforward C (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)) ≫ Hom.base (X.ofRestrict ⋯))) X.presheaf
⊢ X.presheaf =
    obj (Presheaf.pushforward C (Hom.base (X.ofRestrict ⋯)))
      (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf

Tactic:
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]

Premises used: TopCat.Presheaf.Pushforward.comp_eq, AlgebraicGeometry.PresheafedSpace.restrict_top_presheaf
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
⊢ X.presheaf =
    obj (Presheaf.pushforward C (Iso.inv (Opens.inclusionTopIso (↑X : TopCat)) ≫ Hom.base (X.ofRestrict ⋯))) X.presheaf

Tactic:
tauto
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
w :
  ∀ (U : Opens (↑(↑X : TopCat) : Type u_2)),
    Eq (α :=
      X.presheaf.obj (op U) ⟶
        (obj (Presheaf.pushforward C (Hom.base (X.ofRestrict ⋯)))
              (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                  ⋯).presheaf).obj
          (op U))
      (NatTrans.app (Hom.c (X.ofRestrict ⋯)) (op U)) (NatTrans.app (eqToHom ⋯) (op U))
⊢ Hom.c (X.ofRestrict ⋯) = eqToHom ⋯

Tactic:
ext
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U : Opens (↑(↑X : TopCat) : Type u_2)
w :
  Eq (α :=
    X.presheaf.obj (op U) ⟶
      X.presheaf.obj
        (op
          (obj (C :=
            Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
            (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))))
    (X.presheaf.map (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) U)) :
      X.presheaf.obj (op U) ⟶
        X.presheaf.obj
          (op
            (obj (C :=
              Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
              (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))))
    (NatTrans.app (eqToHom ⋯) (op U) :
      X.presheaf.obj (op U) ⟶
        (obj (C :=
              Presheaf.{u_2, v_1, u_1} C
                (obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤))
              (Presheaf.pushforward C (Opens.inclusion' ⊤)) (Functor.op (IsOpenEmbedding.functor ⋯) ⋙ X.presheaf)).obj
          (op U))
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      (obj (Presheaf.pushforward C (Hom.base (X.ofRestrict ⋯)))
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf).obj
        (op U))
    (NatTrans.app (Hom.c (X.ofRestrict ⋯)) (op U)) (NatTrans.app (eqToHom ⋯) (op U))

Tactic:
dsimp [ofRestrict]

Premises used: AlgebraicGeometry.PresheafedSpace.ofRestrict
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U : Opens (↑(↑X : TopCat) : Type u_2)
w :
  op U =
    op
      (obj (C := Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
        (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      X.presheaf.obj
        (op
          (obj (C :=
            Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
            (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))))
    (X.presheaf.map (Quiver.Hom.op (NatTrans.app (Adjunction.counit (IsOpenMap.adjunction ⋯)) U)) :
      X.presheaf.obj (op U) ⟶
        X.presheaf.obj
          (op
            (obj (C :=
              Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
              (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))))
    (NatTrans.app (eqToHom ⋯) (op U) :
      X.presheaf.obj (op U) ⟶
        (obj (C :=
              Presheaf.{u_2, v_1, u_1} C
                (obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤))
              (Presheaf.pushforward C (Opens.inclusion' ⊤)) (Functor.op (IsOpenEmbedding.functor ⋯) ⋙ X.presheaf)).obj
          (op U))

Tactic:
erw [eqToHom_map, eqToHom_app]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.eqToHom_app
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U : Opens (↑(↑X : TopCat) : Type u_2)
⊢ op U =
    op
      (obj (C := Opens (↑(obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) : Type u_2))
        (IsOpenEmbedding.functor ⋯) (obj (Opens.map (Opens.inclusion' ⊤)) U))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
x :
  (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) : TopCat) :
    Type u_2)
⊢ Eq (α :=
    (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) : TopCat) :
      Type u_2))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC := TopCat.carrier)
            (X :=
            (↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) :
              TopCat))
            (Hom.base (X.ofRestrict ⋯ ≫ X.toRestrictTop)) :
          (a : (↑(↑(X.restrict ⋯) : TopCat) : Type u_2)) → (↑(↑(X.restrict ⋯) : TopCat) : Type u_2))
        x :
      (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) :
            TopCat) :
        Type u_2))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC := TopCat.carrier)
            (Hom.base
              (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯))) :
          (a : (↑(↑(X.restrict ⋯) : TopCat) : Type u_2)) → (↑(↑(X.restrict ⋯) : TopCat) : Type u_2))
        x :
      (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) :
            TopCat) :
        Type u_2))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U :
  Opens
    (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) : TopCat) :
      Type u_2)
h :
  Eq (α :=
    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf.obj
        (op U) ⟶
      ((Opens.map
                (Hom.base
                  (𝟙
                    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                      ⋯)))).op ⋙
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf).obj
        (op U))
    (NatTrans.app
      (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf)
      (op U))
    ((Hom.c (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯))).app
      (op U))
⊢ Eq (α :=
    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf.obj
        (op U) ⟶
      ((Opens.map
                (Hom.base
                  (𝟙
                    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                      ⋯)))).op ⋙
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf).obj
        (op U))
    ((CategoryStruct.comp (Y :=
          obj (Presheaf.pushforward C (Hom.base (X.ofRestrict ⋯ ≫ X.toRestrictTop)))
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf)
          (Hom.c (X.ofRestrict ⋯ ≫ X.toRestrictTop))
          (whiskerRight (eqToHom ⋯)
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf)).app
      (op U))
    ((Hom.c (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯))).app
      (op U))

Tactic:
erw [comp_c, toRestrictTop_c, whiskerRight_id',
        comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Functor.whiskerRight_id', CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.comp_c, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U :
  Opens
    (↑(↑(X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯) : TopCat) :
      Type u_2)
⊢ Eq (α :=
    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf.obj
        (op U) ⟶
      ((Opens.map
                (Hom.base
                  (𝟙
                    (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                      ⋯)))).op ⋙
            (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤)
                ⋯).presheaf).obj
        (op U))
    (NatTrans.app
      (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯).presheaf)
      (op U))
    ((Hom.c (𝟙 (X.restrict (U := obj (C := Opens (↑(↑X : TopCat) : Type u_2)) (Opens.toTopCat (↑X : TopCat)) ⊤) ⋯))).app
      (op U))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
w :
  ∀ (x : (↑(↑X : TopCat) : Type u_2)),
    Eq (α := (↑(↑X : TopCat) : Type u_2))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
              TopCat.carrier) (X.toRestrictTop ≫ X.ofRestrict ⋯).base :
            (a : (↑(↑X : TopCat) : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
          x :
        (↑(↑X : TopCat) : Type u_2))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC :=
              TopCat.carrier) (Hom.base (𝟙 X)) :
            (a : (↑(↑X : TopCat) : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
          x :
        (↑(↑X : TopCat) : Type u_2))
h :
  ∀ (U : Opens (↑(↑X : TopCat) : Type u_2)),
    Eq (α := X.presheaf.obj (op U) ⟶ ((Opens.map (Hom.base (𝟙 X))).op ⋙ X.presheaf).obj (op U))
      (NatTrans.app ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf) (op U))
      ((Hom.c (𝟙 X)).app (op U))
⊢ X.toRestrictTop ≫ X.ofRestrict ⋯ = 𝟙 X

Tactic:
ext
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
x : (↑(↑X : TopCat) : Type u_2)
⊢ Eq (α := (↑(↑X : TopCat) : Type u_2))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC := TopCat.carrier)
            (X.toRestrictTop ≫ X.ofRestrict ⋯).base :
          (a : (↑(↑X : TopCat) : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
        x :
      (↑(↑X : TopCat) : Type u_2))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_2}) ↦ C((↑X : Type u_2), (↑Y : Type u_2))) (CC := TopCat.carrier)
            (Hom.base (𝟙 X)) :
          (a : (↑(↑X : TopCat) : Type u_2)) → (↑(↑X : TopCat) : Type u_2))
        x :
      (↑(↑X : TopCat) : Type u_2))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U : Opens (↑(↑X : TopCat) : Type u_2)
h :
  Eq (α := X.presheaf.obj (op U) ⟶ ((Opens.map (Hom.base (𝟙 X))).op ⋙ X.presheaf).obj (op U))
    (NatTrans.app (𝟙 X.presheaf) (op U)) ((Hom.c (𝟙 X)).app (op U))
⊢ Eq (α := X.presheaf.obj (op U) ⟶ ((Opens.map (Hom.base (𝟙 X))).op ⋙ X.presheaf).obj (op U))
    (NatTrans.app ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf) (op U))
    ((Hom.c (𝟙 X)).app (op U))

Tactic:
erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Functor.whiskerRight_id', CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, AlgebraicGeometry.PresheafedSpace.ofRestrict_top_c, AlgebraicGeometry.PresheafedSpace.toRestrictTop_c, AlgebraicGeometry.PresheafedSpace.comp_c, CategoryTheory.eqToHom_trans
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
U : Opens (↑(↑X : TopCat) : Type u_2)
⊢ Eq (α := X.presheaf.obj (op U) ⟶ ((Opens.map (Hom.base (𝟙 X))).op ⋙ X.presheaf).obj (op U))
    (NatTrans.app (𝟙 X.presheaf) (op U)) ((Hom.c (𝟙 X)).app (op U))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : PresheafedSpace.{v_1, u_1, u_2} C
⊢ obj Γ (op X) = X.presheaf.obj (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : PresheafedSpace.{v_1, u_1, u_2} C
f : X ⟶ Y
⊢ Eq (α := obj Γ (op Y) ⟶ obj Γ (op X)) (map Γ f.op) (f.c.app (op ⊤))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X : PresheafedSpace.{v_1, u_1, u_3} C
⊢ (↑(F.mapPresheaf.obj X) : TopCat) = (↑X : TopCat)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X : PresheafedSpace.{v_1, u_1, u_3} C
⊢ (F.mapPresheaf.obj X).presheaf = X.presheaf ⋙ F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y : PresheafedSpace.{v_1, u_1, u_3} C
f : X ⟶ Y
⊢ (F.mapPresheaf.map f).base = f.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y : PresheafedSpace.{v_1, u_1, u_3} C
f : X ⟶ Y
⊢ (F.mapPresheaf.map f).c = whiskerRight f.c F

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerRight, rfl