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

Proof state:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' = count D r'
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
simp [hq]

Result:
no goals

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q

Tactic:
replace h : r + p = q := DyckWord.ext h

Result:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ q

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ p ≤ q

Tactic:
have e : r' = r := by
  simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']

Result:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
⊢ p ≤ q

Proof state:
p q : DyckWord
h : ↑p <:+ ↑q
⊢ p ≤ q

Tactic:
obtain ⟨r', h⟩ := h

Result:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
⊢ p ≤ q

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ q

Tactic:
rw [← h]

Result:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ r + p

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
⊢ p ≤ q

Tactic:
have hc : (q.toList.take (q.toList.length - p.toList.length)).count U =
    (q.toList.take (q.toList.length - p.toList.length)).count D := by
  have hq := q.count_U_eq_count_D
  rw [← h] at hq ⊢
  rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq
  simp [hq]

Result:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
⊢ p ≤ q

Proof state:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U ↑q = count D ↑q
⊢ count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)

Tactic:
rw [← h] at hq ⊢

Result:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U (r' ++ ↑p) = count D (r' ++ ↑p)
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Proof state:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
⊢ count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)

Tactic:
have hq := q.count_U_eq_count_D

Result:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U ↑q = count D ↑q
⊢ count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
⊢ p ≤ q

Tactic:
rw [e] at h

Result:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
h : ↑r ++ ↑p = ↑q
e : r' = ↑r
⊢ p ≤ q

Proof state:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U (r' ++ ↑p) = count D (r' ++ ↑p)
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq

Result:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' = count D r'
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
⊢ p ≤ q

Tactic:
let r : DyckWord := q.take _ hc

Result:
case intro
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ p ≤ q

Proof state:
case intro
p q : DyckWord
r' : List DyckStep
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
e : r' = ↑r
h : r + p = q
⊢ p ≤ r + p

Tactic:
exact le_add_self ..

Result:
no goals

Proof state:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hc : count U (List.take ((↑q).length - (↑p).length) ↑q) = count D (List.take ((↑q).length - (↑p).length) ↑q)
r : DyckWord := q.take ((↑q).length - (↑p).length) hc
⊢ r' = ↑r

Tactic:
simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']

Result:
no goals