mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0

Tactic:
]

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop✝ : Opens ↑↑Z
⊢ g.c.app (op unop✝) ≫
      Y.presheaf.map (((Opens.map g.base).map (homOfLE ⋯).op.unop).op ≫ eqToHom ⋯ ≫ (⋯.functor.map (eqToHom ⋯)).op) =
    g.c.app (op unop✝) ≫ Y.presheaf.map (⋯.adjunction.counit.app ((Opens.map g.base).obj unop✝)).op

Tactic:
]

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop✝ : Opens ↑↑Z
⊢ g.c.app (op unop✝) ≫
      Y.presheaf.map (((Opens.map g.base).map (homOfLE ⋯).op.unop).op ≫ eqToHom ⋯ ≫ (⋯.functor.map (eqToHom ⋯)).op) =
    g.c.app (op unop✝) ≫ Y.presheaf.map (⋯.adjunction.counit.app ((Opens.map g.base).obj unop✝)).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s) ↔
    (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

pp: case h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)

Tactic:
]

Goal state after:
case h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ stalkMap f x ≫ X.presheaf.stalkSpecializes ?h = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯

pp: case h
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ y ⤳ x

Tactic:
]

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
⊢ CoverPreserving (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X) (Opens.map f.base)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ CoverPreserving (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X) (Opens.map f.base)
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
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
⊢ ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹' ↑(unop U) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)

Tactic:
]

Goal state after:
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
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
s' : PullbackCone f.base g.base := PullbackCone.mk s.fst.base s.snd.base ⋯
this : limit.lift (cospan f.base g.base) s' ≫ limit.π (cospan f.base g.base) WalkingCospan.right = s.snd.base
⊢ ⇑(TopCat.Hom.hom (limit.lift (cospan f.base g.base) (PullbackCone.mk s.fst.base s.snd.base ⋯))) ⁻¹' ↑(unop U) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange g = opensRange g

Tactic:
]

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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
]

Goal state after:
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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
]

Goal state after:
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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (⋯.functor.op.map i) ≫
        s.pt.presheaf.map (eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯) ≫
        ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i
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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯ ≫ (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.map i)

Tactic:
]

Goal state after:
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
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map ((Opens.map s.snd.base).op.map (⋯.functor.op.map i) ≫ eqToHom ⋯) =
    s.snd.c.app (⋯.functor.op.obj U) ≫
      s.pt.presheaf.map (eqToHom ⋯ ≫ (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.map i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f (f ''ᵁ f ⁻¹ᵁ V))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f (f ''ᵁ f ⁻¹ᵁ V))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫ X.presheaf.map (eqToHom ⋯) =
    app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ (∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)) ↔
    Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
]

Goal state after:
X Y : Type u
f : X ⟶ Y
⊢ (∀ (x : Y), ∃ Y_1 g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)) ↔
    Function.Surjective ⇑(ConcreteCategory.hom f)
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 : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ U
⊢ V ≤ U

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ U
⊢ V ≤ U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
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 ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
]

Goal state after:
case refine_2.op
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 ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        Y.presheaf.map (eqToHom ⋯) ≫
          s.snd.c.app (⋯.functor.op.obj ((Opens.map (pullbackConeOfLeft f g).fst.base).op.obj (op x))) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

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

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (op U))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ ∀ (x : (fun X ↦ X) X), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))

Tactic:
]

Goal state after:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ ∀ (x : (fun X ↦ X) X), ∃ i_1, x ∈ Set.range ⇑(ConcreteCategory.hom ((E.restrictIndex i).f i_1))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
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 ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
]

Goal state after:
case refine_2.op
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 ↑↑X
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
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
R : Presieve X
⊢ map F R ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj X) ↔
    ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
⊢ map F R ∈ Types.jointlySurjectivePrecoverage.coverings (F.obj X) ↔
    ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R : CommRingCat
g : ↑R
⊢ ↑(opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))))) = ↑(PrimeSpectrum.basicOpen g)

Tactic:
]

Goal state after:
R : CommRingCat
g : ↑R
⊢ ↑(opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))))) = ↑(PrimeSpectrum.basicOpen g)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2.op
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 ↑↑X
this :
  (f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)) =
    g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x)))
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
]

Goal state after:
case refine_2.op
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 ↑↑X
this :
  (f.c.app (op ((opensFunctor f).obj x)) ≫ s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x)))) ≫
      inv (s.pt.presheaf.map (eqToHom ⋯)) =
    g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x)))
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsOpenImmersion
    (Spec.map (CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

Tactic:
]

Goal state after:
R S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
f : R
inst✝ : IsLocalization.Away f S
e :
  (↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm).comp
      (algebraMap R (Localization.Away f)) =
    algebraMap R S
⊢ IsOpenImmersion
    (Spec.map (CommRingCat.ofHom ↑↑(IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f)).symm) ≫
      Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ∀ (x : (fun X ↦ X) (F.obj Y)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
H :
  ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g],
    Function.Surjective ⇑(ConcreteCategory.hom (pullbackComparison F f g))
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : ∀ (x : (fun X ↦ X) (F.obj S)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (f i)))
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ∀ (x : (fun X ↦ X) (F.obj Y)), ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (F.map (p₁ i)))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ⊆
      ↑U

Tactic:
]

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ⊆
      ↑U
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U

Tactic:
]

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U