-- Mathlib/Order/KrullDimension.lean
/-- There exist a series ending in a element for any length up to the element’s height. -/
lemma exists_series_of_le_height (a : α) {n : ℕ} (h : n ≤ height a) :
    ∃ p : LTSeries α, p.last = a ∧ p.length = n

Proof state:
case h.left
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a

Tactic:
simp [hlast]

Result:
no goals

Proof state:
case h.intro.mk
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : (fun x => (↑x).length) ⟨p, ⋯⟩ = m
⊢ m ≤ n

Tactic:
simp only at hp

Result:
case h.intro.mk
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
⊢ m ≤ n

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x => (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
contrapose! ha

Result:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ∀ (p : LTSeries α), RelSeries.last p = a → p.length ≠ n
⊢ ∃ x, ∀ y ∈ Set.range fun x => (↑x).length, y ≤ x

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : height a = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def] at ha

Result:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x => (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Proof state:
case coe.intro.mk
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
use p.drop ⟨m-n, by omega⟩

Result:
case h
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a ∧ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ m - n < p.length + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
simp

Result:
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ p.length - (m - n) = n

Proof state:
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ p.length - (m - n) = n

Tactic:
omega

Result:
no goals

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
ha : height a = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
clear h

Result:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : height a = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Proof state:
case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ m - (m - n) = n

Tactic:
omega

Result:
no goals

Proof state:
case coe.intro.mk
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : ↑(↑⟨p, hlast⟩).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
simp only [Nat.cast_inj] at hlen

Result:
case coe.intro.mk
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype'] at ha

Result:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a ∧ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
constructor

Result:
case h.left
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a

case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Proof state:
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
hnm : n < m
⊢ m - n < p.length + 1

Tactic:
omega

Result:
no goals

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
rw [ha, Nat.cast_le] at h

Result:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : height a = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ∀ (p : LTSeries α), RelSeries.last p = a → p.length ≠ n
⊢ ∃ x, ∀ y ∈ Set.range fun x => (↑x).length, y ≤ x

Tactic:
use n

Result:
case h
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ∀ (p : LTSeries α), RelSeries.last p = a → p.length ≠ n
⊢ ∀ y ∈ Set.range fun x => (↑x).length, y ≤ n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩

Result:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n