-- Mathlib/Order/KrullDimension.lean
lemma height_le {a : α} {n : ℕ∞} (h : ∀ (p : LTSeries α), p.last = a → p.length ≤ n) :
    height a ≤ n

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p.length ≤ n

Tactic:
rw [show p.length = p'.length by simp [p']; omega]

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p'.length ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
⊢ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

Tactic:
intro p hlast

Result:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
⊢ ↑p.length ≤ n

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n

Tactic:
let p' := p.eraseLast.snoc a (lt_of_lt_of_le (p.eraseLast_last_rel_last (by simp_all)) hlast)

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p.length ≤ n

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ p.length ≠ 0

Tactic:
simp_all

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ p.length = p'.length

Tactic:
simp [p']

Result:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ p.length = p.length - 1 + 1

Proof state:
case a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ p'.last = a

Tactic:
simp [p']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
⊢ ↑p.length ≤ n

Tactic:
wlog hlenpos : p.length ≠ 0

Result:
case inr
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
this :
  ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
    (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) →
      ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → p.length ≠ 0 → ↑p.length ≤ n
hlenpos : ¬p.length ≠ 0
⊢ ↑p.length ≤ n

α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
⊢ ↑p.length ≤ n

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ p.length = p.length - 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
⊢ height a ≤ n

Tactic:
apply height_le_iff.mpr

Result:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
⊢ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

Proof state:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ ↑p'.length ≤ n

Tactic:
apply h

Result:
case a
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
h : ∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n
p : LTSeries α
hlast : RelSeries.last p ≤ a
hlenpos : p.length ≠ 0
p' : RelSeries fun x1 x2 => x1 < x2 := (RelSeries.eraseLast p).snoc a ⋯
⊢ p'.last = a