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

Goal state before:
pp: case refine_1.mpr
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
⊢ x ∈ ↑⊥ → x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ })

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
⊢ RingHom.ker (algebraMap (↑R) (↑R ⧸ Ideal.span {e})) = Ideal.span {1 - (1 - e)}

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
⊢ PrimeSpectrum.zeroLocus ↑(RingHom.ker (Ideal.Quotient.mk (Ideal.span {e}))) = PrimeSpectrum.zeroLocus {e}

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.glueDataObjι U ≫ (↑U).ι = Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
by
  rw [glueDataObjι, Category.assoc]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
simp

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ ∃ i x, (𝒰.f i) x ∈ U ∧ (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f i).base) x) = x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊤ * I).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ x ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier → x ∈ ⇑f '' U

Tactic:
simp

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ ∀ (x_1 : 𝒰.I₀) (x_2 : ↥(𝒰.X x_1)),
    (𝒰.f x_1) x_2 ∈ U → (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f x_1).base) x_2) = x → ∃ x_3 ∈ U, f x_3 = x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊤).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊥ * I).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊥).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
inst✝ : IsAffine X
I : X.IdealSheafData
⊢ (ofIdealTop ((fun x ↦ x.ideal ⟨⊤, ⋯⟩) I)).ideal ⟨⊤, ⋯⟩ = I.ideal ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ (fun x ↦ x.ideal ⟨⊤, ⋯⟩) (ofIdealTop I) = I

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x * y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ * y.ideal ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x + y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ + y.ideal ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
simp

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv '' PrimeSpectrum.zeroLocus ↑(I.ideal U) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x))))
⊢ X.isoSpec.inv (X.isoSpec.hom x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ f ⁻¹ᵁ Y.basicOpen s = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op) ≫
        (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ ker (inv f ≫ f ≫ g) ≤ ker g

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑⟨⊤, ⋯⟩)) ≤
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal ⟨⊤, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mp
X : Scheme
R : CommRingCat
f₁ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ ∃ (h₁ : f₁.fst = f₁.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₁.snd

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
⊢ (ConcreteCategory.hom (X.evaluation U x hx)) f ≠ 0 ↔ x ∈ X.basicOpen f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ X.residue x ≫ (residueFieldCongr ⋯).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x₁ : ↥X
⊢ residueFieldMap f x₁ ≫ (residueFieldCongr ⋯).hom = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x₁

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Set.range ⇑(X.fromSpecResidueField x) = {x}

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }

Tactic:
simp

Goal state after:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ x✝¹ = x✝ ∧ y✝¹ = y✝ ∧ s✝¹ = s✝
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: case mp
K : Type u_1
inst✝ : Field K
X : Scheme
f₁ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ ∃ (e : f₁.fst = f₁.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₁.snd

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range ⇑(↑U ⊓ ↑V).ι ⊆ ↑↑V

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ U.1 ∩ Set.range ⇑(X.basicOpen r).ι = ↑(U ⊓ X.basicOpen r)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y)
          ⋯ ≫
        pullback.fst f g)
      p =
    T.x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y)
          ⋯ ≫
        pullback.snd f g)
      p =
    T.y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case ex
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (ofPoint (T.SpecTensorTo p)).x = T.x

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case ey
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (ofPoint (T.SpecTensorTo p)).y = T.y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ ↑i ≤ ↑i ⊓ ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑i ⊓ ↑i)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑↑i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯) =
    I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ ((pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
            (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
          pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1 =
    ((pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
          I.glueDataT i j) ≫
        pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      I.glueDataObjι (j, i).1

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mp
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ ∃ (e : T₁.fst = T₁.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₁.snd

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ ↑↑⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (pullback.fst f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.x ∧ (pullback.snd f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.y

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ ∃ y, g y = (pullback.snd f g ≫ g) a

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀.h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑j).ι =
    pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (↑i).ι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
a : ↥(pullback f g)
⊢ ∃ y, f y = (pullback.fst f g ≫ f) a

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) =
    𝟙 (pullback (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))

Tactic:
apply pullback.hom_ext
      · rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
        rw [pullback.condition_assoc (f := I.glueDataObjι i)]
        simp
      · rw [← cancel_mono (Scheme.Opens.ι _)]
        simp [pullback.condition_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↥X
this : CompactSpace ↥X
i : ↑s
⊢ Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤ = PrimeSpectrum.basicOpen ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.fst f g ≫ i₁) t = (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.fst f' g') t

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
t : ↥(pullback f g)
⊢ (pullback.snd f g ≫ i₂) t = (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.snd f' g') t

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑U ⊓ ↑V)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑↑U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this : IsIso (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑U ⊓ ↑V)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ((I.glueDataObjIso U).hom ≫ I.gluedTo ∣_ ↑U) ≫ (↑U).ι = I.glueDataObjι U ≫ (↑U).ι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.subschemeCover.f U ''ᵁ ⊤ = I.subschemeι ⁻¹ᵁ ↑U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.subschemeι ⁻¹ᵁ ↑U = I.subschemeCover.f U ''ᵁ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ glueDataObjHom ⋯ U ≫ I.glueDataObjι U = 𝟙 (I.glueDataObj U) ≫ I.glueDataObjι U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
hIJ : I ≤ J
hJK : J ≤ K
U : ↑X.affineOpens
⊢ (glueDataObjHom hJK U ≫ glueDataObjHom hIJ U) ≫ I.glueDataObjι U = glueDataObjHom ⋯ U ≫ I.glueDataObjι U

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
x✝ : J.subschemeCover.openCover.I₀
⊢ J.subschemeCover.openCover.f x✝ ≫ inclusion h ≫ I.subschemeι = J.subschemeCover.openCover.f x✝ ≫ J.subschemeι

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝ : I.subschemeCover.openCover.I₀
⊢ I.subschemeCover.openCover.f x✝ ≫ inclusion ⋯ = I.subschemeCover.openCover.f x✝ ≫ 𝟙 I.subscheme

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
h₁ : I ≤ J
h₂ : J ≤ K
x✝ : K.subschemeCover.openCover.I₀
⊢ K.subschemeCover.openCover.f x✝ ≫ inclusion h₂ ≫ inclusion h₁ = K.subschemeCover.openCover.f x✝ ≫ inclusion ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ ↑⟨f ⁻¹ᵁ U, ⋯⟩ ≤ f ⁻¹ᵁ ↑⟨U, hU⟩

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact targetAffineLocally_affineAnd_iff_affineLocally hQ f

Goal state after: