-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma infix_of_le (h : p ≤ q) : p.toList <:+: q.toList

Proof state:
case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
⊢ ↑p <:+: ↑r

Tactic:
rcases mq with hm | hm

Result:
case tail.inr.inl
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
⊢ ↑p <:+: ↑r

case tail.inr.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
⊢ ↑p <:+: ↑r

Proof state:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

Tactic:
rw [insidePart_zero, outsidePart_zero, or_self] at mq

Result:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0
⊢ ↑p <:+: ↑0

Proof state:
case h
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
⊢ [U] ++ ↑r.insidePart ++ ([D] ++ ↑r.outsidePart) = ↑r

Tactic:
rwa [← append_assoc]

Result:
no goals

Proof state:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = 0
⊢ ↑p <:+: ↑0

Tactic:
rwa [mq] at ih

Result:
no goals

Proof state:
case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r

Tactic:
have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r :=
  DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)

Result:
case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
⊢ ↑p <:+: ↑r

Proof state:
case h
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
⊢ [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart ++ [] = ↑r

Tactic:
rwa [append_nil]

Result:
no goals

Proof state:
case tail.inr.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this✝ : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
this : ↑r.outsidePart <:+: ↑r
⊢ ↑p <:+: ↑r

Tactic:
exact ih.trans (hm ▸ this)

Result:
no goals

Proof state:
case tail.inr.inl
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
⊢ ↑p <:+: ↑r

Tactic:
have : r.insidePart <:+: r.toList := by
  use [U], [D] ++ r.outsidePart; rwa [← append_assoc]

Result:
case tail.inr.inl
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this✝ : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
this : ↑r.insidePart <:+: ↑r
⊢ ↑p <:+: ↑r

Proof state:
case tail.inr.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
⊢ ↑p <:+: ↑r

Tactic:
have : r.outsidePart <:+: r.toList := by
  use [U] ++ r.insidePart ++ [D], []; rwa [append_nil]

Result:
case tail.inr.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this✝ : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
this : ↑r.outsidePart <:+: ↑r
⊢ ↑p <:+: ↑r

Proof state:
case refl
p q : DyckWord
⊢ ↑p <:+: ↑p

Tactic:
exact infix_refl _

Result:
no goals

Proof state:
case tail.inr.inl
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this✝ : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
this : ↑r.insidePart <:+: ↑r
⊢ ↑p <:+: ↑r

Tactic:
exact ih.trans (hm ▸ this)

Result:
no goals

Proof state:
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
⊢ ↑r.insidePart <:+: ↑r

Tactic:
use [U], [D] ++ r.outsidePart

Result:
case h
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.insidePart
⊢ [U] ++ ↑r.insidePart ++ ([D] ++ ↑r.outsidePart) = ↑r

Proof state:
case tail
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
⊢ ↑p <:+: ↑r

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Result:
case tail.inl
p q m : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ ↑p <:+: ↑0

case tail.inr
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
hr : r ≠ 0
⊢ ↑p <:+: ↑r

Proof state:
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
⊢ ↑r.outsidePart <:+: ↑r

Tactic:
use [U] ++ r.insidePart ++ [D], []

Result:
case h
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : ↑p <:+: ↑m
hr : r ≠ 0
this : [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart = ↑r
hm : m = r.outsidePart
⊢ [U] ++ ↑r.insidePart ++ [D] ++ ↑r.outsidePart ++ [] = ↑r

Proof state:
case tail
p q b✝ c✝ : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p b✝
mq : b✝ = c✝.insidePart ∨ b✝ = c✝.outsidePart
ih : ↑p <:+: ↑b✝
⊢ ↑p <:+: ↑c✝

Tactic:
rename_i m r

Result:
case tail
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : ↑p <:+: ↑m
⊢ ↑p <:+: ↑r