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

Goal state before:
pp: case H.mpr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
x y : (a : ι) → R a
⊢ Function.update 0 i 1 * x = Function.update 0 i 1 * y →
    (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y

Tactic:
intro e

Goal state after:
case H.mpr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : Function.update 0 i 1 * x = Function.update 0 i 1 * y
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

Tactic:
rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact restrict _ _ hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_
    have := exists_of_pullback_V_V F x
    obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, e⟩ := this -- doing them in the same step times out.
    refine ⟨α.opensRange, ⟨_, e⟩, ?_⟩
    rw [← cancel_mono (pullback.snd _ _), ← cancel_mono (Scheme.Opens.ι _)]
    simp only [t, Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
      limit.lift_π_assoc, cospan_left, IsOpenImmersion.lift_fac, Category.id_comp]
    rw [IsOpenImmersion.comp_lift_assoc]
    simp only [limit.lift_π_assoc, cospan_left, PullbackCone.mk_π_app]
    rw [← cancel_epi α.isoOpensRange.hom]
    simp_rw [Scheme.Hom.isoOpensRange_hom_ι_assoc, IsOpenImmersion.comp_lift_assoc]
    simp only [reassoc_of% hα₁, homOfLE_tAux F _ _ fi fj, Iso.hom_inv_id_assoc, reassoc_of% hα₂]
    generalize_proofs _ h₁
    have : IsOpenImmersion.lift (V F ↓j ↓k).ι (F.map fj) h₁ = (F.map fj).isoOpensRange.hom ≫
        (F.obj ↓j).homOfLE (le_iSup_of_le ⟨l, fj, fk⟩ le_rfl) := by
      rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac,
        ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]
      exact (Scheme.homOfLE_ι _ _).symm
    simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fj fk, Iso.hom_inv_id_assoc]
    generalize_proofs h₂
    have : IsOpenImmersion.lift (V F ↓k ↓i).ι (F.map fk) h₂ = (F.map fk).isoOpensRange.hom ≫
        (F.obj ↓k).homOfLE (le_iSup_of_le ⟨l, fk, fi⟩ le_rfl) := by
      rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac,
        ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]
      exact (Scheme.homOfLE_ι _ _).symm
    simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fk fi, Iso.hom_inv_id_assoc,
      ← Iso.inv_comp_eq, Scheme.Hom.isoOpensRange_inv_comp]
    exact (Scheme.homOfLE_ι _ _).symm

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

Goal state before:
pp: ⊢ (topologically @SpecializingMap).RespectsIso

Tactic:
apply topologically_respectsIso
  · introv
    exact f.isClosedMap.specializingMap
  · introv hf hg
    exact hf.comp hg

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

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact ⟨s, hsone, fun t ht ↦ hPQ (hs t ht)⟩

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

Goal state before:
pp: ⊢ RespectsIso fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f

Tactic:
apply surjective_stableUnderComposition.respectsIso
  intro _ _ _ _ e
  exact e.surjective

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

Goal state before:
pp: case to_basicOpen
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
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen r)

Tactic:
rw [sourceAffineLocally_morphismRestrict]

Goal state after:
case to_basicOpen
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
r : ↑Γ(Y, ⊤)
H : sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ Y.basicOpen r),
    P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsPreimmersion (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ (CommRingCat.Hom.hom f).SurjectiveOnStalks

Tactic:
by
  rw [← HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks), isPreimmersion_iff, and_comm]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.primeHeight = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
by
  rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]

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

Goal state before:
pp: case neg
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
h : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
⊢ ↑r ≠ p.height

Tactic:
intro e

Goal state after:
case neg
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
h : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
e : ↑r = p.height
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H✝ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Y → P f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
H : P ((f ⁻¹ᵁ ↑U).ι ≫ f ≫ g)
⊢ P (f ∣_ ↑U)

Tactic:
rw [← morphismRestrict_ι_assoc] at H

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H✝ :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Y → P f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
H : P (f ∣_ ↑U ≫ (↑U).ι ≫ g)
⊢ P (f ∣_ ↑U)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0

Tactic:
specialize H (f.app _ s) _ x ⟨x, rfl⟩

Goal state after:
case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↥X) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) = ⊥

case h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↥X
H :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
this : IsReduced X
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯)) s = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ ⊤ = ⋂ U, X.zeroLocus ↑(⊥ U)

Tactic:
ext; simp

Goal state after:
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:
← Ideal.map_le_iff_le_comap,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) ≤ I.ideal U
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
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P f ↔ ∀ (x : ↥X), ∃ U V, ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
have inst : HasRingHomProperty P Q := inferInstance
  have : HasRingHomProperty P (Locally Q) := by
    apply @copy (P := P) (P' := P) (Q := Q) (Q' := Locally Q)
    · infer_instance
    · rfl
    · intro R S _ _ f
      exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm
  rw [iff_exists_appLE_locally (P := P) hQ]
  have : HasRingHomProperty P Q := inst
  apply (isLocal_ringHomProperty P (Q := Q)).respectsIso

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ⊤ * I = I

Tactic:
ext; simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ I * ⊤ = I

Tactic:
ext; simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ⊥ * I = ⊥

Tactic:
ext; simp

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ I * ⊥ = ⊥

Tactic:
ext; simp

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

Goal state before:
pp: case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h ≫ (↑V).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Tactic:
← IsAffineOpen.isoSpec_hom V.2,

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ X.homOfLE h ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
← Ideal.map,

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
this✝¹ : Algebra ↑Γ(X, ↑U) ↑Γ(X, ↑(X.affineBasicOpen f)) := (CommRingCat.Hom.hom F).toAlgebra
this✝ : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
this : Topology.IsOpenEmbedding ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, ↑U))
I : Ideal ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(Ideal.map (CommRingCat.Hom.hom F) I))
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus ↑I
⊢ x ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (f.app ↑U))
      (RingHom.ker (CommRingCat.Hom.hom (X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op)))

Tactic:
exact Ideal.ker_le_comap _ hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
K : Type u
inst✝ : Field K
g : Spec (CommRingCat.of K) ⟶ X
⊢ descResidueField (stalkClosedPointTo (g ≫ f)) =
    Hom.residueFieldMap f (g (closedPoint K)) ≫ descResidueField (stalkClosedPointTo g)

Tactic:
by
  simp [← cancel_epi (Y.residue _), stalkClosedPointTo_comp, residue_residueFieldMap_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
by
  subst h
  simp only [Triplet.tensorCongr_refl, Iso.refl_hom, Spec.map_id, Category.id_comp]

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

Goal state before:
pp: X Y✝ Z Y : Scheme
f g : (Over Y)ᵒᵖ
hfg : f ⟶ g
⊢ Hom.ker (Opposite.unop f).hom ≤ Hom.ker (Opposite.unop g).hom

Tactic:
by simpa only [Functor.id_obj, Functor.const_obj_obj,
    OrderDual.toDual_le_toDual, ← Over.w hfg.unop] using hfg.unop.left.le_ker_comp f.unop.hom

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, ↑⟨U i, ⋯⟩ = ⊤

Tactic:
· exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.EssFiniteType
hg : g.EssFiniteType
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.EssFiniteType R S
algebraizeInst✝ : Algebra.EssFiniteType S T
⊢ (g.comp f).EssFiniteType

Tactic:
exact Algebra.EssFiniteType.comp R S T

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)

Tactic:
by
    wlog hZ : IsAffine Z
    · rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this hA hQ _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2
    rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg
    obtain ⟨hY, hg⟩ := hg
    rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
    obtain ⟨hX, hf⟩ := hf
    rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]
    exact ⟨hX, hQ _ _ hg hf⟩

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
h : IsIso I.subschemeι
⊢ I = ⊥

Tactic:
simp [← I.ker_subschemeι]

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this✝ : IsAffine ↑U
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (X.homOfLE ⋯)

Tactic:
ext; simp

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

Goal state before:
pp: case inr.mp
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

Tactic:
intro e

Goal state after:
case inr.mp
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
e :
  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.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr.inl
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
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i = ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (algebraMap R I.ResidueField) 1 = 1

Tactic:
map_one

Goal state after:
case inr.mpr.inl
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
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i = ((LinearMap.mul R A) f).charpoly.natDegree
⊢ 1 = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
⊢ IsOpenMap (comap (algebraMap A (A ⊗[K] B)))

Tactic:
intro U hU
  wlog hU' : ∃ f, U = SetLike.coe (basicOpen f) generalizing U
  · rw [eq_biUnion_of_isOpen hU, Set.image_iUnion₂]
    exact isOpen_iUnion fun _ ↦ isOpen_iUnion fun _ ↦ this _ (basicOpen _).isOpen ⟨_, rfl⟩
  obtain ⟨f, rfl⟩ := hU'
  obtain ⟨B', hB, f, rfl⟩ := exists_fg_and_mem_baseChange f
  have : Algebra.FinitePresentation K B' :=
    Algebra.FinitePresentation.of_finiteType.mp ⟨B'.fg_top.mpr hB⟩
  convert!
    isOpenMap_comap_of_hasGoingDown_of_finitePresentation (R := A) (S := A ⊗[K] B') _
      (basicOpen f).isOpen using 1
  ext x
  rw [PrimeSpectrum.mem_image_comap_basicOpen, PrimeSpectrum.mem_image_comap_basicOpen,
    not_iff_not]
  let ψ := Algebra.TensorProduct.map
    (Algebra.TensorProduct.map (.id A A) B'.val) (.id A x.asIdeal.ResidueField)
  have hψeq : ψ = (Algebra.TensorProduct.comm _ _ _ |>.toAlgHom.comp <|
    Algebra.TensorProduct.cancelBaseChange K A A _ B |>.symm.toAlgHom.comp <|
    Algebra.TensorProduct.map (.id _ _) B'.val |>.comp <|
    Algebra.TensorProduct.cancelBaseChange K A A _ B' |>.toAlgHom.comp <|
    (Algebra.TensorProduct.comm _ _ _).toAlgHom) := by ext; simp [ψ]
  have hψ : Function.Injective ψ := by
    rw [hψeq]
    dsimp
    simp_rw [EmbeddingLike.comp_injective, ← Function.comp_assoc, EquivLike.injective_comp]
    exact Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
  rw [← IsNilpotent.map_iff hψ]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
⊢ IsNoetherianRing R

Tactic:
apply monotone_stabilizes_iff_noetherian.mp
  intro I
  let floc s := algebraMap R (Away (M := R) s)
  let suitableN s :=
    { n : ℕ | ∀ m : ℕ, n ≤ m → (Ideal.map (floc s) (I n)) = (Ideal.map (floc s) (I m)) }
  let minN s := sInf (suitableN s)
  have hSuit : ∀ s : S, minN s ∈ suitableN s := by
    intro s
    apply Nat.sInf_mem
    let f : ℕ →o Ideal (Away (M := R) s) :=
      ⟨fun n ↦ Ideal.map (floc s) (I n), fun _ _ h ↦ Ideal.map_mono (I.monotone h)⟩
    exact monotone_stabilizes_iff_noetherian.mpr (hN s) f
  let N := Finset.sup S minN
  use N
  have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop
  intro n hn
  rw [IsLocalization.ideal_eq_iInf_under_map_away hS (I N),
      IsLocalization.ideal_eq_iInf_under_map_away hS (I n),
      iInf_subtype', iInf_subtype']
  apply iInf_congr
  intro s
  congr 1
  rw [← hSuit s N (hN s)]
  exact hSuit s n <| Nat.le_trans (hN s) hn

Goal state after: