-- Mathlib/RingTheory/Ideal/Height.lean
@[gcongr]
lemma Ideal.height_strict_mono_of_is_prime {I J : Ideal R} [I.IsPrime]
    (h : I < J) [I.FiniteHeight] : I.height < J.height

Proof state:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
⊢ I.primeHeight + 1 ≤ K.primeHeight

Tactic:
haveI := Ideal.minimalPrimes_isPrime hK

Result:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
this : K.IsPrime
⊢ I.primeHeight + 1 ≤ K.primeHeight

Proof state:
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:
rw [Ideal.height_eq_primeHeight I]

Result:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ I.primeHeight < J.height

Proof state:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
this✝ : K.IsPrime
this : I < K
⊢ I.primeHeight + 1 ≤ K.primeHeight

Tactic:
exact Ideal.primeHeight_add_one_le_of_lt this

Result:
no goals

Proof state:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ ∀ (i : Ideal R) (j : i ∈ J.minimalPrimes), I.primeHeight + 1 ≤ i.primeHeight

Tactic:
intro K hK

Result:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
⊢ I.primeHeight + 1 ≤ K.primeHeight

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.primeHeight < ⊤

Tactic:
exact I.primeHeight_lt_top

Result:
no goals

Proof state:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
this : K.IsPrime
⊢ I.primeHeight + 1 ≤ K.primeHeight

Tactic:
have : I < K := lt_of_lt_of_le h hK.1.2

Result:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
this✝ : K.IsPrime
this : I < K
⊢ I.primeHeight + 1 ≤ K.primeHeight

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

Tactic:
by_cases hJ : J = ⊤

Result:
case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.primeHeight < J.height

case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.primeHeight < J.height

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.primeHeight < J.height

Tactic:
rw [← ENat.add_one_le_iff I.primeHeight_ne_top, Ideal.height]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.primeHeight + 1 ≤ ⨅ J_1, ⨅ (h : J_1 ∈ J.minimalPrimes), J_1.primeHeight

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.primeHeight < J.height

Tactic:
rw [hJ, height_top]

Result:
case pos
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : J = ⊤
⊢ I.primeHeight < ⊤

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.primeHeight + 1 ≤ ⨅ J_1, ⨅ (h : J_1 ∈ J.minimalPrimes), J_1.primeHeight

Tactic:
apply le_iInf₂

Result:
case neg.h
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
hJ : ¬J = ⊤
⊢ ∀ (i : Ideal R) (j : i ∈ J.minimalPrimes), I.primeHeight + 1 ≤ i.primeHeight