mathlib-initiative/mathlib-tactics huggingface dataset:
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 f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := gc } }.hom x =
    PresheafedSpace.Hom.stalkMap f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom x

Tactic:
← PresheafedSpace.stalkMap.comp ⟨g, gc⟩ f.hom,

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 f.hom ((ConcreteCategory.hom g) x) ≫
      PresheafedSpace.Hom.stalkMap { hom := { base := g, c := hc } }.hom 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
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base

Tactic:
by

Goal state after:
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
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ (F.map (𝟙 j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom.app U

Tactic:
by

Goal state after:
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
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑↑(F.obj j₃))ᵒᵖ
⊢ (F.map (f ≫ g)).c.app U =
    (F.map g).c.app U ≫
      ((pushforward C (F.map g).base).map (F.map f).c).app U ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U

Tactic:
by

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)
⊢ Mono f

Tactic:
by

Goal state after:
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 (colimit.ι F (unop k)).base).obj U)

Tactic:
by

Goal state after:
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)
i j k : Jᵒᵖ
f : i ⟶ j
g : j ⟶ k
⊢ (F.map (f ≫ g).unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
      (F.obj (unop k)).presheaf.map (eqToHom ⋯) =
    ((F.map f.unop).c.app (op ((Opens.map (colimit.ι F (unop i)).base).obj U)) ≫
        (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map g.unop).c.app (op ((Opens.map (colimit.ι F (unop j)).base).obj U)) ≫
        (F.obj (unop k)).presheaf.map (eqToHom ⋯)

Tactic:
by

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 : 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) y = (ConcreteCategory.hom h) y

Tactic:
by

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
⊢ ∃ inv,
    Hom.stalkMap α x ≫ inv = 𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x)) ∧
      inv ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
by

Goal state after:
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
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j : J
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j)).map (F.map (𝟙 j)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (𝟙 j)) (colimit.ι (F ⋙ forget C) j) (F.obj j).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j).presheaf).hom).op =
    𝟙 (op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf))

Tactic:
by

Goal state after:
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:
by

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)
⊢ Epi f

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
by

Goal state after:
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
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ
⊢ op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) =
    op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))

Tactic:
by

Goal state after:
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
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
by

Goal state after:
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
h : α.c ≍ β.c
⊢ α = β

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1

Tactic:
by

Goal state after:
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
inst✝ : HasColimitsOfShape J TopCat
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
⊢ ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map (f ≫ g)).c ≫
        (Pushforward.comp ((F ⋙ forget C).map (f ≫ g)) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₁).presheaf).inv ≫
          (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op =
    ((pushforward C (colimit.ι (F ⋙ forget C) j₂)).map (F.map f).c ≫
          (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j₂) (F.obj j₁).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₁).presheaf).hom).op ≫
      ((pushforward C (colimit.ι (F ⋙ forget C) j₃)).map (F.map g).c ≫
          (Pushforward.comp ((F ⋙ forget C).map g) (colimit.ι (F ⋙ forget C) j₃) (F.obj j₂).presheaf).inv ≫
            (pushforwardEq ⋯ (F.obj j₂).presheaf).hom).op

Tactic:
by

Goal state after:
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 ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
by

Goal state after:
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 ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
by

Goal state after:
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
inst✝¹ : HasColimitsOfShape J TopCat
inst✝ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') } =
    { base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by

Goal state after:
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
inst✝¹ : HasColimitsOfShape J TopCat
inst✝ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') } =
    { base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
by
        ext1
        · ext x
          exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
        · ext ⟨⟩
          simp [← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op)]

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X

Tactic:
by

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
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x = Hom.stalkMap f y ≫ X.presheaf.stalkSpecializes h

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
h : f.toHom = g.toHom
⊢ f = g

Tactic:
by

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
by

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv } = 𝟙 Y

Tactic:
by

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

Goal state before:
pp: X : LocallyRingedSpace
X✝ Y✝ : LocallyRingedSpace
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : forgetToSheafedSpace.map a₁✝ = forgetToSheafedSpace.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ⟶ Y.toSheafedSpace
h : ∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
⊢ U ≤ iSup V

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c = 𝟙 Y.presheaf

Tactic:
by

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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv = 𝟙 X

Tactic:
by

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

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom = 𝟙 Y

Tactic:
by

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

Goal state before:
pp: X✝ : LocallyRingedSpace
U : TopCat
X : LocallyRingedSpace
f : U ⟶ X.toTopCat
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ ∀ (x : ↑↑(X.restrict h).toPresheafedSpace), IsLocalRing ↑((X.restrict h).presheaf.stalk x)

Tactic:
by

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
⊢ Continuous fun x ↦ x.elim

Tactic:
by

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ ↑(X.presheaf.1 U) →+* PUnit.{u + 1}

Tactic:
by

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

Goal state before:
pp: X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
⊢ f = X.emptyTo

Tactic:
by

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.toRingedSpace.basicOpen 0 = ⊥

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c =
    𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)

Tactic:
by

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

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsNilpotent f
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.hom.base ≫ e.inv.base = 𝟙 ↑X.toPresheafedSpace

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.inv.base ≫ e.hom.base = 𝟙 ↑Y.toPresheafedSpace

Tactic:
by

Goal state after:
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
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
⊢ s.pt.presheaf.obj U ⟶
    ((pushforward C (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj
          (limit (pushforwardDiagramToColimit F).leftOp)).obj
      U

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
⊢ (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x'

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x : ↑X.toTopCat
⊢ Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
by

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
⊢ IsCompatible (sheaf X).obj V g

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ Hom.stalkMap e.hom ((ConcreteCategory.hom e.inv.base) y) ≫ Hom.stalkMap e.inv y = Y.presheaf.stalkSpecializes ⋯

Tactic:
by

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
y : ↑Y.toTopCat
z : ↑(Y.presheaf.stalk ((ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)))
⊢ y = (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y)

Tactic:
by

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : ↑X.toTopCat
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
by

Goal state after: