Lean4
/-- Denest `p`, i.e. `(x)` becomes `x`, given that `p.IsNested`. -/
def denest (hn : p.IsNested) : DyckWord where
toList := p.toList.dropLast.tail
count_U_eq_count_D := by
have := p.count_U_eq_count_D
rw [← cons_tail_dropLast_concat hn.1, count_append, count_cons] at this
simpa using this
count_D_le_count_U
i := by
replace h := toList_ne_nil.mpr hn.1
have l1 : p.toList.take 1 = [p.toList.head h] := by rcases p with - | - <;> tauto
have l3 : p.toList.length - 1 = p.toList.length - 1 - 1 + 1 :=
by
rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
· tauto
· rename_i bal _
cases s <;> simp at bal
· tauto
rw [← drop_one, take_drop, dropLast_eq_take, take_take]
have ub : min (1 + i) (p.toList.length - 1) < p.toList.length :=
(min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos_iff.mpr h).ne'))
have lb : 0 < min (1 + i) (p.toList.length - 1) := by omega
have eq := hn.2 lb ub
set j := min (1 + i) (p.toList.length - 1)
rw [← (p.toList.take j).take_append_drop 1, count_append, count_append, take_take, min_eq_left (by omega), l1,
head_eq_U] at eq
simp only [count_singleton', ite_true] at eq
omega
