awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
inl :
  ∀ (hi : i = 0),
    count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count D (List.take i [U]) ≤
      count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U (List.take i [U])
⊢ count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U (List.take i [U])
have inr : ∀ (hi : i > 0),
  count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U (List.take i [U])
Tactic: rcases i.eq_zero_or_pos with hi | hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ [U].length ≤ i
have rwa : 1 ≤ i
Tactic: rwa [length_singleton]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count D (List.take i [U]) ≤
    count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U (List.take i [U])
have inr : (count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + if U = D then 1 else 0) ≤
  count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U [U]
Tactic: rw [take_of_length_le (show [U].length ≤ i by rwa [length_singleton]), count_singleton']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : i > 0
⊢ count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + 0 ≤
    count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U [U]
have inr : 0 + count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) ≤
  count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U [U]
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < (↑p.nest : List DyckStep).length
⊢ count D (List.take i (↑p.nest : List DyckStep)) < count U (List.take i (↑p.nest : List DyckStep))
have ub₁ : i < 1 + (↑p : List DyckStep).length + 1
Tactic: simp_rw [nest, length_append, length_singleton] at ub ⊢
Cleared hypotheses: ub
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p : List DyckStep).length + 1
⊢ count D (List.take i ([U] ++ (↑p : List DyckStep) ++ [D])) <
    count U (List.take i ([U] ++ (↑p : List DyckStep) ++ [D]))
have rw : count D (List.take (i - 1) (↑p : List DyckStep)) ≤ count U (List.take (i - 1) (↑p : List DyckStep))
Tactic: rw [take_append_of_le_length (by rw [singleton_append, length_cons]; lia),
    take_append, take_of_length_le (by rw [length_singleton]; lia),
    length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
    Nat.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
⊢ count U (↑p : List DyckStep).dropLast.tail = count D (↑p : List DyckStep).dropLast.tail
have this : count U (↑p : List DyckStep) = count D (↑p : List DyckStep)
Tactic: have := p.count_U_eq_count_D
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
this : count U (↑p : List DyckStep) = count D (↑p : List DyckStep)
⊢ count U (↑p : List DyckStep).dropLast.tail = count D (↑p : List DyckStep).dropLast.tail
have this₁ : (count U (↑p : List DyckStep).dropLast.tail + if (U == U) = true then 1 else 0) + count U [D] =
  count D (U :: (↑p : List DyckStep).dropLast.tail ++ [D])
Tactic: rw [← cons_tail_dropLast_concat hn.1, count_append, count_cons] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
h : p ≠ 0
hn : p.IsNested
i : ℕ
⊢ count D (List.take i (↑p : List DyckStep).dropLast.tail) ≤ count U (List.take i (↑p : List DyckStep).dropLast.tail)
have h₁ : (↑p : List DyckStep) ≠ []
Tactic: replace h := toList_ne_nil.mpr hn.1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
⊢ List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
have nil : ∀ (count_U_eq_count_D : count U [] = count D [])
  (count_D_le_count_U : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i []))
  (hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U }.IsNested)
  (h :
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
        List DyckStep) ≠
      []),
  List.take 1
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
            DyckWord } :
        List DyckStep) =
    [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
            List DyckStep).head
        h]
Tactic: rcases p with - | -
Cleared hypotheses: p, hn, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
nil :
  ∀ (count_U_eq_count_D : count U [] = count D [])
    (count_D_le_count_U : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i []))
    (hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U }.IsNested)
    (h :
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
              DyckWord } :
          List DyckStep) ≠
        []),
    List.take 1
        (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
              DyckWord } :
          List DyckStep) =
      [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
              List DyckStep).head
          h]
⊢ List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
have cons : ∀ (head : DyckStep) (tail : List DyckStep) (count_U_eq_count_D : count U (head :: tail) = count D (head :: tail))
  (count_D_le_count_U : ∀ (i : ℕ), count D (List.take i (head :: tail)) ≤ count U (List.take i (head :: tail)))
  (h :
    (↑{ toList := head :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
            DyckWord } :
        List DyckStep) ≠
      []),
  List.take 1
      (↑{ toList := head :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
            DyckWord } :
        List DyckStep) =
    [(↑{ toList := head :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
            List DyckStep).head
        h]
Tactic: rcases p with - | -
Cleared hypotheses: p, hn, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
⊢ count D (List.take i (↑p : List DyckStep).dropLast.tail) ≤ count U (List.take i (↑p : List DyckStep).dropLast.tail)
have l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
Tactic: have l1 : p.toList.take 1 = [p.toList.head h] := by rcases p with - | - <;> tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
⊢ (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
have nil : ∀ (count_U_eq_count_D : count U [] = count D [])
  (count_D_le_count_U : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i []))
  (hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U }.IsNested)
  (h :
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
        List DyckStep) ≠
      [])
  (l1 :
    List.take 1
        (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
              DyckWord } :
          List DyckStep) =
      [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
              List DyckStep).head
          h]),
  (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
Tactic: rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
Cleared hypotheses: p, hn, h, l1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
nil :
  ∀ (count_U_eq_count_D : count U [] = count D [])
    (count_D_le_count_U : ∀ (i : ℕ), count D (List.take i []) ≤ count U (List.take i []))
    (hn : { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U }.IsNested)
    (h :
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
              DyckWord } :
          List DyckStep) ≠
        [])
    (l1 :
      List.take 1
          (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
                DyckWord } :
            List DyckStep) =
        [(↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
                List DyckStep).head
            h]),
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep).length -
        1 =
      (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
                    DyckWord } :
                List DyckStep).length -
            1 -
          1 +
        1
⊢ (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
have cons : ∀ (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 : DyckWord } :
        List DyckStep) ≠
      [])
  (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 :
              DyckWord } :
          List DyckStep) =
      [(↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } :
              List DyckStep).head
          h]),
  (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [s], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
Tactic: rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
Cleared hypotheses: p, hn, h, l1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
q : DyckWord
i : ℕ
s : DyckStep
bal : 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 := bal, count_D_le_count_U := count_D_le_count_U }.IsNested
h :
  (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } : List DyckStep) ≠
    []
l1 :
  List.take 1
      (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
        List DyckStep) =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head h]
⊢ (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
have cons : ∀ (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 : DyckWord } :
        List DyckStep) ≠
      [])
  (l1 :
    List.take 1
        (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep) =
      [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head
          h]),
  (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
Tactic: cases s
Cleared hypotheses: s, bal, count_D_le_count_U, hn, h, l1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
q : DyckWord
i : ℕ
s : DyckStep
bal : 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 := bal, count_D_le_count_U := count_D_le_count_U }.IsNested
h :
  (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } : List DyckStep) ≠
    []
l1 :
  List.take 1
      (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
        List DyckStep) =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head h]
cons :
  ∀ (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 : DyckWord } :
          List DyckStep) ≠
        [])
    (l1 :
      List.take 1
          (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep) =
        [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head
            h]),
    (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep).length -
        1 =
      (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
                List DyckStep).length -
            1 -
          1 +
        1
⊢ (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
have cons₁ : ∀ (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 : DyckWord } :
        List DyckStep) ≠
      [])
  (l1 :
    List.take 1
        (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep) =
      [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head
          h]),
  (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).length -
      1 =
    (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
              List DyckStep).length -
          1 -
        1 +
      1
Tactic: cases s
Cleared hypotheses: s, bal, count_D_le_count_U, hn, h, l1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
⊢ count D (List.take i (↑p : List DyckStep).dropLast.tail) ≤ count U (List.take i (↑p : List DyckStep).dropLast.tail)
have l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
Tactic: 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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
⊢ count D (List.take i (↑p : List DyckStep).dropLast.tail) ≤ count U (List.take i (↑p : List DyckStep).dropLast.tail)
have rw : count D (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))) ≤
  count U (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)))
Tactic: rw [← drop_one, take_drop, dropLast_eq_take, take_take]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)))
have ub : min (1 + i) ((↑p : List DyckStep).length - 1) < (↑p : List DyckStep).length
Tactic: 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'))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
ub : min (1 + i) ((↑p : List DyckStep).length - 1) < (↑p : List DyckStep).length
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)))
have lb : 0 < min (1 + i) ((↑p : List DyckStep).length - 1)
Tactic: have lb : 0 < min (1 + i) (p.toList.length - 1) := by omega
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
ub : min (1 + i) ((↑p : List DyckStep).length - 1) < (↑p : List DyckStep).length
lb : 0 < min (1 + i) ((↑p : List DyckStep).length - 1)
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)))
have eq : count D (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)) <
  count U (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))
Tactic: have eq := hn.2 lb ub
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
ub : min (1 + i) ((↑p : List DyckStep).length - 1) < (↑p : List DyckStep).length
lb : 0 < min (1 + i) ((↑p : List DyckStep).length - 1)
eq :
  count D (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)) <
    count U (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))
⊢ count D (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep))) ≤
    count U (List.drop 1 (List.take (min (1 + i) ((↑p : List DyckStep).length - 1)) (↑p : List DyckStep)))
have set : let j := min (1 + i) ((↑p : List DyckStep).length - 1);
∀ (ub : j < (↑p : List DyckStep).length) (lb : 0 < j)
  (eq : count D (List.take j (↑p : List DyckStep)) < count U (List.take j (↑p : List DyckStep))),
  count D (List.drop 1 (List.take j (↑p : List DyckStep))) ≤ count U (List.drop 1 (List.take j (↑p : List DyckStep)))
Tactic: set j := min (1 + i) (p.toList.length - 1)
Cleared hypotheses: ub, lb, eq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p : List DyckStep).length - 1)
ub : j < (↑p : List DyckStep).length
lb : 0 < j
eq : count D (List.take j (↑p : List DyckStep)) < count U (List.take j (↑p : List DyckStep))
⊢ count D (List.drop 1 (List.take j (↑p : List DyckStep))) ≤ count U (List.drop 1 (List.take j (↑p : List DyckStep)))
have eq₁ : count D [U] + count D (List.drop 1 (List.take j (↑p : List DyckStep))) <
  count U [U] + count U (List.drop 1 (List.take j (↑p : List DyckStep)))
Tactic: rw [← (p.toList.take j).take_append_drop 1, count_append, count_append, take_take,
      min_eq_left (by lia), l1, head_eq_U] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
hn : p.IsNested
i : ℕ
h : (↑p : List DyckStep) ≠ []
l1 : List.take 1 (↑p : List DyckStep) = [(↑p : List DyckStep).head h]
l3 : (↑p : List DyckStep).length - 1 = (↑p : List DyckStep).length - 1 - 1 + 1
j : ℕ := min (1 + i) ((↑p : List DyckStep).length - 1)
ub : j < (↑p : List DyckStep).length
lb : 0 < j
eq :
  count D [U] + count D (List.drop 1 (List.take j (↑p : List DyckStep))) <
    count U [U] + count U (List.drop 1 (List.take j (↑p : List DyckStep)))
⊢ count D (List.drop 1 (List.take j (↑p : List DyckStep))) ≤ count U (List.drop 1 (List.take j (↑p : List DyckStep)))
have eq₁ : (if U = D then 1 else 0) + count D (List.drop 1 (List.take j (↑p : List DyckStep))) <
  1 + count U (List.drop 1 (List.take j (↑p : List DyckStep)))
Tactic: simp only [count_singleton', ite_true] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ p.nest.denest ⋯ = p
have simp_rw : ([U] ++ (↑p : List DyckStep)).tail = (↑p : List DyckStep)
Tactic: simp_rw [nest, denest, DyckWord.ext_iff, dropLast_concat]