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

Goal state before:
pp: case h
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
U✝ : Opens ↑↑X
⊢ (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)

Tactic:
simp

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

Goal state before:
pp: case refine_1
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)ᵒᵖ
j : Jᵒᵖ
⊢ op ((Opens.map (s.ι.app (unop j)).base).obj (unop U)) =
    op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j) ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj
        (unop U))

Tactic:
simp

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
U : Opens ↑↑Y
eq₁ :
  H.inv.c.app (op ((Opens.map H.hom.base).obj U)) ≫
      H.hom.c.app (op ((Opens.map H.inv.base).obj (unop (op ((Opens.map H.hom.base).obj U))))) =
    eqToHom ⋯
eq₂ :
  eqToHom ⋯ ≫ H.hom.c.app (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    H.hom.c.app (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯)
⊢ eqToHom ⋯ ≫ ((Presheaf.pushforward C H.hom.base).obj X.presheaf).map (eqToHom ⋯) =
    𝟙 (((Presheaf.pushforward C H.hom.base).obj X.presheaf).obj (op U))

Tactic:
simp

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

Goal state before:
pp: case refine_2
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)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
w :
  op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
        ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U))) =
    op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))
w' :
  (F.map f.unop).c.app
      (op
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
          ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) =
    (F.obj (unop j)).presheaf.map (eqToHom w) ≫
      (F.map f.unop).c.app (op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))) ≫
        ((pushforward C (F.map f.unop).base).obj (F.obj (unop j')).presheaf).map (eqToHom ⋯)
⊢ 𝟙 (s.pt.presheaf.obj U) ≫
      ((F.map f.unop ≫ s.ι.app (unop j)).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯)) ≫
        (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((F.obj (unop j)).presheaf.map (eqToHom w) ≫
          (F.map f.unop).c.app (op ((Opens.map (((forget C).mapCocone s).ι.app (unop j))).obj (unop U))) ≫
            ((pushforward C (F.map f.unop).base).obj (F.obj (unop j')).presheaf).map (eqToHom ⋯)) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯

Tactic:
simp

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:
simp

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

Goal state before:
pp: case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)

Tactic:
rw [← stalkMap_germ_apply] at hx

Goal state after:
case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case h
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
U : Opens ↑↑s.pt
⊢ limit.lift
        ((pushforwardDiagramToColimit F).leftOp ⋙
          (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
        { pt := s.pt.presheaf.obj (op U),
          π :=
            { app := fun j ↦ (s.ι.app (unop j)).c.app (op U) ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯),
              naturality := ⋯ } } ≫
      limit.π
          ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj U)))
          (op j) ≫
        (whiskerRight (eqToHom ⋯) (F.obj j).presheaf).app (op U) =
    (s.ι.app j).c.app (op U)

Tactic:
simp

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

Goal state before:
pp: case p
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion').obj U✝))

Tactic:
simp

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
j : J
x✝ : ↑((F ⋙ forget C).obj j)
⊢ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ m.base)) x✝ =
    (ConcreteCategory.hom ((forget C).map ((colimitCocone F).ι.app j ≫ m))) x✝

Tactic:
simp

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

Goal state before:
pp: case w
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
⊢ autoParam
    (∀ (j : J),
      (colimit.cocone (F ⋙ forget C)).ι.app j ≫ (Iso.refl (colimit.cocone (F ⋙ forget C)).pt).hom =
        ((forget C).mapCocone (colimitCocone F)).ι.app j)
    Cocone.ext._auto_1

Tactic:
simp

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

Goal state before:
pp: case zero
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : 0 < 0 + Nat.succ 0
⊢ X.basicOpen (f ^ (0 + Nat.succ 0)) = X.basicOpen f

Tactic:
simp

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
⊢ limit.π (componentwiseDiagram F U) (op j) ≫
      (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv.app (op j) ≫
        (F.obj j).presheaf.map (eqToHom ⋯) ≫
          ((pushforward C (colimit.ι F j).base).obj (F.obj j).presheaf).map (eqToHom ⋯) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
simp

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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).obj.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((CommRingCat.Hom.hom (eqToHom ⋯)) x✝) =
    (CommRingCat.Hom.hom ((𝟙 (sheafedSpaceObj R).toPresheafedSpace).c.app (op U✝))) x✝

Tactic:
simp

Goal state after:
case h
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (RingHom.id ↑((structureSheaf ↑R).obj.obj (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))) x✝ =
    (RingHom.id ↑((structureSheaf ↑R).obj.obj (op U✝))) x✝
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 : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map (𝟙 ((Opens.map f.base).op.obj x)) = f.c.app x

Tactic:
simp

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 : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
x✝ : ↑↑Z
⊢ x✝ ∈ ↑(h.functor.obj U) ↔ x✝ ∈ ↑((opensFunctor g).obj ((opensFunctor f).obj U))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
⊢ ↑(f ⁻¹ᵁ iSup U) = ↑(⨆ i, f ⁻¹ᵁ U i)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
⊢ (f ≫ g) x = g (f x)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = app f U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ appTop (inv f) = inv (appTop f)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑(Ideal.span ↑I * Ideal.span ↑J)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
x✝ : ↥X
⊢ x✝ ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) ↔ x✝ ∈ X.zeroLocus s

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case refl
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom ⋯).op) ⁻¹ᵁ W)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ (e.hom ≫ e.inv) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ (e.inv ≫ e.hom) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))
⊢ e.hom (e.inv y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
y : ↑(X.presheaf.stalk (e.inv (e.hom x)))
⊢ e.inv (e.hom x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ (Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f y)).hom =
    (Arrow.mk (stalkMap f x)).hom ≫ (X.presheaf.stalkCongr ⋯).hom

Tactic:
by
    simp only [Arrow.mk_left, Arrow.mk_right, TopCat.Presheaf.stalkCongr_hom,
      Arrow.mk_hom]
    rw [stalkSpecializes_stalkMap]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ ↑(f ''ᵁ ⊤) = ↑(opensRange f)

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullback.lift s.fst.base s.snd.base ⋯ ≫ pullback.fst f.base g.base = s.fst.base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: case h
ι : Type (u_1 + 1)
S : Type u_1
X : ι → Type u_1
f : (i : ι) → X i ⟶ S
σ : ι → Type (u_1 + 1)
Y : (i : ι) → σ i → Type u_1
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hf : ∀ (x : S), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (f i))
hg : ∀ (i : ι) (x : X i), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom (g i i_1))
i : ι
j : σ i
z : Y i j
⊢ (ConcreteCategory.hom (g ⟨i, j⟩.fst ⟨i, j⟩.snd ≫ f ⟨i, j⟩.fst)) z =
    (ConcreteCategory.hom (f i)) ((ConcreteCategory.hom (g i j)) z)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u_1
R S : Presieve X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
x✝ : S ∈ jointlySurjectivePrecoverage.coverings X
x : X
⊢ ∃ Y g, (R ⊔ S) g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
obtain ⟨Y, f, hf, hx⟩ := hR x

Goal state after:
X : Type u_1
R S : Presieve X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
x✝ : S ∈ jointlySurjectivePrecoverage.coverings X
x : X
Y : Type u_1
f : Y ⟶ X
hf : R f
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ ∃ Y g, (R ⊔ S) g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ U = 𝟙 X ''ᵁ U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opens
⊢ g ''ᵁ f ''ᵁ U = (f ≫ g) ''ᵁ U

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
ι : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : MorphismProperty C
S✝ : C
E : P.precoverage.ZeroHypercover S✝
⊢ (E.restrictIndex PEmpty.elim).presieve₀ ∈ P.precoverage.coverings S✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

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
P : MorphismProperty D
F : C ⥤ D
X : C
ι : Type (max u_1 v_1)
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ (Precoverage.comap F P.precoverage).coverings X ↔
    Presieve.ofArrows Y f ∈ (P.inverseImage F).precoverage.coverings X

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ pullback.lift s.fst.base s.snd.base ⋯ ≫ pullback.snd f.base g.base = s.snd.base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K L : Precoverage C
P : MorphismProperty C
inst✝ : K.HasIsos
X : C
⊢ Presieve.singleton (𝟙 X) (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := pullbackSymmetry f g
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ ∃ a, (pullback.snd f g) a = y

Tactic:
use (pullbackSymmetry f g).inv a

Goal state after:
case h
P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
hf : P f
x : ↥X
y : ↥Y
h : f x = g y
iso : pullback f g ≅ pullback g f := ⋯
this : HasPullback g f
a : ↥(pullback g f)
ha : (pullback.fst g f) a = y
⊢ (pullback.snd f g) ((pullbackSymmetry f g).inv a) = y
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ precoverage P ≤ precoverage Q

Tactic:
precoverage,

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ jointlySurjectivePrecoverage ⊓ P.precoverage ≤ precoverage Q

Tactic:
precoverage,

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ jointlySurjectivePrecoverage ⊓ P.precoverage ≤ jointlySurjectivePrecoverage ⊓ Q.precoverage
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : (Opens ↑↑Y)ᵒᵖ
⊢ s.snd.c.app x ≫ s.pt.presheaf.map (𝟙 ((Opens.map s.snd.base).op.obj x)) = s.snd.c.app x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift g f ⋯ ≫ lift f g ⋯) ≫ f = 𝟙 X ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ (precoverage P).coverings X ↔ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(E.f i)) ∧ ∀ (i : E.I₀), P (E.f i)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g

Tactic:
simp

Goal state after: