mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
            (op V) ≫
          colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (X.restrict h).presheaf)
            ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V))) ≫
      (X.restrictStalkIso h x).hom

Tactic:
]

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
            (op V) ≫
          colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (X.restrict h).presheaf)
            ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V))) ≫
      (X.restrictStalkIso h x).hom
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ sheafifyLift (Opens.grothendieckTopology ↑X) (⋯.pullbackIso.hom.app X✝.obj) ?refine_2.hP ≫
      ⋯.functor.op.whiskerLeft u.hom =
    sheafifyLift (Opens.grothendieckTopology ↑X) (⋯.pullbackIso.hom.app X✝.obj) ⋯ ≫ hf.functor.op.whiskerLeft u.hom

pp: case refine_2.hP
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑X) (⋯.functor.op ⋙ X✝.obj)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
]

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          h.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
]

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          h.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
⊢ (Opens.map β.hom.base).op = (Opens.map β.hom.base).op

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ β.hom = β.hom

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (X.restrictStalkIso h x).inv

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (X.restrictStalkIso h x).inv
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom ({ base := f, c := gc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := gc }.base) x) hx))
        s)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc gc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap { hom := { base := f, c := gc } }.hom x
U : Opens ↑↑Y.toPresheafedSpace
s : CC (Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ (Opens.map f).obj (unop (op U))
⊢ (ConcreteCategory.hom ({ base := f, c := fc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := fc }.base) x) hx))
        s) =
    (ConcreteCategory.hom ({ base := f, c := gc }.stalkMap x))
      ((ConcreteCategory.hom (Y.presheaf.germ (unop (op U)) ((ConcreteCategory.hom { base := f, c := gc }.base) x) hx))
        s)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ X.presheaf.stalk x' = X.presheaf.stalk x'

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom β.base) x') = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x')

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Y.presheaf.stalk ((ConcreteCategory.hom β.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Hom.stalkMap α x = Hom.stalkMap α x

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ X.presheaf.stalk x' = X.presheaf.stalk x'

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x') = Y.presheaf.stalk ((ConcreteCategory.hom α.base) x')

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ eqToHom ⋯ ≫ Hom.stalkMap α x' = eqToHom ⋯ ≫ Hom.stalkMap α x'

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ X.presheaf.stalk x = X.presheaf.stalk x

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap ({ base := g, c := gc } ≫ f.hom) x =
    PresheafedSpace.Hom.stalkMap ({ base := g, c := hc } ≫ f.hom) x

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Z.toPresheafedSpace ⟶ ↑X.toPresheafedSpace
gc hc : X.presheaf ⟶ (pushforward C g).obj Z.presheaf
e : { hom := { base := g, c := gc } } ≫ f = { hom := { base := g, c := hc } } ≫ f
x : ↑↑Z.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap ({ base := g, c := gc } ≫ f.hom) x =
    PresheafedSpace.Hom.stalkMap ({ base := g, c := hc } ≫ f.hom) x
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫
      Hom.stalkMap α ((ConcreteCategory.hom (α ≫ β).base) x) ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫
      Hom.stalkMap α ((ConcreteCategory.hom (α ≫ β).base) x) ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map ((F.map f.unop).base ≫ (colimit.ι F (unop j)).base)).obj U)

Tactic:
]

Goal state after:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(colimit F)
j k : Jᵒᵖ
f : j ⟶ k
⊢ (Opens.map (F.map f.unop).base).op.obj (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) =
    op ((Opens.map ((F.map f.unop).base ≫ (colimit.ι F (unop j)).base)).obj U)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap (β ≫ α) ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ eqToHom ⋯ ≫ Hom.stalkMap (β ≫ α) ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (ConcreteCategory.hom h) ((ConcreteCategory.hom f.hom.base) ⋯.choose)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (ConcreteCategory.hom h) ((ConcreteCategory.hom f.hom.base) ⋯.choose)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ 𝟙 (X.presheaf.stalk x) = 𝟙 (X.presheaf.stalk x)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := gc }) ⋯.choose =
    PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := hc }) ⋯.choose

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc hc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := g, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := gc }) ⋯.choose =
    PresheafedSpace.Hom.stalkMap (f.hom ≫ { base := g, c := hc }) ⋯.choose
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
⊢ (Opens.map β.base).op = (Opens.map β.base).op

Tactic:
]

Goal state after: