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

Goal state before:
pp: case refine_1
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' := ⋯ })
⊢ { carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ } = ⊥

Tactic:
ext x

Goal state after:
case refine_1
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 ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) ↔ x ∈ ↑⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsDomain ↑R
⊢ IrreducibleSpace ↥(Spec R)

Tactic:
by
  convert! PrimeSpectrum.irreducibleSpace (R := R)

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.supportSet ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
ext x

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
⊢ x ∈ I.supportSet ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ supportSet = I'.supportSet

Tactic:
ext x

Goal state after:
X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet
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
⊢ ⇑f '' U = (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
ext x

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 ∈ ⇑f '' U ↔ x ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U).topIso.hom ≫ φ = X.presheaf.map (eqToHom ⋯).op ≫ φ

Tactic:
simp only [Scheme.Opens.topIso_hom]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(↑U).ι '' (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) =
    X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
← Set.image_comp,

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

Goal state before:
pp: case a
X : Scheme
I✝ : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
I : Ideal ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (⇑(CommRingCat.Hom.hom F) '' ↑I))
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I))

Tactic:
rwa [← PrimeSpectrum.zeroLocus_span, ← Ideal.map, vanishingIdeal_zeroLocus_eq_radical,
          ← RingHom.algebraMap_toAlgebra (X.presheaf.map _).hom,
          ← IsLocalization.map_radical (.powers f), ← vanishingIdeal_zeroLocus_eq_radical] at hx

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 ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V

Tactic:
X.homOfLE_ι

Goal state after:
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 ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ (↑U ⊓ ↑V).ι) ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (stalkClosedPointIso R).inv = StructureSheaf.toStalk (↑R) (closedPoint ↑R)

Tactic:
ext x

Goal state after:
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↑R
⊢ (CommRingCat.Hom.hom (stalkClosedPointIso R).inv) x =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R) (closedPoint ↑R))) x
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 ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V

Tactic:
X.homOfLE_ι

Goal state after:
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 ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
this : ∀ (U : ↑Y.affineOpens), (⋃ i, ↑(ker (𝒰.f i ≫ f)).support) ∩ ↑↑U = ↑f.ker.support ∩ ↑↑U
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
ext x

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
this : ∀ (U : ↑Y.affineOpens), (⋃ i, ↑(ker (𝒰.f i ≫ f)).support) ∩ ↑↑U = ↑f.ker.support ∩ ↑↑U
x : ↥Y
⊢ x ∈ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support ↔ x ∈ ↑f.ker.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
ext x

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
x : ↑Γ(↑U, ↑V)
⊢ x ∈ (Hom.ker (f ∣_ U)).ideal V ↔ x ∈ f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
ext x

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
⊢ x ∈ (Hom.ker f').ideal W ↔
    x ∈ Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(pullback.fst f g) = ⇑f ⁻¹' Set.range ⇑g

Tactic:
ext x

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥X
⊢ x ∈ Set.range ⇑(pullback.fst f g) ↔ x ∈ ⇑f ⁻¹' Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(pullback.snd f g) = ⇑g ⁻¹' Set.range ⇑f

Tactic:
ext x

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x : ↥Y
⊢ x ∈ Set.range ⇑(pullback.snd f g) ↔ x ∈ ⇑g ⁻¹' Set.range ⇑f
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:
X.homOfLE_ι

Goal state after:
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 ⋯) ≫ (↑i ⊓ ↑j).ι
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
X.homOfLE_ι

Goal state after:
case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑k).ι =
    pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ (↑i ⊓ ↑k).ι
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ⇑(I.subschemeIso.hom ≫ I.gluedTo) = Subtype.val

Tactic:
ext x

Goal state after:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
⊢ (I.subschemeIso.hom ≫ I.gluedTo) x = ↑x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ (Hom.ker f).ideal U ≤
    RingHom.ker (CommRingCat.Hom.hom ((ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)))

