-- Mathlib/Order/KrullDimension.lean
/-- Another characterization of height, based on the supremum of the heights of elements below. -/
lemma height_eq_iSup_lt_height (x : α) : height x = ⨆ y < x, height y + 1

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ i < x, height i + 1 ≤ height x

Tactic:
intro y hyx

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ height y + 1 ≤ height x

Proof state:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply le_iSup_of_le p.eraseLast.last

Result:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ (_ : (RelSeries.eraseLast p).last < x), height (RelSeries.eraseLast p).last + 1

Proof state:
case a.h.zero
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = 0
⊢ ↑0 ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
simp

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
cases hlen : p.length with
| zero => simp
| succ n =>
  apply le_iSup_of_le p.eraseLast.last
  apply le_iSup_of_le (by rw [← hp]; apply RelSeries.eraseLast_last_rel_last _ (by omega))
  rw [height_add_const]
  apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Result:
no goals

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ∀ (i : LTSeries α), RelSeries.last i = y → ↑i.length + 1 ≤ height x

Tactic:
intro p hp

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ height x

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last = (RelSeries.eraseLast p).last

Tactic:
rfl

Result:
no goals

Proof state:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ height x

Tactic:
apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)

Result:
no goals

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
intro p hp

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
⊢ ↑p.length ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x

Tactic:
apply iSup₂_le

Result:
case a.h.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ∀ (i : LTSeries α), RelSeries.last i = y → ↑i.length + 1 ≤ height x

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ height y + 1 ≤ height x

Tactic:
rw [height_add_const]

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = y), ↑p.length + 1 ≤ height x

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ↑(RelSeries.eraseLast p).length + 1

Tactic:
simp [hlen]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ ↑(RelSeries.snoc p x ⋯).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ p.length ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ (RelSeries.snoc p x ⋯).last ≤ x

Tactic:
simp

Result:
no goals

Proof state:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ (_ : (RelSeries.eraseLast p).last < x), height (RelSeries.eraseLast p).last + 1

Tactic:
apply le_iSup_of_le (by rw [← hp]; apply RelSeries.eraseLast_last_rel_last _ (by omega))

Result:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ height (RelSeries.eraseLast p).last + 1

Proof state:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ height (RelSeries.eraseLast p).last + 1

Tactic:
rw [height_add_const]

Result:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1

Proof state:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply height_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ (p : LTSeries α), RelSeries.last p = x → ↑p.length ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < x

Tactic:
rw [← hp]

Result:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ (RelSeries.eraseLast p).last < RelSeries.last p

Tactic:
apply RelSeries.eraseLast_last_rel_last _ (by omega)

Result:
no goals

Proof state:
case a.h.succ
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hp : RelSeries.last p = x
n : ℕ
hlen : p.length = n + 1
⊢ ↑(n + 1) ≤ ⨆ p_1, ⨆ (_ : RelSeries.last p_1 = (RelSeries.eraseLast p).last), ↑p_1.length + 1

Tactic:
apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x

Tactic:
apply iSup₂_le

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ∀ i < x, height i + 1 ≤ height x