-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma monotone_semilength : Monotone semilength := fun p q pq ↦ by
  induction pq with
  | refl => rfl
  | tail _ mq ih =>
    rename_i m r _
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · rcases mq with hm | hm
      · exact ih.trans (hm ▸ semilength_insidePart_lt hr).le
      · exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

Proof state:
case tail.inr.inl
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

Tactic:
exact ih.trans (hm ▸ semilength_insidePart_lt hr).le

Result:
no goals

Proof state:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0

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

Result:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0
⊢ p.semilength ≤ semilength 0

Proof state:
case refl
p q : DyckWord
⊢ p.semilength ≤ p.semilength

Tactic:
rfl

Result:
no goals

Proof state:
case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength

Tactic:
rcases mq with hm | hm

Result:
case tail.inr.inl
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Proof state:
case tail.inr.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Tactic:
exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

Result:
no goals

Proof state:
case tail
p q b✝ c✝ : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p b✝
mq : b✝ = c✝.insidePart ∨ b✝ = c✝.outsidePart
ih : p.semilength ≤ b✝.semilength
⊢ p.semilength ≤ c✝.semilength

Tactic:
rename_i m r _

Result:
case tail
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
⊢ p.semilength ≤ r.semilength

Proof state:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0
⊢ p.semilength ≤ semilength 0

Tactic:
rwa [mq] at ih

Result:
no goals

Proof state:
case tail
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
⊢ p.semilength ≤ r.semilength

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Result:
case tail.inl
p q m : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ p.semilength ≤ semilength 0

case tail.inr
p q m r : DyckWord
a✝ : Relation.ReflTransGen (fun p q => p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
⊢ p.semilength ≤ r.semilength