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

Goal state before:
pp: case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
⊢ ∀ (U : ι → X.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
        stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
U

Goal state after:
case of_sSup_eq_top
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
this : (stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P).RespectsIso := stalkwise_respectsIso hP
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → X.Opens
⊢ iSup U = ⊤ →
    (∀ (i : ι), stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) ((U i).ι ≫ f)) →
      stalkwise (fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X : Scheme
H : ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
⊢ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
U

Goal state after:
case mp
X : Scheme
H : ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
U : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
⊢ ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)

Tactic:
U

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
U : Set ↥Y
⊢ IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
V : ↑s
⊢ ↑↑V ⊓ X.basicOpen f ∈ X.affineOpens

Tactic:
by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _

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

Goal state before:
pp: case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)
U : ↑X.affineOpens
r : ↑↑s
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)

Tactic:
simp_rw [sourceAffineLocally_morphismRestrict] at hs'

Goal state after:
case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
U : ↑X.affineOpens
r : ↑↑s
hs' :
  ∀ (r : ↥s) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen ↑r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen ↑r) (↑V) e))
⊢ P (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯)) ↑r)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
⊢ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
U

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U : ↑X.affineOpens
⊢ ∀ (V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : ↑Y.affineOpens
V₁ V₂ : ↑X.affineOpens
hx₁ : x ∈ ↑V₁
hx₂ : x ∈ ↑V₂
e₂ : ↑V₂ ≤ f ⁻¹ᵁ ↑U₂
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂))
hfx₁ : f x ∈ ↑U₁
r : ↑Γ(Y, ↑U₁)
r' : ↑Γ(Y, ↑U₂)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : f x ∈ Y.basicOpen r
ha : IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r'))
⊢ x ∈ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f (↑U₂) (↑V₂) e₂)) r')

Tactic:
simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)

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

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
S : X.Opens
hS : IsCompact S.carrier
⊢ ∀ (U : ↑X.affineOpens),
    (IsQuasiSeparated S.carrier →
        ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
          ∃ n y,
            (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
      IsQuasiSeparated (S ⊔ ↑U).carrier →
        ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
          ∃ n y,
            (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
              (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x

Tactic:
U

Goal state after:
case refine_2
X : Scheme
U✝ : X.Opens
hU : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
⊢ (IsQuasiSeparated S.carrier →
      ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
        ∃ n y,
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x) →
    IsQuasiSeparated (S ⊔ ↑U).carrier →
      ∀ (f : ↑Γ(X, S ⊔ ↑U)) (x : ↑Γ(X, X.basicOpen f)),
        ∃ n y,
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
            (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

Tactic:
by_cases I_top : I = ⊤

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsPrime), i'.height
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)
⊢ I ≤ J

Tactic:
intro V
  have : ∀ x : V.1, ∃ (i : ι) (r : Γ(X, V.1)) (rU : Γ(X, U i)),
      X.basicOpen r = X.basicOpen rU ∧ x.1 ∈ X.basicOpen r := by
    intro ⟨x, hxV⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))
    exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩
  choose i r rU e hxr using this
  have : Ideal.span (Set.range r) = ⊤ := by
    rw [← V.2.self_le_iSup_basicOpen_iff]
    exact fun x hxV ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨_, _, rfl⟩, hxr ⟨x, hxV⟩⟩
  have inst := V.2.isLocalization_basicOpen
  refine Submodule.le_of_isLocalized_span _ this (fun i ↦ Γ(X, X.basicOpen i.1))
    (fun i ↦ Algebra.linearMap Γ(X, V.1) Γ(X, X.basicOpen i.1)) ?_
  rintro ⟨_, j, rfl⟩
  simp only [← Submodule.restrictScalars_localized' Γ(X, X.basicOpen (r j)),
    Ideal.localized'_eq_map, RingHom.algebraMap_toAlgebra]
  erw [I.map_ideal (U := ⟨_, V.2.basicOpen _⟩) (X.basicOpen_le (r j)),
    J.map_ideal (U := ⟨_, V.2.basicOpen _⟩) (X.basicOpen_le (r j))]
  delta algebra_section_section_basicOpen
  rw! [e]
  rw [← I.map_ideal (V := (U _)) (X.basicOpen_le _), ← J.map_ideal (V := (U _)) (X.basicOpen_le _)]
  exact Ideal.map_mono (f := (X.presheaf.map (homOfLE (X.basicOpen_le (rU j))).op).hom) (H (i j))

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

Goal state before:
pp: case e'
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
· intro R S _ _ f
      exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm

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

Goal state before:
pp: case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ IsOpenImmersion (Spec.map f) → ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
intro H
    obtain ⟨e, he, he'⟩ := PrimeSpectrum.isClopen_iff_zeroLocus.mp
      ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf,
        (Spec.map f).isOpenEmbedding.isOpen_range⟩
    refine ⟨e, he, ?_⟩
    let φ : R ⟶ _ := (CommRingCat.ofHom (Ideal.Quotient.mk (.span {e})))
    have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
    have H : Set.range (Spec.map φ) = Set.range (Spec.map f) :=
      ((range_comap_of_surjective _ _
        Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
    let i : S ≅ .of _ := (Scheme.Spec.preimageIso
      (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
    have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
    have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
    rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi,
      ← RingHom.ker_eq_comap_bot]
    simp [φ]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
hX : ∀ (x : ↥X), ∃ U i, ∃ (x_1 : IsOpenImmersion i), x ∈ Scheme.Hom.opensRange i ∧ IsOpenImmersion (i ≫ f)
⊢ IsOpenImmersion f

Tactic:
choose U i _ hxi hi using hX

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
U : ↥X → Scheme
i : (x : ↥X) → U x ⟶ X
x✝ : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ IsOpenImmersion f
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: ⊢ HasAffineProperty (isomorphisms Scheme) fun X x f x_1 ↦ IsAffine X ∧ IsIso (Scheme.Hom.appTop f)

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget (isomorphisms Scheme) with X Y f hY

Goal state after:
case e'_2
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsAffine X ∧ IsIso (Scheme.Hom.appTop f) ↔ AffineTargetMorphismProperty.of (isomorphisms Scheme) f
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec = Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁

Tactic:
rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

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

Goal state before:
pp: case refine_1
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 ∈
    RingHom.ker
      (CommRingCat.Hom.hom ((ΓSpecIso Γ(X, ↑V)).inv ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)))

Tactic:
simp only [Hom.comp_app, Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
      TopologicalSpace.Opens.map_top, homOfLE_app, homOfLE_leOfHom, Category.assoc, RingHom.mem_ker]

Goal state after:
case refine_1
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
⊢ (CommRingCat.Hom.hom
        ((ΓSpecIso Γ(X, ↑V)).inv ≫
          Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫ X.presheaf.map (homOfLE ⋯).op ≫ Hom.app F ⊤))
      x =
    0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑I.support ∩ ↑↑U = ↑↑U ∩ ↑I.support

Tactic:
Set.inter_comm

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ↑↑U ∩ ↑I.support = ↑↑U ∩ ↑I.support
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

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 = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
⊢ FiniteType R S

Tactic:
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)

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 = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
⊢ FiniteType R S
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mpr
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 : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
U

Goal state after:
case mpr
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 : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
U : Y.Opens
⊢ IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ W) f

Tactic:
U

Goal state after:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f
U : ↑Y.affineOpens
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ W) (f ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)

Tactic:
ext X Y f
    rw [targetAffineLocally_affineAnd_iff hQi, h f]
    aesop

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

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
⊢ ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
U

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U : X.Opens
⊢ ∀ (V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso f

Tactic:
suffices h : IsIso f'.op by
    rwa [isIso_op_iff, ← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),
      ← isIso_iff_of_reflects_iso _ (Over.forget _)] at h

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h True.intro
⊢ IsIso f'.op
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)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ∃ y,
    (pullback.map ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) f f
          ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
        y =
      x

Tactic:
change x ∈ Set.range _

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    Set.range
      ⇑(pullback.map ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) f f
          ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∈ zeroLocus s

Tactic:
by simpa [Set.subset_def]

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

Goal state before:
pp: case hC
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝
      (((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp
          C)
        x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)

pp: case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Tactic:
· simp [scalarRTensorAlgEquiv, e, Algebra.smul_def]

Goal state after:
case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ ↑↑V ∩ ↑↑U))

Tactic:
Set.inter_comm

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ (↑↑U ∩ ↑↑V)))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsNoetherian X
i : 𝒰.I₀
⊢ IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
apply (isLocallyNoetherian_iff_of_affine_openCover _).mp

Goal state after:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
h : IsNoetherian X
i : 𝒰.I₀
⊢ IsLocallyNoetherian X