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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop X.toSpecΓ))

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : ↑X.affineOpens
⊢ (I.comap f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) (I.ideal ⟨f ''ᵁ ↑U, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
I : X.IdealSheafData
J : Y.IdealSheafData
f : X ⟶ Y
H : J ≤ I.map f
⊢ Hom.ker J.subschemeι ≤ Hom.ker (I.subschemeι ≫ f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.snd f I.subschemeι = (I.comap f).subschemeMap I f ⋯

Tactic:
by

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

Goal state before:
pp: ⊢ @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsSeparated

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsSeparated

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsSeparated

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsSeparated

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : IsSeparated f
⊢ IsSeparated (Scheme.Hom.resLE f V U e)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
⊢ x ∈ U.carrier ∧ f x = f x

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
⊢ IsSeparated (Spec.map f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
⊢ IsSeparated f

Tactic:
by

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

Goal state before:
pp: case h₀
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv) ≫ pullback.fst (f ≫ g) (𝟙 Y ≫ g) =
    pullback.mapDesc f (𝟙 Y) g ≫ pullback.fst (f ≫ g) (𝟙 Y ≫ g)

Tactic:
simp [pullback.condition]

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

Goal state before:
pp: case h₁
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ ((pullback.fst f (𝟙 Y) ≫ pullback.lift (𝟙 X) f ⋯) ≫ (pullback.congrHom ⋯ ⋯).inv) ≫ pullback.snd (f ≫ g) (𝟙 Y ≫ g) =
    pullback.mapDesc f (𝟙 Y) g ≫ pullback.snd (f ≫ g) (𝟙 Y ≫ g)

Tactic:
simp [pullback.condition]

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
i : 𝒰.I₀
⊢ W i ≤ 𝒰.f i ⁻¹ᵁ U

Tactic:
by

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated g
⊢ IsClosedImmersion (pullback.lift (𝟙 X) f ⋯)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ f ((pullback.fst f f) x) = f ((pullback.snd f f) x)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ W i ≤ 𝒰.f i ⁻¹ᵁ ⊤

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Set.range ⇑f ⊆ Set.range ⇑(coborderRange f).ι

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
⊢ liftCoborder f ⁻¹ᵁ U = f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(Scheme.Hom.coborderRange f)).Opens
⊢ Scheme.Hom.app (Scheme.Hom.liftCoborder f) U =
    Scheme.Hom.app f ((Scheme.Hom.coborderRange f).ι ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑f ⊆ Set.range ⇑(Scheme.Hom.coborderRange f).ι

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsDominant (Scheme.Hom.coborderRange f).ι

Tactic:
by

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

Goal state before:
pp: ⊢ @IsImmersion = @IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f ↦ IsLocallyClosed (Set.range f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
⊢ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @IsImmersion

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : IsImmersion f
hg : IsImmersion g
⊢ IsImmersion (f ≫ g)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))
⊢ FinitePresentation R S

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsClosedImmersion e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
⊢ FiniteType R S

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ g' ≫ f = (f' ≫ Scheme.Hom.liftCoborder g) ≫ (Scheme.Hom.coborderRange g).ι

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Y' S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → IsImmersion g → IsImmersion g'

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : IsImmersion f
⊢ IsImmersion (Scheme.Hom.resLE f V U e)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f✝ f : X ⟶ Y
inst✝ : IsImmersion f
⊢ LocallyOfFiniteType f

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (pullback.diagonal f)

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsImmersion (prod.lift (𝟙 X) (𝟙 X))

Tactic:
by

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsImmersion (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ Hom.liftCoborder f ≫ (Hom.coborderRange f).ι = Hom.toImage f ≫ Hom.imageι f

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.f i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↥X
hfopen : IsOpenMap ⇑f
hfinj₁ : Function.Injective ⇑f
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↥X
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
res : (i : 𝒰.I₀) → Γ(X, ⊤) ⟶ Γ(𝒰.X i, ⊤) := fun i ↦ Scheme.Hom.appTop (𝒰.f i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : f x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑f '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.I₀) → Opens ↥(𝒰.X i) :=
  fun i ↦ (𝒰.X i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.I₀), W i ≤ 𝒰.f i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.f i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
i : 𝒰.I₀
⊢ ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ IsPullback (Hom.toImage f) (Hom.liftCoborder f) (Hom.imageι f) (Hom.coborderRange f).ι

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
⊢ ∀ a ∈ I, f a = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ StableUnderComposition @FinitePresentation

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ (ker e.toRingHom).FG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ IsStableUnderBaseChange @FinitePresentation

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ HoldsForLocalizationAway @FinitePresentation

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), ((algebraMap S (Localization.Away ↑r)).comp f).FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: ⊢ OfLocalizationSpanTarget @FinitePresentation

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
C : BasicConstructibleSetData R
⊢ map (RingHom.id R) C = C

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ map (RingHom.id R) = id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
φ : S →+* T
ψ : R →+* S
C : BasicConstructibleSetData R
⊢ map (φ.comp ψ) C = map φ (map ψ C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
φ : S →+* T
ψ : R →+* S
⊢ map (φ.comp ψ) = map φ ∘ map ψ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : R →+* S
C : BasicConstructibleSetData R
⊢ (map φ C).toSet = comap φ ⁻¹' C.toSet

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : ConstructibleSetData R
⊢ map (RingHom.id R) s = s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : R →+* S
s : ConstructibleSetData R
⊢ map (f.comp g) s = map f (map g s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ (map f s).toSet = comap f ⁻¹' s.toSet

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
S : ConstructibleSetData R
⊢ IsConstructible S.toSet

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := ⋯
A : Type u_1 := ⋯
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := ⋯
hf' : Function.Surjective ⇑f'
t : Finset A := ⋯
⊢ (Ideal.Quotient.mk I) (∑ g, g' g * h' g) - 1 = 0

Tactic:
← map_one (Ideal.Quotient.mk I),

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g ↦ (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ (Ideal.Quotient.mk I) (∑ g, g' g * h' g) - (Ideal.Quotient.mk I) 1 = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ S, S.toSet = s) ↔ IsConstructible s

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
⊢ Set.range ⇑(pullback.diagonal f) ⊆ ↑(diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
by

Goal state after: