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

Goal state before:
pp: X✝ Y : Scheme
U✝ : X✝.Opens
hU : IsAffineOpen U✝
f : ↑Γ(X✝, U✝)
X : Scheme
U : X.Opens
⊢ (fun U_1 ↦ ↑U_1 ≤ Scheme.Hom.opensRange U.ι) = fun V ↦ ↑V ≤ U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ⁻¹ᵁ U = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯ ≫ equalizer.ι f g =
    pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯ ≫ pullback.fst s v

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.fst s v ≫ s = pullback.snd s v ≫ v

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.fst s v ≫ s = pullback.snd s v ≫ v

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

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
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ 1 • ↑s • f = ↑s • 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
x : ↑(PrimeSpectrum.Top R)
f : M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (localizationtoStalkₗ R M x)) (LocalizedModule.mk f s) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑s) x ⋯)) (const f (↑s) (basicOpen ↑s) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U = (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs =
    pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
Scheme.preimage_basicOpen,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) =
    (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ toStalkₗ' R M x ≫ stalkToLocalizationₗ R M x = ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
      equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯ =
    𝟙 (equalizer lhs rhs)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ (𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec = X.toΓSpec ≫ (Γ.rightOp ⋙ Spec.toLocallyRingedSpace).map f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = PrimeSpectrum.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₀
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
            ⋯ ≫
          pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯) ≫
        pullback.fst (equalizer.ι f g) (pullback.fst s v)) ≫
      equalizer.ι f g =
    (𝟙 (pullback (equalizer.ι f g) (pullback.fst s v)) ≫ pullback.fst (equalizer.ι f g) (pullback.fst s v)) ≫
      equalizer.ι f g

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
            ⋯ ≫
          pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯) ≫
        pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.fst s v =
    (𝟙 (pullback (equalizer.ι f g) (pullback.fst s v)) ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.fst s v

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := ⋯
rhs : pullback s v ⟶ pullback t v := ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ ((equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
            ⋯ ≫
          pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
            (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯) ≫
        pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.snd s v =
    (𝟙 (pullback (equalizer.ι f g) (pullback.fst s v)) ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v)) ≫
      pullback.snd s v

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (X.basicOpen f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ g✝ : X✝ ⟶ Y✝
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯) ⋯ ≫
      pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ =
    𝟙 (pullback (equalizer.ι f g) (pullback.fst s v))

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 : ↑(PrimeSpectrum.Top R)
⊢ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x = 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : ↑Γ(X, ⊤)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).hom ≫ pullback.fst (equalizer.ι f g) (pullback.fst s v) ≫ equalizer.ι f g =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.fst s v

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ ↑x ∈ X.basicOpen r

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : ↑x ∈ X.basicOpen r
⊢ X.basicOpen r ≤ V

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v) =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ↑x ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ X.basicOpen ((CommRingCat.Hom.hom U.topIso.hom) r) ≤ V ∧ ↑x ∈ X.basicOpen ((CommRingCat.Hom.hom U.topIso.hom) r)

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 : ↑(PrimeSpectrum.Top R)
⊢ localizationtoStalkₗ R M x ≫ stalkToLocalizationₗ R M x = 𝟙 (ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).inv ≫
      equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.fst s v =
    pullback.fst (equalizer.ι f g) (pullback.fst s v) ≫ equalizer.ι f g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
⊢ ∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).inv ≫
      equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯) ≫ pullback.snd s v =
    pullback.snd (equalizer.ι f g) (pullback.fst s v) ≫ pullback.snd s v

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 : ↑(PrimeSpectrum.Top R)
⊢ IsLocalizedModule x.asIdeal.primeCompl (ModuleCat.Hom.hom (toStalkₗ' R M x))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H :
  ∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : Presieve Y⦄,
    R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], R g → P (pullback.snd f g))
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X} {U : C} {g : U ⟶ X},
    R ∈ K.coverings X → R g → P f → ∀ [inst : HasPullback f g], P (pullback.snd f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H :
  ∀ ⦃X Y : C⦄ ⦃f : X ⟶ Y⦄ ⦃R : Presieve Y⦄,
    R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], R g → P (pullback.snd f g))
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X},
    R ∈ K.coverings X → (∀ {U : C} {g : U ⟶ X} [inst : HasPullback f g], R g → P (pullback.snd f g)) → P f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
R : Presieve Y
hR : R ∈ K.coverings Y
f : X ⟶ Y
⊢ P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : HasPullback f g], R g → P (pullback.snd f g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : P.RespectsIso
H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P.IsLocalAtTarget K

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 : ↑(PrimeSpectrum.Top R)
m : M
⊢ x ∈ ⊤

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X} {U : C} {g : U ⟶ X},
    R ∈ K.coverings X → R g → ⊤ f → ∀ [inst : HasPullback f g], ⊤ (pullback.snd f 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
x : ↑(PrimeSpectrum.Top R)
⊢ ∀ (x_1 y : M),
    (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) (x_1 + y)) =
      (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) x_1) +
        (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) y)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K✝ : Precoverage C
P : MorphismProperty C
K L : Precoverage C
⊢ ∀ {X Y : C} {f : Y ⟶ X} {R : Presieve X},
    R ∈ K.coverings X → (∀ {U : C} {g : U ⟶ X} [inst : HasPullback f g], R g → ⊤ (pullback.snd f g)) → ⊤ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
hU.fromSpec.naturality_assoc,

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (Scheme.Hom.app hU.fromSpec U ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)
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 : ↑(PrimeSpectrum.Top R)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) (r • m)) =
    (RingHom.id R) r • (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
X' : C
i : 𝒰.I₀
fst : X' ⟶ X
snd : X' ⟶ 𝒰.X i
h : IsPullback fst snd f (𝒰.f i)
hf : P f
⊢ P snd

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : K.HasPullbacks
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ ∀ {U : C} {g : U ⟶ Y} [inst : HasPullback f g], 𝒰.presieve₀ g → P (pullback.snd f g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

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 : ↑(PrimeSpectrum.Top R)
m : M
α : stalk (moduleStructurePresheaf R M).presheaf x ≅
  (forget₂ (ModuleCat R) Ab).obj ((structurePresheafInModuleCat R M).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ (ModuleCat R) Ab).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInModuleCat R M)) }
⊢ x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X✝ Y✝ : Scheme
U✝ : X✝.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X✝, U✝)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
this : IsLocalization.Away ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
  ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) :=
  isLocalization_basicOpen hV ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r) ≤ f ⁻¹ᵁ Y.basicOpen r

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝² : K.HasPullbacks
inst✝¹ : P.IsLocalAtTarget K
X Y : C
f : X ⟶ Y
𝒰 : K.ZeroHypercover Y
inst✝ : 𝒰.Small
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
K : Precoverage C
inst✝ : P.RespectsIso
H : ∀ {X Y : C} {f : X ⟶ Y} {R : Presieve X}, R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (g ≫ f))
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
R✝ : Presieve X✝
hR : R✝ ∈ K.coverings X✝
x✝¹ : C
x✝ : x✝¹ ⟶ X✝
hg : R✝ x✝
hf : P f✝
⊢ P (x✝ ≫ f✝)

Tactic:
by

Goal state after: