-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma firstReturn_add : (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
⊢ (p + q).firstReturn = p.firstReturn

Tactic:
have u : (p + q).toList = p.toList ++ q.toList := rfl

Result:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ (p + q).firstReturn = p.firstReturn

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q)) ∧
    ∀ j < p.firstReturn,
      decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
have v := firstReturn_lt_length h

Result:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q)) ∧
    ∀ j < p.firstReturn,
      decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Proof state:
p q : DyckWord
⊢ (p + q).firstReturn = if p = 0 then q.firstReturn else p.firstReturn

Tactic:
split_ifs with h

Result:
case pos
p q : DyckWord
h : p = 0
⊢ (p + q).firstReturn = q.firstReturn

case neg
p q : DyckWord
h : ¬p = 0
⊢ (p + q).firstReturn = p.firstReturn

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (↑p).length + (↑q).length

Tactic:
exact Nat.lt_add_right _ (firstReturn_lt_length h)

Result:
no goals

Proof state:
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ p.firstReturn + 1 - (↑p).length = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q)) ∧
    ∀ j < p.firstReturn,
      decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
constructor

Result:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q))

case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Proof state:
case pos
p q : DyckWord
h : p = 0
⊢ (p + q).firstReturn = q.firstReturn

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) ↑p) = count D (List.take (j + 1) ↑p)) = false

Tactic:
simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'

Result:
no goals

Proof state:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
rw [take_append_eq_append_take, show j + 1 - p.toList.length = 0 by omega,
  take_zero, append_nil]

Result:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) ↑p) = count D (List.take (j + 1) ↑p)) = false

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ (p + q).firstReturn = p.firstReturn

Tactic:
rw [firstReturn, findIdx_eq]

Result:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ decide
        (count U (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q)) =
          count D (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q))) =
      true ∧
    ∀ (j : ℕ) (hji : j < p.firstReturn),
      decide
          (count U (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q)) =
            count D (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q))) =
        false

case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (range (↑(p + q)).length).length

Proof state:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ ∀ j < p.firstReturn, decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Tactic:
intro j hj

Result:
case neg.right
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (range (↑(p + q)).length).length

Tactic:
rw [length_range, u, length_append]

Result:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ p.firstReturn < (↑p).length + (↑q).length

Proof state:
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
j : ℕ
hj : j < p.firstReturn
⊢ j + 1 - (↑p).length = 0

Tactic:
omega

Result:
no goals

Proof state:
case neg.left
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
v : p.firstReturn < (↑p).length
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q))

Tactic:
rw [take_append_eq_append_take, show p.firstReturn + 1 - p.toList.length = 0 by omega,
  take_zero, append_nil, count_take_firstReturn_add_one h]

Result:
no goals

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ decide
        (count U (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q)) =
          count D (List.take ((range (↑(p + q)).length)[p.firstReturn] + 1) ↑(p + q))) =
      true ∧
    ∀ (j : ℕ) (hji : j < p.firstReturn),
      decide
          (count U (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q)) =
            count D (List.take ((range (↑(p + q)).length)[j] + 1) ↑(p + q))) =
        false

Tactic:
simp_rw [u, decide_eq_true_eq, getElem_range]

Result:
case neg
p q : DyckWord
h : ¬p = 0
u : ↑(p + q) = ↑p ++ ↑q
⊢ count U (List.take (p.firstReturn + 1) (↑p ++ ↑q)) = count D (List.take (p.firstReturn + 1) (↑p ++ ↑q)) ∧
    ∀ j < p.firstReturn,
      decide (count U (List.take (j + 1) (↑p ++ ↑q)) = count D (List.take (j + 1) (↑p ++ ↑q))) = false