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

Goal state before:
pp: case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R

Goal state after:
case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R : Type u
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R

Goal state after:
case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R : Type u
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)) →
        (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f ↦
    P (Spec.map (CommRingCat.ofHom f))

Tactic:
intro R

Goal state after:
case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
R : Type u
⊢ ∀ ⦃S : Type u⦄ (T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T]
    (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) ((algebraMap S T).comp f)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_3
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
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
⊢ ↑(r + 1) ≤ p.primeHeight

Tactic:
rw [← p.height_eq_primeHeight]

Goal state after:
case succ.refine_3
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
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
⊢ ↑(r + 1) ≤ p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_3
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
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ ↑(r + 1) ≤ (J ⊔ span {x}).height

Tactic:
refine le_iInf₂ (fun p hp ↦ ?_)
      have := hp.isPrime
      rw [← p.height_eq_primeHeight]
      by_cases h : p.height = ⊤
      · exact le_of_le_of_eq le_top h.symm
      have : p.FiniteHeight := ⟨Or.inr h⟩
      have := Ideal.height_mono (le_sup_left.trans hp.le)
      suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
      intro e
      apply hx₂ p
      · refine ⟨mem_minimalPrimes_of_height_le (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case hS
X : Scheme
i : X.affineCover.I₀
⊢ IsOpen ↑⟨(fun x ↦ Set.range ⇑(X.affineCover.f x)) i, ⋯⟩

Tactic:
exact (X.affineCover.f i).isOpenEmbedding.isOpen_range

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
x : ↥(Spec R)
⊢ _root_.IsReduced ↑((Spec R).presheaf.stalk x)

Tactic:
have : _root_.IsReduced (CommRingCat.of <| Localization.AtPrime (PrimeSpectrum.asIdeal x)) := by
    dsimp; infer_instance

Goal state after:
X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
x : ↥(Spec R)
this : _root_.IsReduced ↑(CommRingCat.of (Localization.AtPrime x.asIdeal))
⊢ _root_.IsReduced ↑((Spec R).presheaf.stalk x)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
· intro x y
    rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]
    simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]
    generalize x - y = z
    intro H
    obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU _ _ H
    refine ⟨⟨_, n, rfl⟩, ?_⟩
    simpa [mul_comm z] using! e

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

Goal state after:
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 : Type u
⊢ ∀ {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
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
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
by have := 𝒰.exists_eq x; simp; grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case mpr
X : Scheme
x y : ↥X
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(X.fromSpecStalk x)

Tactic:
rintro (hy : y ⤳ x)
    have := fromSpecStalk_closedPoint (x := y)
    rw [← SpecMap_stalkSpecializes_fromSpecStalk hy] at this
    exact ⟨_, this⟩

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 ⋯)
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V

Tactic:
enter [2]

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 ⋯)
| I.glueDataObjι V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V

Tactic:
enter [2]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| I.glueDataObjι 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
x : ↥Y
⊢ x ∈ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support ↔ x ∈ ↑f.ker.support

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

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
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : x ∈ ↑U
⊢ 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
x : ↑Γ(↑U, ↑V)
⊢ x ∈ (Hom.ker (f ∣_ U)).ideal V ↔ x ∈ f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
simpa [Scheme.Hom.appLE] using! map_eq_zero_iff _
    (ConcreteCategory.bijective_of_isIso
      (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : f y = g x
⊢ x ∈ ⇑snd '' ⇑fst ⁻¹' s

Tactic:
obtain ⟨o, hl, hr⟩ := exists_preimage_of_isPullback h y x heq

Goal state after:
case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
s : Set ↥X
x : ↥Y
y : ↥X
hy : y ∈ s
heq : f y = g x
o : ↥P
hl : fst o = y
hr : snd o = x
⊢ x ∈ ⇑snd '' ⇑fst ⁻¹' s
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
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, f x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
      obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩

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
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ ↑(f ⁻¹ᵁ U')
hVU : ↑(f ⁻¹ᵁ U') ⊆ ↑(f ⁻¹ᵁ U)
⊢ ∃ U, f x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
this : Epi (app (ker f).subschemeι ↑U)
⊢ app (toImage f ≫ (ker f).subschemeι) ↑U =
    app (ker f).subschemeι ↑U ≫
      ((ker f).subschemeObjIso U).hom ≫
        CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯)

Tactic:
Scheme.Hom.congr_app f.toImage_imageι,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
this : Epi (app (ker f).subschemeι ↑U)
⊢ app f ↑U ≫ X.presheaf.map (eqToHom ⋯).op =
    app (ker f).subschemeι ↑U ≫
      ((ker f).subschemeObjIso U).hom ≫
        CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯)
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: case refine_3
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)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)

Tactic:
· rw [ht]; trivial

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ Function.Injective ⇑(ConcreteCategory.hom (app (toImage f) (imageι f ⁻¹ᵁ ↑U)))

Tactic:
simp only [f.toImage_app U, CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp]
  exact (RingHom.lift_injective_of_ker_le_ideal _ _ (by simp)).comp
    (f.ker.subschemeObjIso U).commRingCatIsoToRingEquiv.injective

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

Goal state before:
pp: case refine_2
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
⊢ ∀ (Y : CommRingCatᵒᵖ), ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ Y)

Tactic:
intro R

Goal state after:
case refine_2
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
R : CommRingCatᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ Nonempty (F.obj x ≅ R)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsImmersion x✝ ↔ (@IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f ↦ IsLocallyClosed (Set.range f)) x✝

Tactic:
exact isImmersion_iff _

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

Goal state before:
pp: case hP
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Set.range ((U i).carrier.restrictPreimage f)))

Tactic:
Set.range_restrictPreimage

Goal state after:
case hP
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f → (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' Set.range f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

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

Tactic:
exact MorphismProperty.of_isPullback this.flip inferInstance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = 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
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    (pullback.diagonal f) x

Tactic:
rw [← hz₁, ← hy, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy✝ : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = 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
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) w
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

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

Tactic:
let A := MvPolynomial (Fin n) R ⧸ I

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

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)

Tactic:
intro R

Goal state after:
case refine_1
R✝ : Type u_1
S : Type u_2
inst✝¹ : CommRing R✝
inst✝ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
⊢ ∀ [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] (T : Type u_2) [inst_2 : CommRing T]
    (f : R →+* S) (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)

Tactic:
intro R

Goal state after:
case refine_2
R✝ : Type u_1
S : Type u_2
inst✝¹ : CommRing R✝
inst✝ : CommRing S
f : R✝ →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
⊢ ∀ [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] (T : Type u_2) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T),
    (∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)) →
      (∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)) →
        ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap (g.comp f) '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) = X ^ Module.finrank R A ↔
    ∀ i < Module.finrank R A, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
simp_rw [← ((LinearMap.mul R A) f).charpoly_natDegree]

Goal state after:
case inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree ↔
    ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
⊢ IsClosedImmersion g

Tactic:
by
  wlog hX : ∃ R, X = Spec R
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsClosedImmersion) X.affineCover]
    intro i
    by_cases hxU : Set.range g ⊆ (X.affineCover.f i).opensRange
    · rw [Scheme.Cover.pullbackHom,
        ← (IsOpenImmersion.isPullback_lift_id _ _ hxU).flip.isoPullback_inv_snd,
        MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion]
      refine this (X.affineCover.f i ≫ f) _ ?_ ⟨_, rfl⟩
      rw [IsOpenImmersion.lift_fac_assoc, hg]
    · have : IsEmpty ((X.affineCover.pullback₁ g).X i) := by
        apply Scheme.isEmpty_pullback
        rw [← Set.subset_compl_iff_disjoint_left]
        rintro _ hx ⟨x, rfl⟩
        apply hxU
        rintro _ ⟨y, rfl⟩
        exact Subsingleton.elim x y ▸ hx
      infer_instance
  obtain ⟨R, rfl⟩ := hX
  wlog hY : ∃ S, Y = Spec S
  · 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⟩
  obtain ⟨S, rfl⟩ := hY
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
  rw [← Spec.map_comp, ← Spec.map_id, Spec.map_injective.eq_iff] at hg
  apply IsClosedImmersion.spec_of_surjective
  apply Function.LeftInverse.surjective (g := φ)
  exact fun x ↦ congr($hg.1 x)

Goal state after: