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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap e.inv ((ConcreteCategory.hom e.hom.base) x) ≫ Hom.stalkMap e.hom x = X.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
x : ↑X.toTopCat
y : ↑(X.presheaf.stalk ((ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)))
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) 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)
⊢ IsUnit 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)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U V : (Opens ↑↑s.pt)ᵒᵖ
i : U ⟶ V
⊢ s.pt.presheaf.map i ≫ descCApp F s V =
    descCApp F s U ≫
      ((pushforward C (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (colimitCocone F).pt.presheaf).map i

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))
⊢ IsOpen {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) 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.basicOpen f ≤ U

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))
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f)

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
⊢ (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)

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)
⊢ Mono (X.ofRestrict hf)

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
⊢ (X.restrict ⋯).presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

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
j : J
⊢ (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j

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
⊢ X.presheaf = (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj (X.restrict ⋯).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 : PresheafedSpace C
⊢ (X.ofRestrict ⋯).c = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) = unop V ⊓ X.basicOpen 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)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) = X.basicOpen f

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
⊢ X.ofRestrict ⋯ ≫ X.toRestrictTop = 𝟙 (X.restrict ⋯)

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
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = desc F s

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

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
⊢ IsColimit ((forget C).mapCocone (colimitCocone 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))
n : ℕ
h : 0 < n
⊢ X.basicOpen (f ^ n) = X.basicOpen f

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
⊢ X.toRestrictTop ≫ X.ofRestrict ⋯ = 𝟙 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
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
⊢ { base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F } = 𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ 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))
hf : IsUnit f
⊢ X.basicOpen f = U

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ IsClosed (X.zeroLocus s)

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.zeroLocus {f} = (X.basicOpen f).carrierᶜ

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
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F } =
    { base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.zeroLocus ∅ = Set.univ

Tactic:
by

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
⊢ ∃! s, (X.presheafToTypes T).IsGluing U sf s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (X.continuousPrelocal T).pred fun x ↦ f (i x)
⊢ (X.continuousPrelocal T).pred f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ (P.and Q.toPrelocalPredicate).pred f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
V U : Opens ↑X
i : V ⟶ U
f : (x : ↥U) → T ↑x
w : ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
x : ↥V
⊢ ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
w :
  ∀ (x : ↥U),
    ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
h : P.pred f
x : ↥U
⊢ P.pred fun x ↦ f ((𝟙 U) x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_2
P : PrelocalPredicate T
op : {x : ↑X} → T x → T x
hop : ∀ {U : Opens ↑X} {a : (x : ↥U) → T ↑x}, P.pred a → ∀ (p : ↥U), ∃ W i, ↑p ∈ W ∧ P.pred fun x ↦ op (a (i x))
U : Opens ↑X
a : (x : ↥U) → T ↑x
ha : P.sheafify.pred a
⊢ P.sheafify.pred fun x ↦ op (a x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T₁ : ↑X → Type u_2
T₂ : ↑X → Type u_3
T₃ : ↑X → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : ↑X} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
    P₁.pred a → P₂.pred b → ∀ (p : ↥(U ⊓ V)), ∃ W ia ib, ↑p ∈ W ∧ P₃.pred fun x ↦ op (a (ia x)) (b (ib x))
U : Opens ↑X
a : (x : ↥U) → T₁ ↑x
b : (x : ↥U) → T₂ ↑x
ha : P₁.sheafify.pred a
hb : P₂.sheafify.pred b
⊢ P₃.sheafify.pred fun x ↦ op (a x) (b x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
⊢ IsCompatible (X.sheafToTypes T).obj U sf'

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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
⊢ (Limits.colimit F).presheaf.obj (op U) ≅ limit (componentwiseDiagram F U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
⊢ ∃! s, (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
U : Opens ↑X
x : ↑X
hx : x ∈ U
f : (fun X ↦ X) ((subsheafToTypes P).presheaf.obj (op U))
⊢ (ConcreteCategory.hom (stalkToFiber P x)) ((ConcreteCategory.hom ((subsheafToTypes P).presheaf.germ U x hx)) f) =
    ↑f ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
t : (fun X ↦ X) (T x)
⊢ ∃ a, (ConcreteCategory.hom (stalkToFiber P x)) a = t

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

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
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (colimitPresheafObjIsoComponentwiseLimit F U).hom ≫ limit.π (componentwiseDiagram F U) (op j) =
    (colimit.ι F j).c.app (op U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
x : ↑X
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥↑U) → T ↑y),
    P.pred fU →
      ∀ (fV : (y : ↥↑V) → T ↑y), P.pred fV → fU ⟨x, ⋯⟩ = fV ⟨x, ⋯⟩ → ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)
tU tV : (fun X ↦ X) ((subsheafToTypes P).presheaf.stalk x)
h : (ConcreteCategory.hom (stalkToFiber P x)) tU = (ConcreteCategory.hom (stalkToFiber P x)) tV
⊢ tU = tV

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝² x✝¹ : (TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (sheafedSpaceObj R).presheaf.map x✝ ≫
      CommRingCat.ofHom
        (comap (CommRingCat.Hom.hom f) (unop x✝¹) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝¹)) ⋯) =
    CommRingCat.ofHom
        (comap (CommRingCat.Hom.hom f) (unop x✝²) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝²)) ⋯) ≫
      ((TopCat.Presheaf.pushforward CommRingCat (topMap f)).obj (sheafedSpaceObj S).presheaf).map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ U✝ = (TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ sheafedSpaceMap (𝟙 R) = 𝟙 (sheafedSpaceObj R)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ sheafedSpaceMap (f ≫ g) = sheafedSpaceMap g ≫ sheafedSpaceMap f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ sheafedSpaceMap (f ≫ g).unop = sheafedSpaceMap f.unop ≫ sheafedSpaceMap g.unop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
r : ↑R
U : TopologicalSpace.Opens (PrimeSpectrum ↑R) := PrimeSpectrum.basicOpen r
⊢ (TopologicalSpace.Opens.map α.hom.base).op.obj (op U) = (TopologicalSpace.Opens.map β.hom.base).op.obj (op U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫ toStalk (↑S) p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ (CommRingCat.Hom.hom
        (((stalkIso (↑R) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).toRingEquiv.toCommRingCatIso.symm.inv ≫
            PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) ≫
          (stalkIso (↑S) p).toRingEquiv.toCommRingCatIso.symm.hom))
      ((algebraMap (↑R) (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal)) x) =
    (algebraMap (↑S) (Localization.AtPrime p.asIdeal)) ((CommRingCat.Hom.hom f) x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toPresheafedSpace
a : ↑((locallyRingedSpaceObj R).presheaf.stalk ((ConcreteCategory.hom (sheafedSpaceMap f).hom.base) p))
ha : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (sheafedSpaceMap f).hom p)) a)
⊢ IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
⊢ (locallyRingedSpaceMap (𝟙 R)).toHom = (𝟙 (locallyRingedSpaceObj R)).toHom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (locallyRingedSpaceMap (f ≫ g)).toHom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 R).unop = 𝟙 (locallyRingedSpaceObj (unop R))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (f ≫ g).unop = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
⊢ (𝟭 CommRingCat).map f ≫ (asIso (toSpecΓ Y)).hom =
    (asIso (toSpecΓ X)).hom ≫ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (PresheafedSpace.Hom.stalkMap (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op)
      x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toStalk (↑R) p ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).hom.c

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ PresheafedSpace.IsOpenImmersion f.toHom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
        (structureSheaf ↑S).obj).obj
    (op (PrimeSpectrum.basicOpen r))) :=
  (ConcreteCategory.hom
      (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (structureSheaf ↑S).obj).map
        (homOfLE hrU).op))
    s
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
⊢ (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf ≅ (Y.restrict ⋯).presheaf

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
a b : ↥X
⊢ a ≤ b ↔ b ⤳ a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
x : ↥X
hx : IsClosed {x}
⊢ height x = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ appLE f U V e ≫ X.presheaf.map i = appLE f U V' ⋯

Tactic:
by

Goal state after: