mathlib-initiative/mathlib-tactics huggingface dataset:
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.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toHom = g.toHom
⊢ { toHom := toHom✝, prop := prop✝ } = g

Tactic:
;

Goal state after:
case mk
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝, prop := prop✝ }.toHom = g.toHom
⊢ { toHom := toHom✝, prop := prop✝ } = g
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toHom = { toHom := toHom✝, prop := prop✝ }.toHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }

Tactic:
;

Goal state after:
case mk.mk
X Y : LocallyRingedSpace
toHom✝¹ : X.Hom Y.toPresheafedSpace
prop✝¹ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝¹.stalkMap x))
toHom✝ : X.Hom Y.toPresheafedSpace
prop✝ : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom✝.stalkMap x))
h : { toHom := toHom✝¹, prop := prop✝¹ }.toHom = { toHom := toHom✝, prop := prop✝ }.toHom
⊢ { toHom := toHom✝¹, prop := prop✝¹ } = { toHom := toHom✝, prop := prop✝ }
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:
;

Goal state after:
X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

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

Tactic:
;

Goal state after:
X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))
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
⊢ IsUnit f

Tactic:
choose g hg using fun x : U => IsUnit.exists_right_inv (h_unit x)

Goal state after:
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
⊢ IsUnit f
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case h
X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
carrier✝ : Set ↑↑X.toPresheafedSpace
is_open'✝ : IsOpen carrier✝
x : ↑(X.presheaf.obj (op { carrier := carrier✝, is_open' := is_open'✝ }))
⊢ (CommRingCat.Hom.hom
        ((f.c ≫ whiskerRight (eqToHom ⋯) ∅.presheaf).app (op { carrier := carrier✝, is_open' := is_open'✝ })))
      x =
    (CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier✝, is_open' := is_open'✝ }))) x

Tactic:
;

Goal state after:
case h
X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
carrier✝ : Set ↑↑X.toPresheafedSpace
is_open'✝ : IsOpen carrier✝
x : ↑(X.presheaf.obj (op { carrier := carrier✝, is_open' := is_open'✝ }))
⊢ (CommRingCat.Hom.hom
        ((f.c ≫ whiskerRight (eqToHom ⋯) ∅.presheaf).app (op { carrier := carrier✝, is_open' := is_open'✝ })))
      x =
    (CommRingCat.Hom.hom (X.emptyTo.c.app (op { carrier := carrier✝, is_open' := is_open'✝ }))) x
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ (ConcreteCategory.hom (X.presheaf.germ U y ⋯)) f =
    (CommRingCat.Hom.hom (X.presheaf.germ V y hy)) ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
exact (X.presheaf.germ_res_apply i y hy f).symm

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
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ U

Tactic:
;

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ U
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 : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
;

Goal state after:
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f

Tactic:
;

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ unop V ⊓ X.basicOpen f ≤ X.basicOpen f
Module: Mathlib.Geometry.RingedSpace.Basic

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

Tactic:
;

Goal state after:
case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
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)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
;

Goal state after:
case refine_1
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)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
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)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
;

Goal state after:
case refine_1
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)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
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)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
;

Goal state after:
case refine_2
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)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
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)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
;

Goal state after:
case refine_2
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)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝³ x✝² : (TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((sheafedSpaceObj R).presheaf.obj x✝³)
⊢ (CommRingCat.Hom.hom
        ((sheafedSpaceObj R).presheaf.map x✝¹ ≫
          CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom f) (unop x✝²) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝²)) ⋯)))
      x✝ =
    (CommRingCat.Hom.hom
        (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✝¹))
      x✝

Tactic:
;

Goal state after:
R S : CommRingCat
f : R ⟶ S
x✝³ x✝² : (TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((sheafedSpaceObj R).presheaf.obj x✝³)
⊢ (CommRingCat.Hom.hom
        ((sheafedSpaceObj R).presheaf.map x✝¹ ≫
          CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom f) (unop x✝²) ((TopologicalSpace.Opens.map (topMap f)).obj (unop x✝²)) ⋯)))
      x✝ =
    (CommRingCat.Hom.hom
        (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✝¹))
      x✝
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
apply ((TopCat.Sheaf.pushforward _ β.hom.base).obj X.sheaf).hom_ext _
      PrimeSpectrum.isBasis_basic_opens

Goal state after:
case h
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)
⊢ ∀ (i : ↑R),
    (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen i)) =
      β.hom.c.app (op (PrimeSpectrum.basicOpen i))
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
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)
⊢ ∀ (i : ↑R),
    (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen i)) =
      β.hom.c.app (op (PrimeSpectrum.basicOpen i))

Tactic:
intro r

Goal state after:
case h
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)
r : ↑R
⊢ (α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    β.hom.c.app (op (PrimeSpectrum.basicOpen r))
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
;

Goal state after:
R : CommRingCat
⊢ (𝟙 (sheafedSpaceObj R)).hom = (𝟙 (locallyRingedSpaceObj R)).toHom
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
;

Goal state after:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
;

Goal state after:
R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
;

Goal state after:
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x' =
    ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x'

Tactic:
;

Goal state after:
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x' =
    ↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op)) x✝) x'
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
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
e :
  (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
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
;

Goal state after:
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
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
e :
  (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
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1
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
⊢ Mono ((isoRestrict f).hom ≫ Y.ofRestrict ⋯)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono ((isoRestrict f).hom ≫ Y.ofRestrict ⋯)
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
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V ⋯)

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toLRSHom' := toLRSHom'✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toLRSHom' := toLRSHom'✝ } = g

Tactic:
;

Goal state after:
case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝ }.base = g.base
h_app : ∀ (U : Y.Opens), { toLRSHom' := toLRSHom'✝ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ { toLRSHom' := toLRSHom'✝ } = g
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }

Tactic:
;

Goal state after:
case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ { toLRSHom' := toLRSHom'✝¹ } = { toLRSHom' := toLRSHom'✝ }
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:
;

Goal state after:
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))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹ = toLRSHom'✝

Tactic:
apply LocallyRingedSpace.Hom.ext'

Goal state after:
case mk.mk
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.toHom = toLRSHom'✝.toHom
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝ }.toLRSHom = toLRSHom g
⊢ { toLRSHom' := toLRSHom'✝ } = g

Tactic:
;

Goal state after:
case mk
X Y : Scheme
g : X ⟶ Y
toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom'✝ }.toLRSHom = toLRSHom g
⊢ { toLRSHom' := toLRSHom'✝ } = g