awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_5 : HasColimit F
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
X : Jᵒᵖ
x : (↑((F ⋙ forget C).obj (unop X)) : Type v)
⊢ Eq (α := (F ⋙ forget C).obj (unop X) ⟶ (↑(Limits.colimit F) : TopCat))
    (colimit.ι (F ⋙ forget C) (unop X) ≫
      Hom.base
        (Iso.hom
          (Iso.symm
            (colimit.isoColimitCocone
              {
                cocone :=
                  {
                    pt :=
                      { carrier := Limits.colimit (F ⋙ forget C),
                        presheaf :=
                          (limit
                              (Functor.leftOp (pushforwardDiagramToColimit F) :
                                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                            Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                        PresheafedSpace.{v, u, v} C },
                    ι :=
                      {
                        app := fun (j : J) ↦
                          { base := colimit.ι (F ⋙ forget C) j,
                            c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) :
                            (F.obj j).Hom
                              (obj
                                (obj (Functor.const J)
                                  { carrier := Limits.colimit (F ⋙ forget C),
                                    presheaf :=
                                      (limit
                                          (Functor.leftOp (pushforwardDiagramToColimit F) :
                                            Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                        Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                    PresheafedSpace.{v, u, v} C })
                                j) },
                        naturality := ⋯ :
                        NatTrans F
                          (obj (Functor.const J)
                            { carrier := Limits.colimit (F ⋙ forget C),
                              presheaf :=
                                (limit
                                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                              PresheafedSpace.{v, u, v} C }) } :
                    Cocone F },
                isColimit := (colimitCoconeIsColimit F : IsColimit (colimitCocone F)) : ColimitCocone F }))))
    (Hom.base (colimit.ι F (unop X)))

Tactic:
ι_preservesColimitIso_inv (forget C) F (unop X)

Premises used: AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.ι_preservesColimitIso_inv, Opposite.unop
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_5 : HasColimit F
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
X : Jᵒᵖ
x : (↑((F ⋙ forget C).obj (unop X)) : Type v)
⊢ Eq (α := (F ⋙ forget C).obj (unop X) ⟶ (↑(Limits.colimit F) : TopCat))
    (colimit.ι (F ⋙ forget C) (unop X) ≫
      Hom.base
        (Iso.hom
          (Iso.symm
            (colimit.isoColimitCocone
              {
                cocone :=
                  {
                    pt :=
                      { carrier := Limits.colimit (F ⋙ forget C),
                        presheaf :=
                          (limit
                              (Functor.leftOp (pushforwardDiagramToColimit F) :
                                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                            Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                        PresheafedSpace.{v, u, v} C },
                    ι :=
                      {
                        app := fun (j : J) ↦
                          { base := colimit.ι (F ⋙ forget C) j,
                            c := limit.π (Functor.leftOp (pushforwardDiagramToColimit F)) (op j) :
                            (F.obj j).Hom
                              (obj
                                (obj (Functor.const J)
                                  { carrier := Limits.colimit (F ⋙ forget C),
                                    presheaf :=
                                      (limit
                                          (Functor.leftOp (pushforwardDiagramToColimit F) :
                                            Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                        Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                    PresheafedSpace.{v, u, v} C })
                                j) },
                        naturality := ⋯ :
                        NatTrans F
                          (obj (Functor.const J)
                            { carrier := Limits.colimit (F ⋙ forget C),
                              presheaf :=
                                (limit
                                    (Functor.leftOp (pushforwardDiagramToColimit F) :
                                      Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                                  Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C))) :
                              PresheafedSpace.{v, u, v} C }) } :
                    Cocone F },
                isColimit := (colimitCoconeIsColimit F : IsColimit (colimitCocone F)) : ColimitCocone F }))))
    (Hom.base (colimit.ι F (unop X)))

Tactic:
exact ι_preservesColimitIso_inv (forget C) F (unop X)

Premises used: AlgebraicGeometry.PresheafedSpace.forget, CategoryTheory.ι_preservesColimitIso_inv, Opposite.unop
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
j : J
⊢ Eq (α :=
    limit (componentwiseDiagram F U) ⟶ (F.obj j).presheaf.obj (op (obj (Opens.map (Hom.base (colimit.ι F j))) U)))
    (limit.π (componentwiseDiagram F U) (op j) ≫
      CategoryStruct.comp (Y :=
        (Functor.comp (D := CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
              (Functor.leftOp (pushforwardDiagramToColimit F) :
                Jᵒᵖ ⥤ Presheaf.{v, v, u} C (Limits.colimit (F ⋙ forget C)))
              (obj (evaluation (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C)
                  (op
                    (obj
                      (Opens.map
                        (Hom.base
                          (Iso.inv
                            (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                      U)) :
                CategoryTheory.Functor.{v, v, v, u} (Opens (↑(Limits.colimit (F ⋙ forget C)) : Type v))ᵒᵖ C ⥤ C)).obj
          (op j))
        (NatTrans.app (Iso.inv (NatIso.ofComponents (fun (X : Jᵒᵖ) ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯))
          (op j))
        (CategoryStruct.comp (Y :=
          (obj
                (pushforward C
                  (CategoryStruct.comp (Y := Limits.colimit F) (colimit.ι F j)
                      (Iso.hom
                        (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F :
                            ColimitCocone F }))).base)
                (F.obj j).presheaf).obj
            (op
              (obj
                (Opens.map
                  (Hom.base
                    (Iso.inv
                      (colimit.isoColimitCocone
                        { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F : ColimitCocone F }))))
                U)))
          ((F.obj j).presheaf.map (eqToHom ⋯))
          (map (obj (pushforward C (Hom.base (colimit.ι F j))) (F.obj j).presheaf) (eqToHom ⋯))))
    (limit.π (componentwiseDiagram F U) (op j))

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
j : J
rw :
  Eq (α := limit (componentwiseDiagram F U) ⟶ (componentwiseDiagram F U).obj (op j))
    (limit.π (componentwiseDiagram F U) (op j) :
      limit (componentwiseDiagram F U) ⟶ (componentwiseDiagram F U).obj (op j))
    (Iso.inv (colimitPresheafObjIsoComponentwiseLimit F U) ≫ NatTrans.app (Hom.c (colimit.ι F j)) (op U) :
      limit (componentwiseDiagram F U) ⟶ (componentwiseDiagram F U).obj (op j))
rw₁ rw₂ :
  Eq (α := limit (componentwiseDiagram F U) ⟶ (componentwiseDiagram F U).obj (op j))
    (limit.π (componentwiseDiagram F U) (op j)) (limit.π (componentwiseDiagram F U) (op j))
⊢ CategoryStruct.comp (Y := limit (componentwiseDiagram F U))
      (Iso.hom (colimitPresheafObjIsoComponentwiseLimit F U) :
        (Limits.colimit F).presheaf.obj (op U) ⟶ limit (componentwiseDiagram F U))
      (limit.π (componentwiseDiagram F U) (op j) :
        limit (componentwiseDiagram F U) ⟶ (componentwiseDiagram F U).obj (op j)) =
    NatTrans.app (Hom.c (colimit.ι F j)) (op U)

Tactic:
rw [← Iso.eq_inv_comp, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app]

Premises used: AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, CategoryTheory.Iso.eq_inv_comp
-- 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
α β : X.Hom Y
w : α.base = β.base
rw rw₁ : (Opens.map β.base).op = (Opens.map β.base).op
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
rw [w]
-- 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
α β : X.Hom Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
rcases :
  ∀ (base : (↑X : TopCat) ⟶ (↑Y : TopCat)) (c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf)
    (w : { base := base, c := c : X.Hom Y }.base = β.base)
    (h : { base := base, c := c : X.Hom Y }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c),
    { base := base, c := c : X.Hom Y } = β
⊢ α = β

Tactic:
rcases α with ⟨base, c⟩

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.Hom.c
-- 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
β : X.Hom Y
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
w : { base := base, c := c : X.Hom Y }.base = β.base
h : { base := base, c := c : X.Hom Y }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
rcases :
  ∀ (base' : (↑X : TopCat) ⟶ (↑Y : TopCat)) (c' : Y.presheaf ⟶ obj (Presheaf.pushforward C base') X.presheaf)
    (w : { base := base, c := c : X.Hom Y }.base = { base := base', c := c' }.base)
    (h : { base := base, c := c : X.Hom Y }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c),
    { base := base, c := c : X.Hom Y } = { base := base', c := c' }
⊢ { base := base, c := c : X.Hom Y } = β

Tactic:
rcases β with ⟨base', c'⟩
-- 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
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
base' : (↑X : TopCat) ⟶ (↑Y : TopCat)
c' : Y.presheaf ⟶ obj (Presheaf.pushforward C base') X.presheaf
w : base = base'
h : { base := base, c := c : X.Hom Y }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' : X.Hom Y }.c
subst :
  ∀ (c' : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf)
    (h :
      { base := base, c := c : X.Hom Y }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf =
        { base := base, c := c' : X.Hom Y }.c),
    { base := base, c := c : X.Hom Y } = { base := base, c := c' }
⊢ { base := base, c := c : X.Hom Y } = { base := base', c := c' }

Tactic:
subst w
-- 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
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c c' : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ c = c'

Tactic:
erw [whiskerRight_id', comp_id] at h

Premises used: CategoryTheory.Functor.whiskerRight_id', CategoryTheory.Category.comp_id
-- 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
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c c' : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
h : c = c'
subst : { base := base, c := c : X.Hom Y } = { base := base, c := c }
⊢ { base := base, c := c : X.Hom Y } = { base := base, c := c' }

Tactic:
subst h
-- 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
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
⊢ { base := base, c := c : X.Hom Y } = { base := base, c := c }

Tactic:
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
α β : X.Hom Y
w : α.base = β.base
h : α.c ≍ β.c
mk :
  ∀ (base : (↑X : TopCat) ⟶ (↑Y : TopCat)) (c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf)
    (w : { base := base, c := c : X.Hom Y }.base = β.base) (h : { base := base, c := c : X.Hom Y }.c ≍ β.c),
    { base := base, c := c : X.Hom Y } = β
⊢ α = β

Tactic:
cases α
-- 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
β : X.Hom Y
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
w : { base := base, c := c : X.Hom Y }.base = β.base
h : { base := base, c := c : X.Hom Y }.c ≍ β.c
mk :
  ∀ (base_1 : (↑X : TopCat) ⟶ (↑Y : TopCat)) (c_1 : Y.presheaf ⟶ obj (Presheaf.pushforward C base_1) X.presheaf)
    (w : { base := base, c := c : X.Hom Y }.base = { base := base_1, c := c_1 }.base)
    (h : { base := base, c := c : X.Hom Y }.c ≍ { base := base_1, c := c_1 : X.Hom Y }.c),
    { base := base, c := c : X.Hom Y } = { base := base_1, c := c_1 }
⊢ { base := base, c := c : X.Hom Y } = β

Tactic:
cases β
-- 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
base : (↑X : TopCat) ⟶ (↑Y : TopCat)
c : Y.presheaf ⟶ obj (Presheaf.pushforward C base) X.presheaf
base_1 : (↑X : TopCat) ⟶ (↑Y : TopCat)
c_1 : Y.presheaf ⟶ obj (Presheaf.pushforward C base_1) X.presheaf
w : { base := base, c := c : X.Hom Y }.base = { base := base_1, c := c_1 }.base
h : { base := base, c := c : X.Hom Y }.c ≍ { base := base_1, c := c_1 : X.Hom Y }.c
⊢ { base := base, c := c : X.Hom Y } = { base := base_1, c := c_1 }

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : PresheafedSpace.{v_1, u_1, u_2} C
α : X.Hom Y
β : Y.Hom Z
⊢ (comp α β).c = β.c ≫ map (Presheaf.pushforward C β.base) α.c

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Set.Mem, setOf, CategoryTheory.Functor.comp, Set.preimage, TopologicalSpace.Opens.map, 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
α β : X ⟶ Y
w : α.base = β.base
rw rw₁ : (Opens.map β.base).op = (Opens.map β.base).op
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
rw [w]
-- 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
α β : X ⟶ Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
Hom.ext α β w h

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.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
⊢ Hom.base (𝟙 X) = 𝟙 (↑X : TopCat)

Tactic:
rfl

Premises used: 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
⊢ Hom.c (𝟙 X) = 𝟙 X.presheaf

Tactic:
rfl

Premises used: 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))ᵒᵖ
rw : NatTrans.app (𝟙 X.presheaf) U = 𝟙 (X.presheaf.obj U)
⊢ (Hom.c (𝟙 X)).app U = X.presheaf.map (𝟙 U)

Tactic:
rw [id_c, map_id]

Premises used: CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.id_c
-- 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))ᵒᵖ
⊢ NatTrans.app (𝟙 X.presheaf) U = 𝟙 (X.presheaf.obj U)

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : PresheafedSpace.{v_1, u_1, u_2} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).base = f.base ≫ g.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : PresheafedSpace.{v_1, u_1, u_2} C
α : X ⟶ Y
β : Y ⟶ Z
U : (Opens (↑(↑Z : TopCat) : Type u_2))ᵒᵖ
⊢ (α ≫ β).c.app U = β.c.app U ≫ α.c.app (op ((Opens.map β.base).obj (unop U)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, 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
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y : TopCat) : Type u_2))ᵒᵖ
subst : (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
subst h
-- 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
α : X ⟶ Y
U : (Opens (↑(↑Y : TopCat) : Type u_2))ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
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
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y : TopCat) : Type u_2))ᵒᵖ
subst : α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)
⊢ α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
subst h
-- 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
α : X ⟶ Y
U : (Opens (↑(↑Y : TopCat) : Type u_2))ᵒᵖ
⊢ α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
simp
-- 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
H : (↑X : TopCat) ≅ (↑Y : TopCat)
α : obj (Presheaf.pushforward C H.hom) X.presheaf ≅ Y.presheaf
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 := (↑X : TopCat)) (Y := (↑X : TopCat))
              (Hom.base
                ({ base := H.hom, c := α.inv : X.Hom Y } ≫
                  { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom })) :
            (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))
      ((CategoryStruct.comp (Y :=
            obj
              (Presheaf.pushforward C
                (Hom.base
                  ({ base := H.hom, c := α.inv : X.Hom Y } ≫
                    { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom : Y.Hom X })))
              X.presheaf)
            (Hom.c
              ({ base := H.hom, c := α.inv : X.Hom Y } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }))
            (whiskerRight (eqToHom ⋯) X.presheaf)).app
        (op U))
      ((Hom.c (𝟙 X)).app (op U))
⊢ { base := H.hom, c := α.inv : X.Hom Y } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X

Tactic:
ext
-- 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
H : (↑X : TopCat) ≅ (↑Y : TopCat)
α : obj (Presheaf.pushforward C H.hom) X.presheaf ≅ Y.presheaf
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 := (↑X : TopCat)) (Y := (↑X : TopCat))
            (Hom.base
              ({ base := H.hom, c := α.inv : X.Hom Y } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom })) :
          (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:
simp
-- 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
H : (↑X : TopCat) ≅ (↑Y : TopCat)
α : obj (Presheaf.pushforward C H.hom) X.presheaf ≅ Y.presheaf
U : Opens (↑(↑X : TopCat) : Type u_2)
⊢ Eq (α := X.presheaf.obj (op U) ⟶ ((Opens.map (Hom.base (𝟙 X))).op ⋙ X.presheaf).obj (op U))
    ((CategoryStruct.comp (Y :=
          obj
            (Presheaf.pushforward C
              (Hom.base
                ({ base := H.hom, c := α.inv : X.Hom Y } ≫
                  { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom : Y.Hom X })))
            X.presheaf)
          (Hom.c
            ({ base := H.hom, c := α.inv : X.Hom Y } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }))
          (whiskerRight (eqToHom ⋯) X.presheaf)).app
      (op U))
    ((Hom.c (𝟙 X)).app (op U))

Tactic:
simp