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

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
obtain ⟨n, e⟩ := (hU.isLocalization_basicOpen f).exists_of_eq _ H

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n : ℕ
e :
  ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁ =
    ↑⟨(fun x ↦ (f |_ ↑S) ⋯ ^ x) n, ⋯⟩ * (((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂
m : ℕ
hm : n ≤ m
⊢ (((f |_ U₁) ⋯ ^ (m - n + n + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m - n + n + n₁) * y₂) |_ ↑S) h₂

Tactic:
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply,
    pow_add, map_pow, map_mul, mul_assoc, ← Functor.map_comp, ← op_comp, homOfLE_comp,
    ← CommRingCat.comp_apply] at e ⊢

Goal state after:
case h
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
n m : ℕ
hm : n ≤ m
e :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂)
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₂ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₁).op)) y₁)) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ (m - n) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n₁ *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE h₂).op)) y₂))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
K : Ideal R
⊢ K ∈ hS.toFinset → ¬I ≤ K

Tactic:
hK

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
K : Ideal R
hK : K ∈ hS.toFinset
⊢ ¬I ≤ K
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
this : ∃ a ∈ ↑I, a ∉ ⋃ K ∈ hS.toFinset, ↑K
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height

Tactic:
Set.mem_iUnion,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
this : ∃ a ∈ ↑I, ¬∃ i, ∃ (_ : i ∈ hS.toFinset), a ∈ ↑i
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑(r + 1) ∧ ↑(r + 1) ≤ J.height
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), IsOpen ↑s

pp: case inst
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), QuasiSober ↑↑s

pp: case hS'
X : Scheme
⊢ (⋃₀ Set.range fun x ↦ Set.range ⇑(X.affineCover.f x)) = ⊤

Tactic:
· rintro ⟨_, i, rfl⟩; exact (X.affineCover.f i).isOpenEmbedding.isOpen_range

Goal state after:
case inst
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), QuasiSober ↑↑s

case hS'
X : Scheme
⊢ (⋃₀ Set.range fun x ↦ Set.range ⇑(X.affineCover.f x)) = ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑V
i : ι
hi : x ∈ ↑(U i)
⊢ ∃ i r rU, X.basicOpen r = X.basicOpen rU ∧ ↑⟨x, hxV⟩ ∈ X.basicOpen r

Tactic:
exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩

Goal state after:
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)
⊢ supportSet = ⋂ U, X.zeroLocus ↑(ideal U)

Tactic:
by
    let I' : X.IdealSheafData := { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen }
    change supportSet = I'.supportSet
    ext x
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
    exact (supportSet_inter ⟨U, hU⟩ x hxU).trans
      (I'.mem_support_iff_of_mem (U := ⟨U, hU⟩) hxU).symm

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ IsIso f

Tactic:
← isomorphisms.iff,

Goal state after:
R S : CommRingCat
f : R ⟶ S
h : IsIso (Spec.map f)
⊢ isomorphisms CommRingCat f
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) := ⋯
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ≤
    PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

Tactic:
rw [Ideal.map_le_iff_le_comap]

Goal state after:
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
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z) ≤
    Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
        Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Tactic:
rw [← cancel_mono <| Y.fromSpecResidueField T.y]

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ((Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
          Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom) ≫
        Spec.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ : ↥(Spec T.tensor)
T' : Triplet f g
snd✝ : ↥(Spec T'.tensor)
⊢ (∃ (e : ⟨T, snd✝¹⟩.fst = ⟨T', snd✝⟩.fst), (Spec.map (Triplet.tensorCongr e).inv) ⟨T, snd✝¹⟩.snd = ⟨T', snd✝⟩.snd) →
    ⟨T, snd✝¹⟩ = ⟨T', snd✝⟩

Tactic:
rintro ⟨rfl : T = T', e⟩

Goal state after:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
snd✝¹ snd✝ : ↥(Spec T.tensor)
e : (Spec.map (Triplet.tensorCongr ⋯).inv) ⟨T, snd✝¹⟩.snd = ⟨T, snd✝⟩.snd
⊢ ⟨T, snd✝¹⟩ = ⟨T, snd✝⟩
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) = ⊤
⊢ IsAffine X

Tactic:
apply isAffine_of_isAffineOpen_basicOpen _ hS

Goal state after:
case of_basicOpenCover
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS' : ∀ (r : ↥S), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r)
hS : Ideal.span (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S) = ⊤
⊢ ∀ i ∈ ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) '' ↑S, IsAffineOpen (X.basicOpen i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
have := I.subschemeCover_map_subschemeι U
  simp only [glueDataObjι, Category.assoc, IsAffineOpen.isoSpec_inv_ι] at this
  replace this := Scheme.Hom.congr_app this U
  simp only [Hom.comp_base, TopologicalSpace.Opens.map_comp_obj, Hom.comp_app,
    IsAffineOpen.fromSpec_app_self, eqToHom_op, Category.assoc, Hom.naturality_assoc,
    TopologicalSpace.Opens.map_top, ← ΓSpecIso_inv_naturality_assoc] at this
  simp_rw [← Category.assoc, ← IsIso.comp_inv_eq] at this
  simp only [← this, ← Functor.map_inv, inv_eqToHom, Category.assoc, eqToHom_unop,
    ← Functor.map_comp, IsIso.Iso.inv_inv, subschemeObjIso, Iso.trans_inv, Functor.mapIso_inv,
    Iso.op_inv, eqToIso.inv, eqToHom_op, Iso.hom_inv_id_assoc, Hom.appIso_inv_naturality_assoc,
      Functor.op_map, unop_comp, unop_inv, Quiver.Hom.unop_op,
    Hom.app_appIso_inv_assoc, TopologicalSpace.Opens.carrier_eq_coe, TopologicalSpace.Opens.map_coe,
    homOfLE_leOfHom]
  convert! (Category.comp_id _).symm
  exact CategoryTheory.Functor.map_id _ _

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

Goal state before:
pp: case pos
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∃ U, f x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen

Goal state after:
case pos
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, f x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
⊢ ∀ (x y : J.subschemeCover.openCover.I₀),
    pullback.fst (J.subschemeCover.openCover.f x) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h x ≫ I.subschemeCover.f x =
      pullback.snd (J.subschemeCover.openCover.f x) (J.subschemeCover.openCover.f y) ≫
        glueDataObjHom h y ≫ I.subschemeCover.f y

Tactic:
intro U V
    simp only [← cancel_mono I.subschemeι, AffineOpenCover.openCover_X, glueDataObjHom_ι_assoc,
      AffineOpenCover.openCover_f, Category.assoc, subschemeCover_map_subschemeι]
    rw [← subschemeCover_map_subschemeι, pullback.condition_assoc, subschemeCover_map_subschemeι]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ DenseRange ⇑(Hom.toImage f)

Tactic:
by
    rw [denseRange_iff_closure_range, f.imageι.isEmbedding.closure_eq_preimage_closure_image,
      ← Set.univ_subset_iff, ← Set.image_subset_iff, Set.image_univ,
      IdealSheafData.range_subschemeι, Hom.support_ker, ← Set.range_comp,
      ← TopCat.coe_comp, ← Scheme.Hom.comp_base, f.toImage_imageι]

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

Goal state before:
pp: R✝ S✝ : Type u_5
inst✝² : CommRing R✝
inst✝¹ : CommRing S✝
inst✝ : Algebra R✝ S✝
s : Set R✝
hs : Ideal.span s = ⊤
h : ∀ r ∈ s, (algebraMap (Localization.Away r) (Localization.Away r ⊗[R✝] S✝)).FiniteType
⊢ (algebraMap R✝ S✝).FiniteType

Tactic:
simp_rw [finiteType_algebraMap] at h ⊢

Goal state after:
R✝ S✝ : Type u_5
inst✝² : CommRing R✝
inst✝¹ : CommRing S✝
inst✝ : Algebra R✝ S✝
s : Set R✝
hs : Ideal.span s = ⊤
h : ∀ r ∈ s, Algebra.FiniteType (Localization.Away r) (Localization.Away r ⊗[R✝] S✝)
⊢ Algebra.FiniteType R✝ S✝
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
S : P.CostructuredArrow ⊤ Scheme.Spec X
q : ↥(Spec (unop (F.obj S)))
U : Opens ↥X
hU : U ∈ X.affineOpens
hqU : S.hom q ∈ ↑U
f : ↑(unop S.left)
hqf : q ∈ ↑(PrimeSpectrum.basicOpen f)
hfU : ↑(PrimeSpectrum.basicOpen f) ⊆ ↑(S.hom ⁻¹ᵁ U)
this : LocallyOfFiniteType S.hom
⊢ ∃ f, q ∈ PrimeSpectrum.basicOpen f ∧ Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen f)

Tactic:
exact ⟨f, hqf, _, ⟨U, rfl⟩, S.hom.appLE _ _ hfU,
        (S.hom.finiteType_appLE hU (.Spec_basicOpen _)) _⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0

Tactic:
nontriviality R
  rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion (Scheme.IdealSheafData.inclusion h ≫ I.subschemeι)

Tactic:
simp only [Scheme.IdealSheafData.inclusion_subschemeι]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
I J : X.IdealSheafData
h : I ≤ J
⊢ IsClosedImmersion J.subschemeι
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
← mem_image_comap_zeroLocus_sdiff f ∅ x,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ x ∈ comap (algebraMap R A) '' (zeroLocus ∅ \ zeroLocus {f})
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
· rw [IsAffineOpen.range_fromSpec]
      exact Set.inter_subset_left

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)

Tactic:
have : IsReduced (Y.affineCover.X i) := isReduced_of_isOpenImmersion (Y.affineCover.f i)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : IsLocallyNoetherian Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
this : IsReduced (Y.affineCover.X i)
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ S
g : Y ⟶ S
pX : Z ⟶ X
pY : Z ⟶ Y
H : IsPullback pX pY f g
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
⊢ IsSchemeTheoreticallyDominant pY

Tactic:
by
  rw [← H.isoPullback_hom_snd]
  infer_instance

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

Goal state before:
pp: case convert_6
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.HasGoingDown ↑R ↑S

Tactic:
Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap

Goal state after:
case convert_6
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap ↑R ↑S))
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, True

Tactic:
and_true

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
z : X
hz : z ∈ U
⊢ ∃ t, t ∈ 𝓝 z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommMonoid Y
ι : Type u_3
s : Finset ι
F : ι → locallyFinsuppWithin U Y
⊢ ⇑(∑ n ∈ s, F n) = ∑ n ∈ s, ⇑(F n)

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp_all
  | insert => simp_all

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

Goal state before:
pp: case refine_2
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
⊢ UX ≤ iSup D.obj

Tactic:
· subst hVU; exact iSup_le_iff.mpr fun i ↦ le_iSup D.obj (.single i)

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
⊢ ∀ (a : locallyFinsuppWithin U Y), a ≤ a

Tactic:
by simp [le_def]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ max (n • f x) 0 = n • max (f x) 0

Tactic:
by_cases h : f x < 0

Goal state after:
case pos
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : f x < 0
⊢ max (n • f x) 0 = n • max (f x) 0

case neg
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
h : ¬f x < 0
⊢ max (n • f x) 0 = n • max (f x) 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx :
  (ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
      ((algebraMap ↑R ↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x) =
    0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0

Tactic:
elementwise_of% StructureSheaf.algebraMap_germ

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
x : ↑R
s : ↥(Submonoid.powers f)
hx : (ConcreteCategory.hom (StructureSheaf.toStalk (↑R) p)) x = 0
⊢ IsLocalization.mk' (↑((Spec.structureSheaf ↑R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f)))) x s = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
rw [← cancel_mono V.toScheme.isoSpec.hom]

Goal state after:
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ (↑V).isoSpec.hom = Scheme.Hom.resLE g V U ⋯ ≫ (↑V).isoSpec.hom