Module: Mathlib.Combinatorics.Enumerative.DyckWord

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

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

Tactic:
· rename_i bal _
        cases s <;> simp at bal

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