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

Goal state before:
pp: case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ (S.carrier ∪ ↑↑V))

Tactic:
rw [Set.inter_union_distrib_left]

Goal state after:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ ↑↑V)
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
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ∈ X.affineOpens

Tactic:
exact V.1.2.basicOpen _

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
eq_affineLocally P,

Goal state after:
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
H : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H : P g
⊢ P (f ≫ g)

Tactic:
eq_affineLocally P,

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) g
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (f ≫ g)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
eq_affineLocally P,

Goal state after:
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
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : p.FiniteHeight
n : ℕ
hn : ↑n = p.height
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.height

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝² : CommRing R
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : p.FiniteHeight
n : ℕ
hn : ↑n = p.primeHeight
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.primeHeight
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height ≤ ringKrullDim R

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.primeHeight ≤ ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I✝ I : Ideal R
inst✝ : FiniteRingKrullDim R
⊢ I.FiniteHeight

Tactic:
rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I✝ I : Ideal R
inst✝ : FiniteRingKrullDim R
⊢ ¬I = ⊤ → ↑I.height < ↑⊤
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I✝ I : Ideal R
inst✝ : FiniteRingKrullDim R
⊢ I.FiniteHeight

Tactic:
rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]
  exact fun h ↦ lt_of_le_of_lt (Ideal.height_le_ringKrullDim_of_ne_top h) ringKrullDim_lt_top

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = 0 ↔ I ∈ minimalPrimes R

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.primeHeight = 0 ↔ I ∈ minimalPrimes R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ↑(maximalIdeal R).height = ringKrullDim R

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ↑(maximalIdeal R).primeHeight = ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ J.height = (comap (algebraMap R A) J).height

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ J.primeHeight = (comap (algebraMap R A) J).height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ J.primeHeight = (comap (algebraMap R A) J).height

Tactic:
Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ J.primeHeight = (comap (algebraMap R A) J).primeHeight
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.ideal V ≤ Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)

Tactic:
rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) =
    PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

Tactic:
let F := X.presheaf.map (homOfLE (X.basicOpen_le f)).op

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

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

Tactic:
rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ

Goal state after:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ f x ∈ ↑(ker f).support

Tactic:
refine ((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ f x ∈ Y.zeroLocus ↑((ker f).ideal ⟨U, hU⟩)
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 (Triplet.tensorCongr ⋯).inv)
      ((fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩) ((fun T ↦ T.fst.SpecTensorTo T.snd) ⟨T, p⟩)).snd =
    ⟨T, p⟩.snd

Tactic:
have : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) (⊥ : PrimeSpectrum _) =
        (⊥ : PrimeSpectrum _) :=
      (PrimeSpectrum.instUnique).uniq _

Goal state after:
case h
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
this : (Spec.map (Hom.residueFieldMap T.SpecTensorTo p)) ⊥ = ⊥
⊢ (Spec.map (Triplet.tensorCongr ⋯).inv)
      ((fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩) ((fun T ↦ T.fst.SpecTensorTo T.snd) ⟨T, p⟩)).snd =
    ⟨T, p⟩.snd
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
· rw [← cancel_mono (Scheme.Opens.ι _)]
        simp [pullback.condition_assoc]

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

Goal state before:
pp: case hs
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
hs :
  Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span ↑s) =
    Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤
⊢ Ideal.span (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) '' ↑s) = ⊤

Tactic:
rwa [Ideal.map_span, Ideal.map_top] at hs

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

pp: X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤

Tactic:
· exact hfU

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↥Y → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_1
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 := ⋯
x✝ : S
r : ↑↑s
x : S
hx : x ∈ ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑r) (t r))
⊢ x ∈ (⋃ x ∈ ↑s.attach, ↑(sf x)) ∪ ↑s ∪ ↑(Finset.image (⇑l) l.support)

Tactic:
exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ IsAffine X) f ↔
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
by
  delta AffineTargetMorphismProperty.diagonal
  constructor
  · intro H U V hU hV
    dsimp at H
    have : IsAffine _ := hU
    have : IsAffine _ := hV
    let g : pullback U.ι V.ι ⟶ X := pullback.fst _ _ ≫ U.ι
    have := IsOpenImmersion.isPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right)
      U.ι V.ι (by simp) (by ext; simp)
    exact .of_isIso this.isoPullback.hom
  · introv H h₁ h₂
    have : IsAffineOpen (pullback.fst f₁ f₂ ≫ f₁).opensRange := by
      convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂)
      exact Opens.ext (IsOpenImmersion.range_pullback_to_base_of_left _ _)
    change IsAffine _ at this
    exact .of_isIso (pullback.fst f₁ f₂ ≫ f₁).isoOpensRange.hom

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

Goal state before:
pp: X Y Z : Scheme
i : Z ⟶ Y
f : X ⟶ Y
inst✝ : IsClosedImmersion i
⊢ Hom.ker (pullback.fst f i) = Hom.ker (pullback.fst f (Hom.ker i).subschemeι)

Tactic:
rw [← Hom.ker_comp_of_isIso (pullback.map f i f i.imageι (𝟙 _) (i.toImage) (𝟙 _)
    (by simp) (by simp)), pullback.lift_fst, Category.comp_id]

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))
⊢ ∀ (g : ↑↑t), (RingHom.ker (Localization.awayMap f.toRingHom ↑g)).FG

Tactic:
intro g

Goal state after:
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))
g : ↑↑t
⊢ (RingHom.ker (Localization.awayMap f.toRingHom ↑g)).FG
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case inr
Y : Scheme
inst✝ : Subsingleton ↥Y
R : CommRingCat
f : Spec R ⟶ Y
g : Y ⟶ Spec R
hg : g ≫ f = 𝟙 Y
this :
  ∀ {Y : Scheme} [Subsingleton ↥Y] (R : CommRingCat) (f : Spec R ⟶ Y) (g : Y ⟶ Spec R),
    g ≫ f = 𝟙 Y → (∃ S, Y = Spec S) → IsClosedImmersion g
hY : ¬∃ S, Y = Spec S
⊢ IsClosedImmersion g

Tactic:
have inst := (Scheme.isoSpec Y).inv.homeomorph.injective.subsingleton
    rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (Scheme.isoSpec Y).inv]
    exact this R (f ≫ (Scheme.isoSpec Y).hom) ((Scheme.isoSpec Y).inv ≫ g)
      (by simp [reassoc_of% hg]) ⟨_, rfl⟩

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

Goal state before:
pp: 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
⊢ e
        ((Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f)) =
      0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
change (e.toAlgHom.toRingHom.comp (Algebra.TensorProduct.comm ..).toRingHom).comp
      (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0

Goal state after:
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
⊢ (((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        f =
      0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := topologically IsOpenMap) X.affineCover]

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
⊢ ∀ (i : X.affineCover.I₀),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
i : 𝒰.I₀
hi₁ : t ∈ (Opens.comap { toFun := comap φ, continuous_toFun := ⋯ }) (Ti i)
hi₂ : p z ∈ U i
⊢ False

Tactic:
rw [comap_basicOpen, show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂), basicOpen_zero] at hi₁

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.I₀ → T.Opens := fun i ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun x ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K := (aeval fun i ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : t' ∈ basicOpen g
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ i ∈ σ, (pullback.fst f q) z ∉ (U i).carrier
i : 𝒰.I₀
hi₁ : t ∈ ⊥
hi₂ : p z ∈ U i
⊢ False
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫ Spec.map (Scheme.Hom.appTop (𝔸(n; S) ↘ S)) ≫ S.isoSpec.inv = 𝔸(n; S) ↘ S

Tactic:
← Scheme.toSpecΓ_naturality_assoc

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S) ↘ S ≫ S.toSpecΓ ≫ S.isoSpec.inv = 𝔸(n; S) ↘ S
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
⊢ ⇑(single x y) = Pi.single x y

Tactic:
ext
  simp [Pi.single_apply]

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

Goal state before:
pp: case refine_2
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
⊢ (e₂.val i).degree.succ < (e.val i).degree.succ

Tactic:
gcongr
      exact degree_map_lt (by simp [q₂, ← hi]) (by simpa [hi] using hc)

Goal state after: