mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.primeHeight ≠ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.primeHeight < ⊤

Tactic:
by

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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i)).ι ''ᵁ ⊤) ⋯))
⊢ (↑(S i)).ι ''ᵁ ⊤ = ↑(S i)

Tactic:
by

Goal state after:
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
⊢ ∃ l, RelSeries.last l = { asIdeal := p, isPrime := ⋯ } ∧ ↑l.length = p.height

Tactic:
by

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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ P f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ I.height ≤ J.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I ≤ J
⊢ I.primeHeight ≤ J.primeHeight

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ I.height + 1 ≤ J.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ I.primeHeight + 1 ≤ J.primeHeight

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ⊤.height = ⊤

Tactic:
by

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
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ I.height ≤ J.height

Tactic:
by

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
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ I.height < J.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : J.FiniteHeight
⊢ I.height < J.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : J.FiniteHeight
⊢ I.primeHeight < J.primeHeight

Tactic:
by

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 ≤ ringKrullDim R

Tactic:
by

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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ ↑(U i) = (↑(U i)).ι ''ᵁ ⊤

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I ≠ ⊤
⊢ ↑I.height ≤ ringKrullDim R

Tactic:
by

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
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
⊢ P f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
⊢ J ∈ I.minimalPrimes

Tactic:
by

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:
by

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.primeHeight = 0 ↔ I ∈ minimalPrimes R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
⊢ 1 ≤ (span {x}).height

Tactic:
by

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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⊥.height = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI0 : I = ⊥
⊢ I.height = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
⊢ I = ⊥

Tactic:
rcases exists_isPrime_height_eq hI with ⟨p, _, hIp, hp0⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
hI : I.height = 0
p : Ideal R
w✝ : p.IsPrime
hIp : I ≤ p
hp0 : p.height = ↑0
⊢ I = ⊥
Module: Mathlib.RingTheory.Ideal.Height

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : Subsingleton R
⊢ I.height = ⊤

Tactic:
by

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
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
⊢ I.IsMaximal

Tactic:
by

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
inst✝ : FiniteRingKrullDim R
e : ↑I.primeHeight = ringKrullDim R
⊢ ↑I.height = ringKrullDim R

Tactic:
by

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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
by

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

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

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
val✝ : Fintype ↑s
⊢ S ⊓ ↑U = ⨆ i, ↑↑i

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
e : R ≃+* S
p : Ideal S
inst✝ : p.IsPrime
⊢ (comap e p).height = p.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal S
⊢ (comap e I).height = I.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
e : R ≃+* S
I : Ideal R
⊢ (map e I).height = I.height

Tactic:
by

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:
by

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

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

Tactic:
by

Goal state after:
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
⊢ (comap (algebraMap R A) J).height = J.height

Tactic:
by

Goal state after:
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
⊢ (comap (algebraMap R A) J).primeHeight = J.primeHeight

Tactic:
by

Goal state after:
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
⊢ (under R J).height = J.height

Tactic:
by

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
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsLocalization.AtPrime A I
⊢ ringKrullDim A = ↑I.height

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
let P := p.map (algebraMap R S)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
P : Ideal S := Ideal.map (algebraMap R S) p
⊢ (Ideal.map (algebraMap R S) p).height = p.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
M : Submonoid R
inst✝¹ : IsLocalization M S
p : Ideal R
inst✝ : p.IsPrime
h : Disjoint ↑M ↑p
⊢ (Ideal.map (algebraMap R S) p).height = p.height

Tactic:
by

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

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
i : ↑s
⊢ ↑↑i ≤ S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : J.IsPrime
e : I ≤ J
e' : J.primeHeight = I.height
inst✝ : J.FiniteHeight
⊢ J ∈ I.minimalPrimes

Tactic:
by

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

Goal state before:
pp: 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 : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f)))
      ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ Ideal.span (Set.range fun i ↦ ↑i) = ⊤

Tactic:
by

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

Goal state before:
pp: 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 : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))) (Localization.awayMap f ↑r)
⊢ Ideal.span (Set.range fun i ↦ ↑i) = ⊤

Tactic:
by

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

Goal state before:
pp: 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
⊢ ¬↑I ⊆ ⋃ K ∈ hS.toFinset, ↑K

Tactic:
by

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

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
i : ↑s
⊢ ↑↑i ≤ ↑U

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ Cardinal.mk ↑{x} ≤ 1

Tactic:
by

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

Goal state before:
pp: 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
h : ↑r ≠ p.height
⊢ ↑(r + 1) ≤ p.height

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
hr : ↑r ≤ I.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height

Tactic:
by

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
⊢ P ⊓ P' = affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I ≠ ⊤), I.height) = ringKrullDim R

Tactic:
by

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

Goal state before:
pp: P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso P
⊢ HasRingHomProperty (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] ↦ P) fun {x S} {x_1} {x_2} φ ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime), P (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsPrime), I.height) = ringKrullDim R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (x : I.IsPrime), I.primeHeight) = ringKrullDim R

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (x : I.IsMaximal), I.primeHeight) = ringKrullDim R

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_2
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
n : ℕ
h : ∀ (P : Ideal R) [inst : P.IsMaximal], KrullDimLE n (Rₚ P)
⊢ KrullDimLE n R

Tactic:
by

Goal state after: