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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ CommRingCat.ofHom (algebraMap R ((structureSheafInType R R).obj.obj (op U))) ≫
      (structurePresheafInCommRingCat R).germ U x hxU =
    toStalk R x

Tactic:
dsimp [toStalk]
  rw [← (structurePresheafInCommRingCat R).germ_res (homOfLE (le_top : U ≤ ⊤)) _ hxU]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
⊢ F.IsLocallyDirected

Tactic:
by
  constructor
  rintro i j k (_ | i) (_ | j)
  · simpa using fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩
  · simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_comm, forall_eq]
    exact fun x ↦ ⟨_, .init _, 𝟙 _, x, by simp⟩
  · simp only [WidePushoutShape.hom_id, Functor.map_id, id_apply, forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, .init _, x, by simp⟩
  · simp only [((CategoryTheory.mono_iff_injective (F.map (.init i))).mp inferInstance).eq_iff,
      forall_eq']
    exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ ∀ (U : Opens ↑(PrimeSpectrum.Top R)) (hxU : x ∈ U),
    (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
      (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)

Tactic:
intro U hxU

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
⊢ (structurePresheafInModuleCat R M).germ U x hxU ≫ stalkToLocalizationₗ R M x ≫ localizationtoStalkₗ R M x =
    (structurePresheafInModuleCat R M).germ U x hxU ≫ 𝟙 ((structurePresheafInModuleCat R M).stalk x)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
rw [← Category.assoc, ← D.t_fac]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
rw [← Category.assoc, ← D.t_fac]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
this : (Spec R).toSpecΓ = Spec.map (Scheme.ΓSpecIso R).hom
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
eq_comm

Goal state after:
R : CommRingCat
this : Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ∀ x ∈ s, ↑(X.basicOpen x) ⊆ ↑U

Tactic:
intro x _

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ ↑(X.basicOpen x) ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ∀ x ∈ s, X.basicOpen x ≤ U

Tactic:
intro x _

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ X.basicOpen x ≤ U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Set.range ⇑g ⊆ Set.range ⇑U.ι

Tactic:
simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ (Opens.map f.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    (Opens.map g.base).obj
      (Y.toRingedSpace.basicOpen
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))

Tactic:
rw [preimage_basicOpen f, preimage_basicOpen g]

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (f.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this)) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          (g.c.app
            (op (unop (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 (unop (op U))))))))
        (have this := (ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s;
        this))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

Tactic:
change Ideal.comap _ _ = x.asIdeal.prod ⊤
    ext; simp [Ideal.prod, CommRingCat.ofHom]

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
f' : Z ⟶ Y
g' : Z ⟶ X
h : IsPullback g' f' f g
hg : P g
⊢ P (pullback.fst f g)

Tactic:
exact H f g hg

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k)))

Tactic:
← limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))),

Goal state after:
case op.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
        (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) =
    𝟙 (limit (D.diagramOverOpen U)) ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
        (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))
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 : J
xi : ↥(F.obj i)
xj : ↥(F.obj j)
⊢ (colimit.ι F i) xi = (colimit.ι F j) xj ↔ ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj

Tactic:
by
  constructor; swap
  · rintro ⟨k, fi, fj, x, rfl, rfl⟩; simp only [← Scheme.Hom.comp_apply, colimit.w]
  obtain ⟨i, rfl⟩ := (equivShrink J).symm.surjective i
  obtain ⟨j, rfl⟩ := (equivShrink J).symm.surjective j
  rw [← ((isColimit F).coconePointUniqueUpToIso
    (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]
  simp only [Limits.colimit, ← Scheme.Hom.comp_apply,
    colimit.comp_coconePointUniqueUpToIso_inv, cocone, glueDataι_naturality]
  refine ?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp
  dsimp +instances only [GlueData.Rel]
  rintro ⟨x, rfl, rfl⟩
  obtain ⟨⟨k, ki, kj⟩, y, hy : F.map ki y = (glueData F).f i j x⟩ := mem_iSup.mp x.2
  refine ⟨k, ki, kj, y, hy, ?_⟩
  obtain ⟨k, rfl⟩ := (equivShrink J).symm.surjective k
  apply ((glueData F).ι _).isOpenEmbedding.injective
  simp only [← Scheme.Hom.comp_apply, Category.assoc, GlueData.glue_condition]
  trans (glueData F).ι k y
  · simp [← glueDataι_naturality F kj]; rfl
  · simp [← glueDataι_naturality F ki, ← hy]; rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x * (algebraMap R (Rₜ ⟨a, ha⟩)) ↑⟨a ^ ((sec a x).2 + 1), ⋯⟩ = (algebraMap R (Rₜ ⟨a, ha⟩)) (a * (sec a x).1)

Tactic:
map_pow,

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x * (algebraMap R (Rₜ ⟨a, ha⟩)) a ^ ((sec a x).2 + 1) = (algebraMap R (Rₜ ⟨a, ha⟩)) (a * (sec a x).1)
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ (n + 1) * y ∈ J
⊢ y ∈ J

Tactic:
add_comm,

Goal state after:
case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ (1 + n) * y ∈ J
⊢ y ∈ J
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

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

Tactic:
intro H

Goal state after:
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)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

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

Tactic:
intro H

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

Goal state before:
pp: case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis (Set.range fun U ↦ ↑U)

Tactic:
rw [Subtype.range_coe]; exact X.isBasis_affineOpens

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

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

Tactic:
intro H

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.QuasiSeparated

Goal state before:
pp: case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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:
intro H

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 V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact ↑⊤

Tactic:
← f.preimage_top,

Goal state after:
case of_basicOpenCover
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset ↑Γ(Y, ⊤)
hS : ⨆ f, Y.basicOpen ↑f = ⊤
hS' : ∀ (r : ↥S), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)
⊢ IsCompact ↑(f ⁻¹ᵁ ⊤)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
⊢ ∃ p, p.IsMaximal ∧ ↑p.height = ringKrullDim R

Tactic:
let l := LTSeries.longestOf (PrimeSpectrum R)
  obtain ⟨m, hm, hle⟩ := l.last.asIdeal.exists_le_maximal IsPrime.ne_top'
  refine ⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩
  trans (l.last.asIdeal.height : WithBot ℕ∞)
  · rw [Ideal.height_eq_primeHeight]
    exact LTSeries.height_last_longestOf.symm.le
  · norm_cast
    exact height_mono hle

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
⊢ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
H : ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n
⊢ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

Tactic:
rw [Ideal.height_le_iff]
  constructor
  · intro H q hq e _
    exact H q hq e
  · intro H q hq e
    obtain ⟨⟨x, hx⟩, hqx, hxp⟩ :=
      @exists_le_covBy_of_lt { I : Ideal R // I.IsPrime } ⟨q, hq⟩ ⟨p, ‹_›⟩ _ _ e
    exact (Ideal.height_mono hqx).trans_lt
      (H _ hx hxp.1 (fun I hI e ↦ hxp.2 (show Subtype.mk x hx < ⟨I, hI⟩ from e)))

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n

Tactic:
ringKrullDim,

Goal state after:
R : Type u_2
inst✝ : CommRing R
n : WithBot ℕ∞
⊢ Order.krullDim (PrimeSpectrum R) ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
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))
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap S T)))

Tactic:
Spec.map_comp

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 S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
r : S
inst✝ : IsLocalization.Away r T
f : R →+* S
hf : P (Spec.map (CommRingCat.ofHom f))
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap S T)))
⊢ P (Spec.map (CommRingCat.ofHom (algebraMap S T)) ≫ Spec.map (CommRingCat.ofHom 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 S T _ _ _ _ r _ f hf
    have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := T) r
    change P (Spec.map (CommRingCat.ofHom f ≫ CommRingCat.ofHom (algebraMap _ _)))
    rw [Spec.map_comp]
    exact IsZariskiLocalAtSource.comp hf ..

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

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

Tactic:
exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, le_refl _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) (s ^ n) = (ConcreteCategory.hom (X.presheaf.map iV.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
map_pow,

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s ^ n = (ConcreteCategory.hom (X.presheaf.map iV.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst✝ : IsReduced (Spec R)
hx : x.asIdeal ∈ minimalPrimes ↑R
⊢ Subsingleton (PrimeSpectrum ↑((Spec R).presheaf.stalk x))

Tactic:
exact IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes _ hx
    ((Spec.structureSheaf R).presheaf.stalk x)

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

Goal state before:
pp: case refine_1
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ I.ideal U

Tactic:
add_comm,

Goal state after:
case refine_1
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₂ + n₁) * x ∈ I.ideal U
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 y z : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0 → ∃ c, ↑c * z = 0

Tactic:
intro H

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : ↑Γ(X, U)
H : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) z = 0
⊢ ∃ c, ↑c * z = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
⊢ False

Tactic:
replace e := congr_arg (X.presheaf.germ U x hxU) e

Goal state after:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (a * b) = (ConcreteCategory.hom (X.presheaf.germ U x hxU)) 0
⊢ False
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

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