awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
v : p.firstReturn < (↑p : List DyckStep).length
⊢ p.firstReturn + 1 - (↑p : List DyckStep).length = 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
v : p.firstReturn < (↑p : List DyckStep).length
neg :
  count U
      (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++
        List.take (p.firstReturn + 1 - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D
      (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++
        List.take (p.firstReturn + 1 - (↑p : List DyckStep).length) (↑q : List DyckStep))
neg₁ :
  count U (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++ List.take 0 (↑q : List DyckStep)) =
    count D (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++ List.take 0 (↑q : List DyckStep))
neg₂ :
  count U (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++ []) =
    count D (List.take (p.firstReturn + 1) (↑p : List DyckStep) ++ [])
neg₃ :
  count U (List.take (p.firstReturn + 1) (↑p : List DyckStep)) =
    count D (List.take (p.firstReturn + 1) (↑p : List DyckStep))
neg₄ neg₅ :
  count D (List.take (p.firstReturn + 1) (↑p : List DyckStep)) =
    count D (List.take (p.firstReturn + 1) (↑p : List DyckStep))
⊢ count U (List.take (p.firstReturn + 1) ((↑p : List DyckStep) ++ (↑q : List DyckStep))) =
    count D (List.take (p.firstReturn + 1) ((↑p : List DyckStep) ++ (↑q : List DyckStep)))

Tactic:
rw [take_append, show p.firstReturn + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil, count_take_firstReturn_add_one h]

Premises used: DyckWord.count_take_firstReturn_add_one, List.take_append, List.take_zero, List.append_nil
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
v : p.firstReturn < (↑p : List DyckStep).length
j : ℕ
hj : j < p.firstReturn
⊢ j + 1 - (↑p : List DyckStep).length = 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
v : p.firstReturn < (↑p : List DyckStep).length
j : ℕ
hj : j < p.firstReturn
neg :
  decide (count U (List.take (j + 1) (↑p : List DyckStep)) = count D (List.take (j + 1) (↑p : List DyckStep))) = false
⊢ decide
      (count U (List.take (j + 1) ((↑p : List DyckStep) ++ (↑q : List DyckStep))) =
        count D (List.take (j + 1) ((↑p : List DyckStep) ++ (↑q : List DyckStep)))) =
    false

Tactic:
rw [take_append, show j + 1 - p.toList.length = 0 by lia,
        take_zero, append_nil]

Premises used: List.take_append, List.take_zero, List.append_nil
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
v : p.firstReturn < (↑p : List DyckStep).length
j : ℕ
hj : j < p.firstReturn
⊢ decide (count U (List.take (j + 1) (↑p : List DyckStep)) = count D (List.take (j + 1) (↑p : List DyckStep))) = false

Tactic:
simpa using (count_D_lt_count_U_of_lt_firstReturn hj).ne'

Premises used: DyckWord.count_D_lt_count_U_of_lt_firstReturn, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
neg : p.firstReturn < (↑p : List DyckStep).length + (↑q : List DyckStep).length
⊢ p.firstReturn < (range (↑(p + q) : List DyckStep).length).length

Tactic:
rw [length_range, u, length_append]

Premises used: List.length_range, List.length_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
⊢ p.firstReturn < (↑p : List DyckStep).length + (↑q : List DyckStep).length

Tactic:
Nat.lt_add_right _ (firstReturn_lt_length h)

Premises used: DyckWord.firstReturn_lt_length, Nat.lt_add_right
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
u : (↑(p + q) : List DyckStep) = (↑p : List DyckStep) ++ (↑q : List DyckStep)
⊢ p.firstReturn < (↑p : List DyckStep).length + (↑q : List DyckStep).length

Tactic:
exact Nat.lt_add_right _ (firstReturn_lt_length h)

Premises used: DyckWord.firstReturn_lt_length, Nat.lt_add_right
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]

Tactic:
have u : p.nest.toList = U :: p.toList ++ [D] := rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
rw :
  decide
        (count U
            (List.take
              (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length)
                  ((↑p : List DyckStep).length + 1) ⋯ +
                1)
              (↑p.nest : List DyckStep)) =
          count D
            (List.take
              (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length)
                  ((↑p : List DyckStep).length + 1) ⋯ +
                1)
              (↑p.nest : List DyckStep))) =
      true ∧
    ∀ (j : ℕ) (hji : j < (↑p : List DyckStep).length + 1),
      decide
          (count U
              (List.take
                (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length) j
                    ⋯ +
                  1)
                (↑p.nest : List DyckStep)) =
            count D
              (List.take
                (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length) j
                    ⋯ +
                  1)
                (↑p.nest : List DyckStep))) =
        false
rw₁ : (↑p : List DyckStep).length + 1 < (range (↑p.nest : List DyckStep).length).length
⊢ p.nest.firstReturn = (↑p : List DyckStep).length + 1

Tactic:
rw [firstReturn, findIdx_eq]

Premises used: List.findIdx_eq, DyckWord.firstReturn
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
simp_rw :
  count U (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) =
      count D (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) ∧
    ∀ (j : ℕ) (hji : j < (↑p : List DyckStep).length + 1),
      decide
          (count U (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D])) =
            count D (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D]))) =
        false
⊢ decide
        (count U
            (List.take
              (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length)
                  ((↑p : List DyckStep).length + 1) ⋯ +
                1)
              (↑p.nest : List DyckStep)) =
          count D
            (List.take
              (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length)
                  ((↑p : List DyckStep).length + 1) ⋯ +
                1)
              (↑p.nest : List DyckStep))) =
      true ∧
    ∀ (j : ℕ) (hji : j < (↑p : List DyckStep).length + 1),
      decide
          (count U
              (List.take
                (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length) j
                    ⋯ +
                  1)
                (↑p.nest : List DyckStep)) =
            count D
              (List.take
                (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (range (↑p.nest : List DyckStep).length) j
                    ⋯ +
                  1)
                (↑p.nest : List DyckStep))) =
        false

Tactic:
simp_rw [u, decide_eq_true_eq, getElem_range]

Premises used: List.getElem_range, decide_eq_true_eq
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
left :
  count U (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) =
    count D (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D]))
right :
  ∀ (j : ℕ) (hji : j < (↑p : List DyckStep).length + 1),
    decide
        (count U (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D])) =
          count D (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D]))) =
      false
⊢ count U (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) =
      count D (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) ∧
    ∀ (j : ℕ) (hji : j < (↑p : List DyckStep).length + 1),
      decide
          (count U (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D])) =
            count D (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D]))) =
        false

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
⊢ (U :: (↑p : List DyckStep) ++ [D]).length ≤ (↑p : List DyckStep).length + 1 + 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
left : count U (U :: (↑p : List DyckStep) ++ [D]) = count D (U :: (↑p : List DyckStep) ++ [D])
left₁ : count U (↑p.nest : List DyckStep) = count D (↑p.nest : List DyckStep)
left₂ left₃ : count D (↑p.nest : List DyckStep) = count D (↑p.nest : List DyckStep)
⊢ count U (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D])) =
    count D (List.take ((↑p : List DyckStep).length + 1 + 1) (U :: (↑p : List DyckStep) ++ [D]))

Tactic:
rw [take_of_length_le (by simp), ← u, p.nest.count_U_eq_count_D]

Premises used: DyckWord.count_U_eq_count_D, List.take_of_length_le, DyckWord.nest
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
j : ℕ
hj : j < (↑p : List DyckStep).length + 1
⊢ j - (↑p : List DyckStep).length = 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
j : ℕ
hj : j < (↑p : List DyckStep).length + 1
right : decide (count U (List.take j (↑p : List DyckStep)) + 1 = count D (List.take j (↑p : List DyckStep)) + 0) = false
⊢ decide
      (count U (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D])) =
        count D (List.take (j + 1) (U :: (↑p : List DyckStep) ++ [D]))) =
    false

Tactic:
simp_rw [cons_append, take_succ_cons, count_cons, beq_self_eq_true, ite_true,
        beq_iff_eq, reduceCtorEq, ite_false, take_append,
        show j - p.toList.length = 0 by lia, take_zero, append_nil]

Premises used: reduceCtorEq, List.take_succ_cons, ite_false, beq_iff_eq, List.take_append, List.take_zero, List.count_cons, ite_true, List.append_nil, beq_self_eq_true, List.cons_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
j : ℕ
hj : j < (↑p : List DyckStep).length + 1
⊢ count D (List.take j (↑p : List DyckStep)) ≤ count U (List.take j (↑p : List DyckStep))

Tactic:
have := p.count_D_le_count_U j
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
j : ℕ
hj : j < (↑p : List DyckStep).length + 1
this : count D (List.take j (↑p : List DyckStep)) ≤ count U (List.take j (↑p : List DyckStep))
right : ¬count U (List.take j (↑p : List DyckStep)) + 1 = count D (List.take j (↑p : List DyckStep))
⊢ decide (count U (List.take j (↑p : List DyckStep)) + 1 = count D (List.take j (↑p : List DyckStep)) + 0) = false

Tactic:
simp only [add_zero, decide_eq_false_iff_not, ne_eq]

Premises used: ne_eq, decide_eq_false_iff_not, add_zero
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
j : ℕ
hj : j < (↑p : List DyckStep).length + 1
this : count D (List.take j (↑p : List DyckStep)) ≤ count U (List.take j (↑p : List DyckStep))
⊢ ¬count U (List.take j (↑p : List DyckStep)) + 1 = count D (List.take j (↑p : List DyckStep))

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
simp_rw : (↑p : List DyckStep).length + 1 < (↑p : List DyckStep).length + 1 + (length (α := DyckStep) [] + 1)
⊢ (↑p : List DyckStep).length + 1 < (range (↑p.nest : List DyckStep).length).length

Tactic:
simp_rw [length_range, u, length_append, length_cons]

Premises used: List.length_cons, List.length_range, List.length_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
⊢ (↑p : List DyckStep).length + 1 < (↑p : List DyckStep).length + 1 + (length (α := DyckStep) [] + 1)

Tactic:
Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
u : (↑p.nest : List DyckStep) = U :: (↑p : List DyckStep) ++ [D]
⊢ (↑p : List DyckStep).length + 1 < (↑p : List DyckStep).length + 1 + (length (α := DyckStep) [] + 1)

Tactic:
exact Nat.lt_add_one _

Premises used: Nat.lt_add_one
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
rw :
  (↑{ toList := List.take (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ :
          DyckWord } :
      List DyckStep) ≠
    []
⊢ p.take (p.firstReturn + 1) ⋯ ≠ 0

Tactic:
rw [← toList_ne_nil, take]

Premises used: DyckWord.toList_ne_nil, DyckWord.take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
⊢ (↑{ toList := List.take (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ :
          DyckWord } :
      List DyckStep) ≠
    []

Tactic:
simpa using toList_ne_nil.mpr h

Premises used: Iff.mpr, DyckWord.toList_ne_nil
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < (↑(p.take (p.firstReturn + 1) ⋯) : List DyckStep).length
simp :
  ∀ (ub : i < p.firstReturn + 1 ∧ i < (↑p : List DyckStep).length),
    count D (List.take i (List.take (p.firstReturn + 1) (↑p : List DyckStep))) <
      count U (List.take i (List.take (p.firstReturn + 1) (↑p : List DyckStep)))
⊢ count D (List.take i (↑(p.take (p.firstReturn + 1) ⋯) : List DyckStep)) <
    count U (List.take i (↑(p.take (p.firstReturn + 1) ⋯) : List DyckStep))

Tactic:
simp only [take, length_take, lt_min_iff] at ub ⊢

Premises used: List.length_take, lt_min_iff, DyckWord.take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1 ∧ i < (↑p : List DyckStep).length
⊢ i < p.firstReturn + 1

Tactic:
replace ub := ub.1
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1
rw : count D (List.take i (↑p : List DyckStep)) < count U (List.take i (↑p : List DyckStep))
⊢ count D (List.take i (List.take (p.firstReturn + 1) (↑p : List DyckStep))) <
    count U (List.take i (List.take (p.firstReturn + 1) (↑p : List DyckStep)))

Tactic:
rw [take_take, min_eq_left ub.le]

Premises used: LT.lt.le, min_eq_left, List.take_take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1
⊢ i = i - 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 + 1 < p.firstReturn + 1
⊢ i = i - 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < p.firstReturn + 1
rw :
  ∀ (ub : i - 1 + 1 < p.firstReturn + 1),
    count D (List.take (i - 1 + 1) (↑p : List DyckStep)) < count U (List.take (i - 1 + 1) (↑p : List DyckStep))
⊢ count D (List.take i (↑p : List DyckStep)) < count U (List.take i (↑p : List DyckStep))

Tactic:
rw [show i = i - 1 + 1 by lia] at ub ⊢
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 + 1 < p.firstReturn + 1
⊢ i - 1 < p.firstReturn

Tactic:
rw [Nat.add_lt_add_iff_right] at ub

Premises used: Nat.add_lt_add_iff_right
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 < p.firstReturn
⊢ count D (List.take (i - 1 + 1) (↑p : List DyckStep)) < count U (List.take (i - 1 + 1) (↑p : List DyckStep))

Tactic:
count_D_lt_count_U_of_lt_firstReturn ub

Premises used: DyckWord.count_D_lt_count_U_of_lt_firstReturn
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h_1 : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i - 1 < p.firstReturn
⊢ count D (List.take (i - 1 + 1) (↑p : List DyckStep)) < count U (List.take (i - 1 + 1) (↑p : List DyckStep))

Tactic:
exact count_D_lt_count_U_of_lt_firstReturn ub

Premises used: DyckWord.count_D_lt_count_U_of_lt_firstReturn
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
⊢ insidePart 0 = 0

Tactic:
simp [insidePart]

Premises used: DyckWord.insidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
⊢ outsidePart 0 = 0

Tactic:
simp [outsidePart]

Premises used: DyckWord.outsidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
simp_rw :
  (↑({ toList := List.take (p.firstReturn + 1) (↑(p + q) : List DyckStep), count_U_eq_count_D := ⋯,
              count_D_le_count_U := ⋯ : DyckWord }.denest
          ⋯) :
      List DyckStep) =
    (↑({ toList := List.take (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯,
              count_D_le_count_U := ⋯ }.denest
          ⋯) :
      List DyckStep)
⊢ (p + q).insidePart = p.insidePart

Tactic:
simp_rw [insidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
    DyckWord.ext_iff, take]

Premises used: add_eq_zero', dite_false, ite_false, false_and, DyckWord.firstReturn_add, DyckWord.ext_iff, DyckWord.insidePart, DyckWord.take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
e_self : List.take (p.firstReturn + 1) (↑(p + q) : List DyckStep) = List.take (p.firstReturn + 1) (↑p : List DyckStep)
⊢ (↑({ toList := List.take (p.firstReturn + 1) (↑(p + q) : List DyckStep), count_U_eq_count_D := ⋯,
              count_D_le_count_U := ⋯ : DyckWord }.denest
          ⋯) :
      List DyckStep) =
    (↑({ toList := List.take (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯,
              count_D_le_count_U := ⋯ }.denest
          ⋯) :
      List DyckStep)

Tactic:
congr 3
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) (↑(p + q) : List DyckStep) = List.take (p.firstReturn + 1) (↑p : List DyckStep)

Tactic:
take_append_of_le_length (firstReturn_lt_length h)

Premises used: List.take_append_of_le_length, DyckWord.firstReturn_lt_length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
⊢ List.take (p.firstReturn + 1) (↑(p + q) : List DyckStep) = List.take (p.firstReturn + 1) (↑p : List DyckStep)

Tactic:
exact take_append_of_le_length (firstReturn_lt_length h)

Premises used: List.take_append_of_le_length, DyckWord.firstReturn_lt_length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
simp_rw :
  List.drop (p.firstReturn + 1) (↑(p + q) : List DyckStep) =
    (↑({ toList := List.drop (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯,
            count_D_le_count_U := ⋯ : DyckWord } +
          q) :
      List DyckStep)
⊢ (p + q).outsidePart = p.outsidePart + q

Tactic:
simp_rw [outsidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
    DyckWord.ext_iff, drop]

Premises used: add_eq_zero', dite_false, ite_false, false_and, DyckWord.firstReturn_add, DyckWord.outsidePart, DyckWord.ext_iff, DyckWord.drop
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
⊢ List.drop (p.firstReturn + 1) (↑(p + q) : List DyckStep) =
    (↑({ toList := List.drop (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯,
            count_D_le_count_U := ⋯ : DyckWord } +
          q) :
      List DyckStep)

Tactic:
drop_append_of_le_length (firstReturn_lt_length h)

Premises used: DyckWord.firstReturn_lt_length, List.drop_append_of_le_length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
⊢ List.drop (p.firstReturn + 1) (↑(p + q) : List DyckStep) =
    (↑({ toList := List.drop (p.firstReturn + 1) (↑p : List DyckStep), count_U_eq_count_D := ⋯,
            count_D_le_count_U := ⋯ : DyckWord } +
          q) :
      List DyckStep)

Tactic:
exact drop_append_of_le_length (firstReturn_lt_length h)

Premises used: DyckWord.firstReturn_lt_length, List.drop_append_of_le_length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
simp_rw : (p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯).denest ⋯ = p
⊢ p.nest.insidePart = p

Tactic:
simp_rw [insidePart, nest_ne_zero, dite_false, firstReturn_nest]

Premises used: DyckWord.nest_ne_zero, dite_false, DyckWord.firstReturn_nest, DyckWord.insidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ p.nest.denest ⋯ = p

Tactic:
p.denest_nest

Premises used: DyckWord.denest_nest
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯ = p.nest
⊢ (p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯).denest ⋯ = p

Tactic:
convert! p.denest_nest

Premises used: DyckWord.denest_nest
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑(p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯) : List DyckStep) = (↑p.nest : List DyckStep)
⊢ p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯ = p.nest

Tactic:
rw [DyckWord.ext_iff]

Premises used: DyckWord.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p.nest : List DyckStep).length ≤ (↑p : List DyckStep).length + 1 + 1
⊢ (↑(p.nest.take ((↑p : List DyckStep).length + 1 + 1) ⋯) : List DyckStep) = (↑p.nest : List DyckStep)

Tactic:
apply take_of_length_le

Premises used: List.take_of_length_le
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : 1 + (↑p : List DyckStep).length + 1 ≤ (↑p : List DyckStep).length + 1 + 1
⊢ (↑p.nest : List DyckStep).length ≤ (↑p : List DyckStep).length + 1 + 1

Tactic:
simp_rw [nest, length_append, length_singleton]

Premises used: List.length_singleton, List.length_append, DyckWord.nest
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ 1 + (↑p : List DyckStep).length + 1 ≤ (↑p : List DyckStep).length + 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
simp_rw : (↑(p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯) : List DyckStep) = (↑p : List DyckStep)
⊢ p.insidePart.nest + p.outsidePart = p

Tactic:
simp_rw [insidePart, outsidePart, h, dite_false, nest_denest, DyckWord.ext_iff]

Premises used: dite_false, DyckWord.nest_denest, DyckWord.outsidePart, DyckWord.ext_iff, DyckWord.insidePart
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
⊢ (↑(p.take (p.firstReturn + 1) ⋯ + p.drop (p.firstReturn + 1) ⋯) : List DyckStep) = (↑p : List DyckStep)

Tactic:
apply take_append_drop

Premises used: List.take_append_drop