Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case cons.nil.U
q : DyckWord
i : ℕ
bal : count U [U] = count D [U]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [U]) ≤ count U (List.take i [U])
hn : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

pp: case cons.nil.D
q : DyckWord
i : ℕ
bal : count U [D] = count D [D]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [D]) ≤ count U (List.take i [D])
hn : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

Tactic:
<;>

Goal state after:
case cons.nil.U
q : DyckWord
i : ℕ
bal : count U [U] = count D [U]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [U]) ≤ count U (List.take i [U])
hn : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1

case cons.nil.D
q : DyckWord
i : ℕ
bal : count U [D] = count D [D]
count_D_le_count_U✝ : ∀ (i : ℕ), count D (List.take i [D]) ≤ count U (List.take i [D])
hn : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }.IsNested
h : ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } ≠ []
l1 :
  List.take 1 ↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ } =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).head h]
⊢ (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 =
    (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U✝ }).length - 1 - 1 + 1