Tactic:
by
  let e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(Limits.pullback (C := Scheme) f U.1.ι, ⊤) :=
    X.presheaf.mapIso (eqToIso (by simp [Scheme.Hom.opensRange_pullbackFst])).op
      ≪≫ (Limits.pullback.fst (C := Scheme) f U.1.ι).appIso ⊤
  have he : f.app U ≫ e.hom =
      (ΓSpecIso Γ(Y, ↑U)).inv ≫ (pullback.snd f U.1.ι ≫ U.1.toSpecΓ).appTop := by
    rw [← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop, Category.assoc, Iso.eq_inv_comp]
    simp only [Opens.topIso_hom, eqToHom_op, Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom,
      Iso.op_hom, eqToIso.hom, Hom.appIso_hom, Hom.appLE_map, Hom.map_appLE, Hom.appLE_comp_appLE,
      Opens.map_top, e, pullback.condition, IsAffineOpen.toSpecΓ_isoSpec_inv, Category.assoc]
    rw [Hom.comp_appLE, Opens.ι_app]
    exact Hom.map_appLE _ _ (homOfLE le_top).op
  rw [← he]
  refine (IdealSheafData.ideal_ofIdeals_le _ _).trans_eq
    (RingHom.ker_equiv_comp _ e.commRingCatIsoToRingEquiv).symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom (pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
by
  refine congr($(HasAffineProperty.eq_targetAffineLocally
    (.diagonal @IsAffineHom)) f).to_iff.trans ?_
  simp only [targetAffineLocally, diagonal_isAffine_iff_forall_isAffineOpen_inf,
    (IsOpenImmersion.opensEquiv (f ⁻¹ᵁ _).ι).forall_congr_left, Scheme.affineOpens,
    Subtype.forall, Set.mem_ofPred_eq, Scheme.Opens.opensRange_ι, ← Scheme.Hom.preimage_inf,
    IsOpenImmersion.opensEquiv_symm_apply, Scheme.Hom.image_preimage_eq_opensRange_inf,
    ← Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (Scheme.Opens.ι _)]
  congr! with U hU V₁ hV₁ V₂ hV₂
  rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]

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

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderSpecialization s
hs' : IsConstructible s
⊢ IsClosed s

Tactic:
obtain ⟨S, _, f, rfl⟩ := exists_range_eq_of_isConstructible hs'
  exact isClosed_range_of_stableUnderSpecialization _ hs

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

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
⊢ comap (algebraMap A (A ⊗[K] B)) '' ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) =
    comap (algebraMap A (A ⊗[K] ↥B')) '' ↑(basicOpen f)

Tactic:
ext x

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
⊢ x ∈ comap (algebraMap A (A ⊗[K] B)) '' ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) ↔
    x ∈ comap (algebraMap A (A ⊗[K] ↥B')) '' ↑(basicOpen f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
⊢ LocallyOfFiniteType f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation] at hf
  rw [HasRingHomProperty.eq_affineLocally @LocallyOfFiniteType]
  refine affineLocally_le (fun hf ↦ ?_) f hf
  exact RingHom.FiniteType.of_finitePresentation hf

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

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ Set.range Subtype.val =
    Subtype.val ''
      ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
        ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
← Set.image_comp,

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ Set.range Subtype.val =
    Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
      ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ Set.range Subtype.val =
    Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
      ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
← Set.image_comp,

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ Set.range Subtype.val =
    (Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i)))) ∘ ⇑(Cover.pullbackHom Y.affineCover f i) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) =
    (zeroLocus
        ↑(Finset.image
            (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
            (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
ext x

Goal state after:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
⊢ QuasiCompact f

Tactic:
apply quasiCompact_iff_forall_isAffineOpen.mpr

Goal state after:
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
wlog hU : IsAffineOpen U generalizing U; swap
  · rw [RingHom.injective_iff_ker_eq_bot, ← f.ker_apply ⟨U, hU⟩, f.ker_eq_bot]
    simp
  rw [injective_iff_map_eq_zero]
  intro s hs
  refine Y.IsSheaf.section_ext fun x hx ↦ ?_
  obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ U⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open hx U.isOpen
  refine ⟨V, hVU, hxV, this V hV ?_⟩
  rw [← ConcreteCategory.comp_apply, f.naturality]
  simp [hs]

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Mono (pushoutSection ⋯ hVU ⋯ ⋯)
⊢ x ∈ ⊥

Tactic:
rw [@ConcreteCategory.mono_iff_injective_of_preservesPullback] at this

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ x ∈ ⊥
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyIrreducible x✝ ↔ geometrically (fun x ↦ IrreducibleSpace ↥x) x✝

Tactic:
exact geometricallyIrreducible_iff _

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

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact

Tactic:
← universally_eq_iff (P := @QuasiCompact).mpr inferInstance,

Goal state after:
⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ universally @QuasiCompact