-- Mathlib/Order/KrullDimension.lean
/--
In a maximally long series, i.e one as long as the height of the last element, the height of each
element is its index in the series.
-/
lemma height_eq_index_of_length_eq_height_last {p : LTSeries α} (h : p.length = height p.last)
    (i : Fin (p.length + 1)) : height (p i) = i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑(RelSeries.smash p' (RelSeries.drop p i) ⋯).length ≤ height (RelSeries.smash p' (RelSeries.drop p i) ⋯).last
⊢ ↑p'.length ≤ ↑↑i

Tactic:
simp [← h] at hp''

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑p'.length + (↑p.length - ↑↑i) ≤ ↑p.length
⊢ ↑p'.length ≤ ↑↑i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ height (p.toFun i) = ↑↑i

Tactic:
refine le_antisymm (height_le ?_) (index_le_height p i)

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ ∀ (p_1 : LTSeries α), RelSeries.last p_1 = p.toFun i → ↑p_1.length ≤ ↑↑i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑p'.length + (↑p.length - ↑↑i) ≤ ↑p.length
⊢ ↑p'.length ≤ ↑↑i

Tactic:
clear h

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑p'.length + (↑p.length - ↑↑i) ≤ ↑p.length
⊢ ↑p'.length ≤ ↑↑i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ ∀ (p_1 : LTSeries α), RelSeries.last p_1 = p.toFun i → ↑p_1.length ≤ ↑↑i

Tactic:
intro p' hp'

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
⊢ ↑p'.length ≤ ↑↑i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
⊢ RelSeries.last p' = (RelSeries.drop p i).head

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : p'.length + (p.length - ↑i) ≤ p.length
⊢ p'.length ≤ ↑i

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
⊢ ↑p'.length ≤ ↑↑i

Tactic:
have hp'' := length_le_height_last (p := p'.smash (p.drop i) (by simpa))

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑(RelSeries.smash p' (RelSeries.drop p i) ⋯).length ≤ height (RelSeries.smash p' (RelSeries.drop p i) ⋯).last
⊢ ↑p'.length ≤ ↑↑i

Proof state:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : ↑p'.length + (↑p.length - ↑↑i) ≤ ↑p.length
⊢ ↑p'.length ≤ ↑↑i

Tactic:
norm_cast at *

Result:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
i : Fin (p.length + 1)
p' : LTSeries α
hp' : RelSeries.last p' = p.toFun i
hp'' : p'.length + (p.length - ↑i) ≤ p.length
⊢ p'.length ≤ ↑i