-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma firstReturn_nest : p.nest.firstReturn = p.toList.length + 1

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
      count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) ∧
    ∀ j < (↑p).length + 1,
      decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
constructor

Result:
case left
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
    count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D]))

case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ ∀ j < (↑p).length + 1,
    decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Proof state:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take j ↑p) + 1 = count D (List.take j ↑p) + 0) = false

Tactic:
have := p.count_D_le_count_U j

Result:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
this : count D (List.take j ↑p) ≤ count U (List.take j ↑p)
⊢ decide (count U (List.take j ↑p) + 1 = count D (List.take j ↑p) + 0) = false

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ j - (↑p).length = 0

Tactic:
omega

Result:
no goals

Proof state:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
this : count D (List.take j ↑p) ≤ count U (List.take j ↑p)
⊢ decide (count U (List.take j ↑p) + 1 = count D (List.take j ↑p) + 0) = false

Tactic:
simp only [add_zero, decide_eq_false_iff_not, ne_eq]

Result:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
this : count D (List.take j ↑p) ≤ count U (List.take j ↑p)
⊢ ¬count U (List.take j ↑p) + 1 = count D (List.take j ↑p)

Proof state:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ ∀ j < (↑p).length + 1,
    decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
intro j hj

Result:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (↑p).length + 1 + ([].length + 1)

Tactic:
exact Nat.lt_add_one _

Result:
no goals

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (U :: ↑p ++ [D]).length ≤ (↑p).length + 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Tactic:
simp_rw [cons_append, take_succ_cons, count_cons, beq_self_eq_true, ite_true,
  beq_iff_eq, reduceCtorEq, ite_false, take_append_eq_append_take,
  show j - p.toList.length = 0 by omega, take_zero, append_nil]

Result:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
⊢ decide (count U (List.take j ↑p) + 1 = count D (List.take j ↑p) + 0) = false

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length

Tactic:
simp_rw [length_range, u, length_append, length_cons]

Result:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (↑p).length + 1 + ([].length + 1)

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

Tactic:
simp_rw [u, decide_eq_true_eq, getElem_range]

Result:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
      count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) ∧
    ∀ j < (↑p).length + 1,
      decide (count U (List.take (j + 1) (U :: ↑p ++ [D])) = count D (List.take (j + 1) (U :: ↑p ++ [D]))) = false

Proof state:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ p.nest.firstReturn = (↑p).length + 1

Tactic:
rw [firstReturn, findIdx_eq]

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

p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ (↑p).length + 1 < (range (↑p.nest).length).length

Proof state:
case left
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ count U (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D])) =
    count D (List.take ((↑p).length + 1 + 1) (U :: ↑p ++ [D]))

Tactic:
rw [take_of_length_le (by simp), ← u, p.nest.count_U_eq_count_D]

Result:
no goals

Proof state:
p : DyckWord
⊢ p.nest.firstReturn = (↑p).length + 1

Tactic:
have u : p.nest.toList = U :: p.toList ++ [D] := rfl

Result:
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
⊢ p.nest.firstReturn = (↑p).length + 1

Proof state:
case right
p : DyckWord
u : ↑p.nest = U :: ↑p ++ [D]
j : ℕ
hj : j < (↑p).length + 1
this : count D (List.take j ↑p) ≤ count U (List.take j ↑p)
⊢ ¬count U (List.take j ↑p) + 1 = count D (List.take j ↑p)

Tactic:
omega

Result:
no goals