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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)

Tactic:
by

Goal state after:
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.OpenCover
f : 𝒰 ⟶ 𝒱
i : 𝒰.I₀
⊢ IsOpenImmersion (f.h₀ i ≫ 𝒱.f (f.s₀ i))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
this :
  IsIso
    ((colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).c.app
      (op (H.functor.obj U)))
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ ↑(⨆ i, Hom.opensRange (𝒰.f i)) = ↑⊤

Tactic:
by

Goal state after:
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
⊢ ∀ (x : ↥X), ∃ y, x ∈ Set.range ⇑(𝒰.f (Cover.idx 𝒰 ↑y))

Tactic:
by

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

Goal state after:
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
⊢ X.OpenCover

Tactic:
by

Goal state after:
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
H : CompactSpace ↥X
⊢ Fintype 𝒰.finiteSubcover.I₀

Tactic:
by

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

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
⊢ CompactSpace ↥X

Tactic:
by

Goal state after:
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
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ pullback.fst (𝒰.f i.fst) f ≫ 𝟙 (𝒰.X i.fst) = (pullbackSymmetry (𝒰.f i.fst) f).hom ≫ Cover.pullbackHom 𝒰 f i.fst

Tactic:
by

Goal state after:
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
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ ((fun i ↦ ((fun j ↦ (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd ≫ 𝟙 (𝒰.X i.fst) =
    𝟙 (𝒰.affineRefinement.openCover.X i) ≫ (𝒰.X i.fst).affineCover.f i.snd

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i =
    (Precoverage.ZeroHypercover.pullback₁ (Cover.pullbackHom 𝒰 f i.fst) (𝒰.X i.fst).affineCover).f i.snd ≫
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
⊢ IsIso ((colimit.ι F i).hom.c.app (op (⋯.functor.obj U)))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
⊢ (pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ Cover.pullbackHom 𝒰.affineRefinement.openCover f i =
    Cover.pullbackHom (𝒰.X i.fst).affineCover (Cover.pullbackHom 𝒰 f i.fst) i.snd

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasLimits C
ι✝ : Type v
F✝ : Discrete ι✝ ⥤ SheafedSpace C
inst✝³ : HasColimit F✝
i✝ : Discrete ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
ι' : Type v
e : ι ≃ ι'
f : Discrete ι' ≌ Discrete ι := Discrete.equivalence e.symm
⊢ colimit.ι F i =
    (colimit.ι F i ≫ (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).inv) ≫
      (HasColimit.isoOfEquivalence f (Iso.refl (f.functor ⋙ F))).hom

Tactic:
by

Goal state after:
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)
⊢ ∃ i, s i ∉ x.asIdeal

Tactic:
by

Goal state after:
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)
⊢ ι

Tactic:
by

Goal state after:
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)
⊢ x ∈
    Set.range
      ⇑(Spec.map
          (CommRingCat.ofHom
            (algebraMap (↑R)
              (Localization.Away
                (s
                  (have this := ⋯;
                  this.choose))))))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasLimits C
ι✝ : Type v
F✝ : Discrete ι✝ ⥤ SheafedSpace C
inst✝³ : HasColimit F✝
i✝ : Discrete ι✝
ι : Type w
inst✝² : Small.{v, w} ι
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
⊢ IsOpenImmersion (colimit.ι F i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PullbackCone f g

Tactic:
by

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

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ { l //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.snd f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit (forgetToSheafedSpace.mapCone (pullbackConeOfLeft f g))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ IsLimit ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).mapCone (pullbackConeOfLeft f g))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g) (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat)

Tactic:
by

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
by

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ lift f g H' ≫ f = g

Tactic:
by

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
⊢ ∀ {U V : Opens ↑(PrimeSpectrum.Top R)} (i : U ⟶ V) (f : (x : ↥V) → Localizations M ↑x),
    IsFraction f → IsFraction fun x ↦ f (i x)

Tactic:
by

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

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h : ∀ (i : 𝒰.I₀), IsNilpotent ((ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s)
⊢ IsNilpotent s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
hb : b ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (a + b) (i x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
x y : ↥U
⊢ ∃ (hs : 1 ∉ (↑y).asIdeal), (fun x ↦ 0 ((𝟙 U) x)) y = LocalizedModule.mk 0 ⟨1, hs⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : R
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ {f | (isLocallyFraction R M).pred f}
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R A).pred fun x ↦ (a * b) (i x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : R
x y : ↥U
⊢ 1 ∉ (↑y).asIdeal

Tactic:
by

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

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

Goal state before:
pp: X : Scheme
x : ↥X
r : ↑⋯.choose
⊢ Set.range ⇑(X.affineBasisCover.f ⟨x, r⟩) = ⇑(X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).carrier

Tactic:
by

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

Goal state before:
pp: X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ↑((structurePresheafInCommRingCat R ⋙ forget₂ CommRingCat RingCat).obj X)
    ↑((structurePresheafInModuleCat R M ⋙ forget₂ (ModuleCat R) Ab).obj X)

Tactic:
by

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

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ Set.range ⇑(ConcreteCategory.hom (lift f g H').base) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).inv ≫ f = Y.ofRestrict ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ IsIso (invApp f U)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : Epi f.base
⊢ Epi (forgetToSheafedSpace.map f).hom.base

Tactic:
by

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

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : Epi f.base
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (Hom.appLE U.ι U ⊤ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ U.ι ''ᵁ unop (op (U.ι ⁻¹ᵁ U)) = U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Nonempty ↥↑U ↔ (↑U).Nonempty

Tactic:
by

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
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ∃ g,
    ∃ (_ : x ∈ basicOpen g) (i : basicOpen g ≤ U),
      ∃ f, const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map i.hom.op)) s

Tactic:
by

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))
⊢ ↑(const 0 f U hu) x = ↑0 x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x✝ : ↥(unop (op U))
⊢ 1 • 1 • (algebraMap R A) f = 1 • ⟨f, ⋯⟩ • 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
⊢ U ≤ basicOpen 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
⊢ const 1 1 U ⋯ = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
f₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ U ≤ basicOpen (g₁ * g₂)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
f₁ f₂ : A
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ U ≤ basicOpen (g₁ * g₂)

Tactic:
by

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₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
h : g₂ • f₁ = g₁ • f₂
x : ↥(unop (op U))
⊢ ∃ u, u • ⟨g₂, ⋯⟩ • f₁ = u • ⟨g₁, ⋯⟩ • f₂

Tactic:
by

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₁ f₂ : M
g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
hf : f₁ = f₂
hg : g₁ = g₂
⊢ const f₁ g₁ U hu = const f₂ g₂ U ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g
hu₂ : U ≤ basicOpen f
⊢ const f g U hu₁ * const g f U hu₂ = 1

Tactic:
by

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

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
⊢ (U.stalkIso x).inv = Hom.stalkMap U.ι x

Tactic:
by

Goal state after: