-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma firstReturn_pos : 0 < p.firstReturn

Proof state:
p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ 0 < (range (↑p).length).length

Tactic:
rw [length_range, length_pos]

Result:
p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ ↑p ≠ []

Proof state:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f : count U (List.take 1 (U :: (↑p).dropLast.tail ++ [D])) = count D (List.take 1 (U :: (↑p).dropLast.tail ++ [D]))
⊢ False

Tactic:
simp at f

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
      true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

Tactic:
rw [getElem_range] at f

Result:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

Proof state:
p : DyckWord
h : p ≠ 0
f : p.firstReturn ≤ 0
⊢ False

Tactic:
rw [Nat.le_zero, firstReturn, findIdx_eq] at f

Result:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
      true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ 0 < (range (↑p).length).length

Proof state:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take (0 + 1) ↑p) = count D (List.take (0 + 1) ↑p)) = true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

Tactic:
simp at f

Result:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f : count U (List.take 1 ↑p) = count D (List.take 1 ↑p)
⊢ False

Proof state:
p : DyckWord
h : p ≠ 0
⊢ 0 < p.firstReturn

Tactic:
by_contra! f

Result:
p : DyckWord
h : p ≠ 0
f : p.firstReturn ≤ 0
⊢ False

Proof state:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
      true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ 0 < (range (↑p).length).length

Tactic:
swap

Result:
p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ 0 < (range (↑p).length).length

p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f :
  decide (count U (List.take ((range (↑p).length)[0] + 1) ↑p) = count D (List.take ((range (↑p).length)[0] + 1) ↑p)) =
      true ∧
    ∀ (j : ℕ) (hji : j < 0),
      decide
          (count U (List.take ((range (↑p).length)[j] + 1) ↑p) = count D (List.take ((range (↑p).length)[j] + 1) ↑p)) =
        false
⊢ False

Proof state:
p : DyckWord
h : p ≠ 0
f : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
⊢ ↑p ≠ []

Tactic:
exact toList_ne_nil.mpr h

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f : count U (List.take 1 ↑p) = count D (List.take 1 ↑p)
⊢ False

Tactic:
rw [← p.cons_tail_dropLast_concat h] at f

Result:
p : DyckWord
h : p ≠ 0
f✝ : findIdx (fun i => decide (count U (List.take (i + 1) ↑p) = count D (List.take (i + 1) ↑p))) (range (↑p).length) = 0
f : count U (List.take 1 (U :: (↑p).dropLast.tail ++ [D])) = count D (List.take 1 (U :: (↑p).dropLast.tail ++ [D]))
⊢ False