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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      CommRingCat.ofHom
          (algebraMap ↑S
            ↑((structureSheaf ↑S).obj.obj
                (op
                  ((TopologicalSpace.Opens.comap
                      { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ })
                    ⊤)))) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

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

Tactic:
rfl

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

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

Goal state before:
pp: case app.op.mk
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)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ↑{ carrier := carrier✝, is_open' := is_open'✝ } = carrier✝

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
rfl

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'
⊢ app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

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

Tactic:
rfl

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

Tactic:
by
  rw [← H.isoRestrict_hom_ofRestrict]; apply mono_comp

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

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ app (eqToHom ⋯) U = eqToHom ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
⊢ f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g

Tactic:
have hxU : x ∈ U := X.basicOpen_le _ hx

Goal state after:
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ carrier✝ =
    ⇑(ConcreteCategory.hom f.base) ''
      ↑((↑(TopCat.Hom.frameHom f.base)).toFunctor.obj { carrier := carrier✝, is_open' := is_open'✝ })

Tactic:
exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm

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
⊢ (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
grind

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
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso (Hom.stalkMap ((isoRestrict f).hom ≫ Y.ofRestrict ⋯) x)

Tactic:
PresheafedSpace.stalkMap.comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso
    (Hom.stalkMap (Y.ofRestrict ⋯) ((ConcreteCategory.hom (isoRestrict f).hom.base) x) ≫
      Hom.stalkMap (isoRestrict f).hom x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case op.op
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
unop✝¹ unop✝ : Opens ↑↑X
i : op unop✝¹ ⟶ op unop✝
⊢ invApp f unop✝¹ ≫
      g.c.app (op ((opensFunctor f).obj unop✝¹)) ≫
        Y.presheaf.map (((Opens.map g.base).map ((opensFunctor f).map i.unop)).op ≫ eqToHom ⋯) =
    invApp f unop✝¹ ≫
      g.c.app (op (⋯.functor.obj unop✝¹)) ≫
        Y.presheaf.map (eqToHom ⋯ ≫ (⋯.functor.map ((Opens.map (pullback.fst f.base g.base)).map i.unop)).op)

Tactic:
rfl

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 : (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:
rfl

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

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

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

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

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.IsMultiplicative
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : Q.IsMultiplicative
inst✝ : Q.IsStableUnderBaseChange
⊢ (P.precoverage ⊓ Q.precoverage).coverings = (P.pretopology ⊓ Q.pretopology).coverings

Tactic:
rfl

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

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.fst f.base g.base))

Tactic:
rw [TopCat.pullback_fst_range f.base g.base]

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ x ∈ {x | ∃ y, f x = g y}
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
ι : Type u_1
X : ι → Scheme
f : (i : ι) → X i ⟶ S
⊢ Presieve.ofArrows X f ∈ (precoverage P).coverings S ↔ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)

Tactic:
simp_rw [← Scheme.forget_map', ← Scheme.forget_obj,
    ← Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff]
  exact ⟨fun hmem ↦ ⟨hmem.1, fun i ↦ hmem.2 ⟨i⟩⟩, fun h ↦ ⟨h.1, fun {Y} g ⟨i⟩ ↦ h.2 i⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }

Tactic:
rfl

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

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ j y, (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ (∀ (x : ↥X), ∃ i y, (map i) y = x) ∧ ∀ (i : J), P (map i)

Tactic:
grind

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

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ 𝒰.presieve₀ ∈ (precoverage Q).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : JointlySurjective K
𝒰 : Cover K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑(𝒰.f i)) ∧ ∀ (i : 𝒰.I₀), Q (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ { I₀ := J, X := obj, f := map }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := obj, f := map }.f i)) ∧
    ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰✝ : Cover K X✝
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f✝) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (𝒰.add f).presieve₀ ∈ (precoverage P).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
K : Precoverage Scheme
X✝ Y✝ Z : Scheme
𝒰✝ : Cover K X✝
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f✝) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑((𝒰.add f).f i)) ∧ ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover P X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)) ∧
    ∀ (i : { I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.I₀),
      P ({ I₀ := 𝒰.I₀, X := fun j ↦ Spec (𝒰.X j), f := 𝒰.f }.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
⊢ iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W

Tactic:
by
  ext x
  by_cases hx : x ∈ Set.range iU
  · obtain ⟨x, rfl⟩ := hx
    simp only [SetLike.mem_coe, Opens.map_coe, Set.mem_preimage, ← Scheme.Hom.comp_apply, ← H.w]
    simp
  · constructor
    · rintro ⟨x, hx, rfl⟩; cases hx ⟨x, rfl⟩
    · rintro ⟨y, hy, e : iV y = f x⟩
      obtain ⟨x, rfl⟩ := (IsOpenImmersion.range_pullbackSnd iV f).ge ⟨y, e⟩
      rw [← H.isoPullback_inv_snd] at hx
      cases hx ⟨_, rfl⟩

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

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
⊢ { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.I₀),
      P ({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
X✝ Y Z : Scheme
𝒰 : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
X : Scheme
U : (x : ↑X.toTopCat) → OpenNhds x
R : ↑X.toTopCat → CommRingCat
h : ∀ (x : ↑X.toTopCat), Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)))
e : (x : ↑X.toTopCat) → X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op (R x)) := fun x ↦ ⋯.some
⊢ (∀ (x : ↥X),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.I₀),
      IsOpenImmersion
        ({ I₀ := ↥X, X := fun x ↦ Spec (R x), f := fun x ↦ { toLRSHom' := (e x).inv ≫ X.ofRestrict ⋯ } }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
X✝ Y Z : Scheme
𝒰✝ : X✝.OpenCover
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
X : Scheme
𝒰 : X.OpenCover
H : CompactSpace ↥X
this : ∃ t, ⋃ x ∈ t, Set.range ⇑(𝒰.f (Cover.idx 𝒰 x)) = ⊤
t : Finset ↥X := this.choose
h : ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))
⊢ (∀ (x : ↥X),
      ∃ i, x ∈ Set.range ⇑({ I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.f i)) ∧
    ∀ (i : { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.I₀),
      IsOpenImmersion ({ I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x) }.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ False

Tactic:
apply x.2.ne_top

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ x.asIdeal = ⊤
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  f.stalkMap ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x) ≫
      PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯ ≫ g.toHom) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))

Tactic:
PresheafedSpace.stalkMap.comp

Goal state after:
case prop
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
x : ↑↑(Y.restrict ⋯).toPresheafedSpace
this :
  f.stalkMap ((ConcreteCategory.hom (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom).base) x) ≫
      PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x =
    eqToHom ⋯ ≫
      g.stalkMap ((ConcreteCategory.hom (Y.ofRestrict ⋯).base) x) ≫ PresheafedSpace.Hom.stalkMap (Y.ofRestrict ⋯) x
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f.toHom g.toHom) x))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ { I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
        f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings (Spec R)

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ (∀ (x : ↥(Spec R)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
                    f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
                i)) ∧
    ∀
      (i :
        { I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.I₀),
      IsOpenImmersion
        ({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (∃ x, x ∈ U) ↔ (↑U).Nonempty

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ 0 = ↑0 x

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ : M
g₁ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
⊢ const f₁ g₁ U hu = const f₁ g₁ U ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
presieve₀_mem_precoverage_iff

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)) ∧
    ∀ (i : { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.I₀),
      IsOpenImmersion ({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
x : ↥X
hx : x ∈ U
⊢ (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) ⟨x, hx⟩ = ⟨x, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
R : TopCommRingCat
X : TopCatᵒᵖ
x✝ : ↑(continuousFunctions X R)
⊢ (CommRingCat.Hom.hom (continuousFunctions.pullback (𝟙 X) R)) x✝ =
    (CommRingCat.Hom.hom (𝟙 (continuousFunctions X R))) x✝

Tactic:
rfl

Goal state after: