awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
e_val : a = 0
e_neg : b = 0
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
⊢ a = 0

Tactic:
toList_eq_nil.mp ha

Premises used: DyckWord.toList_eq_nil, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
⊢ a = 0

Tactic:
exact toList_eq_nil.mp ha

Premises used: DyckWord.toList_eq_nil, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
⊢ b = 0

Tactic:
toList_eq_nil.mp hb

Premises used: DyckWord.toList_eq_nil, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
⊢ b = 0

Tactic:
exact toList_eq_nil.mp hb

Premises used: DyckWord.toList_eq_nil, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
nil :
  ∀ (count_U_eq_count_D : count U [] = count D [])
    (count_D_le_count_U : ∀ (i : ℕ), count D (take i []) ≤ count U (take i []))
    (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) ≠
        []),
    (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep).head
        h =
      U
cons :
  ∀ (s : DyckStep) (tail : List DyckStep) (count_U_eq_count_D : count U (s :: tail) = count D (s :: tail))
    (count_D_le_count_U : ∀ (i : ℕ), count D (take i (s :: tail)) ≤ count U (take i (s :: tail)))
    (h :
      (↑{ toList := s :: 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 := s :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
                DyckWord } :
            List DyckStep).head
        h =
      U
⊢ (↑p : List DyckStep).head h = U

Tactic:
rcases p with - | s
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
count_U_eq_count_D : count U [] = count D []
count_D_le_count_U : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
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) ≠
    []
⊢ (↑{ toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).head
      h =
    U

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
s : DyckStep
tail : List DyckStep
count_U_eq_count_D : count U (s :: tail) = count D (s :: tail)
count_D_le_count_U : ∀ (i : ℕ), count D (take i (s :: tail)) ≤ count U (take i (s :: tail))
h :
  (↑{ toList := s :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
          DyckWord } :
      List DyckStep) ≠
    []
cons : s = U
⊢ (↑{ toList := s :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
              DyckWord } :
          List DyckStep).head
      h =
    U

Tactic:
rw [head_cons]

Premises used: List.head_cons
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
s : DyckStep
tail : List DyckStep
count_U_eq_count_D : count U (s :: tail) = count D (s :: tail)
count_D_le_count_U : ∀ (i : ℕ), count D (take i (s :: tail)) ≤ count U (take i (s :: tail))
h :
  (↑{ toList := s :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U :
          DyckWord } :
      List DyckStep) ≠
    []
cons : ∀ (f : ¬s = U), False
⊢ s = U

Tactic:
by_contra f
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
s : DyckStep
tail : List DyckStep
count_U_eq_count_D : count U (s :: tail) = count D (s :: tail)
nonneg : ∀ (i : ℕ), count D (take i (s :: tail)) ≤ count U (take i (s :: tail))
h :
  (↑{ toList := s :: tail, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := nonneg : DyckWord } :
      List DyckStep) ≠
    []
f : ¬s = U
⊢ False

Tactic:
simpa [s.dichotomy.resolve_left f] using nonneg 1

Premises used: DyckStep.dichotomy, Or.resolve_left, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
by_contra : ∀ (f : ¬(↑p : List DyckStep).getLast h = D), False
⊢ (↑p : List DyckStep).getLast h = D

Tactic:
by_contra f
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
⊢ count U (↑p : List DyckStep) = count D (↑p : List DyckStep)

Tactic:
have s := p.count_U_eq_count_D
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
s : count U (↑p : List DyckStep) = count D (↑p : List DyckStep)
⊢ count U ((↑p : List DyckStep).dropLast ++ [U]) = count D ((↑p : List DyckStep).dropLast ++ [U])

Tactic:
rw [← dropLast_append_getLast h, (dichotomy _).resolve_right f] at s

Premises used: DyckStep.dichotomy, Or.resolve_right, List.dropLast_append_getLast
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
s : count U ((↑p : List DyckStep).dropLast ++ [U]) = count D ((↑p : List DyckStep).dropLast ++ [U])
⊢ count U (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 1 =
    count D (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 0

Tactic:
simp_rw [dropLast_eq_take, count_append, count_singleton', ite_true, reduceCtorEq, ite_false] at s

Premises used: reduceCtorEq, ite_false, List.dropLast_eq_take, ite_true, List.count_singleton', List.count_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
s :
  count U (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 1 =
    count D (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 0
⊢ count D (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) ≤
    count U (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep))

Tactic:
have := p.count_D_le_count_U (p.toList.length - 1)
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
s :
  count U (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 1 =
    count D (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) + 0
this :
  count D (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep)) ≤
    count U (take ((↑p : List DyckStep).length - 1) (↑p : List DyckStep))
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
⊢ (↑p : List DyckStep) ≠ []

Tactic:
have h' := toList_ne_nil.mpr h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
nil :
  ∀ (count_U_eq_count_D : count U [] = count D [])
    (count_D_le_count_U : ∀ (i : ℕ), count D (take i []) ≤ count U (take i []))
    (h :
      { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠
        0)
    (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) ≠
        []),
    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).dropLast =
      [(↑{ 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']
cons :
  ∀ (s : DyckStep) (count_U_eq_count_D : count U [s] = count D [s])
    (count_D_le_count_U : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s]))
    (h :
      { toList := [s], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠
        0)
    (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) ≠
        []),
    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).dropLast =
      [(↑{ 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']
cons₁ :
  ∀ (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 (take i (s :: head :: tail)) ≤ count U (take i (s :: head :: tail)))
    (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 : DyckWord } ≠
        0)
    (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 : DyckWord } :
          List DyckStep) ≠
        []),
    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 : DyckWord } :
            List DyckStep).dropLast =
      [(↑{ toList := s :: 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']
⊢ take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']

Tactic:
rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
count_U_eq_count_D : count U [] = count D []
count_D_le_count_U : ∀ (i : ℕ), count D (take i []) ≤ count U (take i [])
h : { toList := [], count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0
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) ≠
    []
⊢ 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).dropLast =
    [(↑{ 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:
tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
s : DyckStep
bal : count U [s] = count D [s]
count_D_le_count_U : ∀ (i : ℕ), count D (take i [s]) ≤ count U (take i [s])
h : { toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0
h' :
  (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } : List DyckStep) ≠
    []
cons :
  ∀ (bal : count U [U] = count D [U]) (count_D_le_count_U : ∀ (i : ℕ), count D (take i [U]) ≤ count U (take i [U]))
    (h : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0)
    (h' :
      (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep) ≠
        []),
    take 1
        (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep).dropLast =
      [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head
          h']
cons₁ :
  ∀ (bal : count U [D] = count D [D]) (count_D_le_count_U : ∀ (i : ℕ), count D (take i [D]) ≤ count U (take i [D]))
    (h : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0)
    (h' :
      (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep) ≠
        []),
    take 1
        (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
            List DyckStep).dropLast =
      [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head
          h']
⊢ take 1
      (↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).dropLast =
    [(↑{ toList := [s], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head h']

Tactic:
cases s
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
bal : count U [U] = count D [U]
count_D_le_count_U : ∀ (i : ℕ), count D (take i [U]) ≤ count U (take i [U])
h : { toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0
h' :
  (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } : List DyckStep) ≠
    []
⊢ take 1
      (↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).dropLast =
    [(↑{ toList := [U], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head h']

Tactic:
simp at bal
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
bal : count U [D] = count D [D]
count_D_le_count_U : ∀ (i : ℕ), count D (take i [D]) ≤ count U (take i [D])
h : { toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } ≠ 0
h' :
  (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } : List DyckStep) ≠
    []
⊢ take 1
      (↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U : DyckWord } :
          List DyckStep).dropLast =
    [(↑{ toList := [D], count_U_eq_count_D := bal, count_D_le_count_U := count_D_le_count_U } : List DyckStep).head h']

Tactic:
simp at bal
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
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 (take i (s :: head :: tail)) ≤ count U (take i (s :: head :: tail))
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 :
      DyckWord } ≠
    0
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 :
          DyckWord } :
      List DyckStep) ≠
    []
⊢ 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 : DyckWord } :
          List DyckStep).dropLast =
    [(↑{ toList := s :: 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:
tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
⊢ take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']

Tactic:
have : p.toList.dropLast.take 1 = [p.toList.head h'] := by
    rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
    · tauto
    · rename_i bal _
      cases s <;> simp at bal
    · tauto
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
this : take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
nth_rw :
  U :: (↑p : List DyckStep).dropLast.tail ++ [D] =
    take 1 (↑p : List DyckStep).dropLast ++ drop 1 (↑p : List DyckStep).dropLast ++ [(↑p : List DyckStep).getLast h']
⊢ U :: (↑p : List DyckStep).dropLast.tail ++ [D] = (↑p : List DyckStep)

Tactic:
nth_rw 2 [← p.toList.dropLast_append_getLast h', ← p.toList.dropLast.take_append_drop 1]

Premises used: List.take_append_drop, List.dropLast, OfNat.ofNat, DyckWord.toList, List.dropLast_append_getLast
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
this : take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
rw : U :: (↑p : List DyckStep).dropLast.tail ++ [D] = [U] ++ (↑p : List DyckStep).dropLast.tail ++ [D]
⊢ U :: (↑p : List DyckStep).dropLast.tail ++ [D] =
    take 1 (↑p : List DyckStep).dropLast ++ drop 1 (↑p : List DyckStep).dropLast ++ [(↑p : List DyckStep).getLast h']

Tactic:
rw [getLast_eq_D, drop_one, this, head_eq_U]

Premises used: DyckWord.getLast_eq_D, DyckWord.head_eq_U, List.drop_one
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
this : take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
⊢ U :: (↑p : List DyckStep).dropLast.tail ++ [D] = [U] ++ (↑p : List DyckStep).dropLast.tail ++ [D]

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
k : ℕ
rw : count D (List.take (min k i) (↑p : List DyckStep)) ≤ count U (List.take (min k i) (↑p : List DyckStep))
⊢ count D (List.take k (List.take i (↑p : List DyckStep))) ≤ count U (List.take k (List.take i (↑p : List DyckStep)))

Tactic:
rw [take_take]

Premises used: List.take_take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
k : ℕ
⊢ count D (List.take (min k i) (↑p : List DyckStep)) ≤ count U (List.take (min k i) (↑p : List DyckStep))

Tactic:
p.count_D_le_count_U (min k i)

Premises used: DyckWord.count_D_le_count_U, Min.min
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
k : ℕ
⊢ count D (List.take (min k i) (↑p : List DyckStep)) ≤ count U (List.take (min k i) (↑p : List DyckStep))

Tactic:
exact p.count_D_le_count_U (min k i)

Premises used: DyckWord.count_D_le_count_U, Min.min
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
⊢ count U (↑p : List DyckStep) = count D (↑p : List DyckStep)

Tactic:
have := p.count_U_eq_count_D
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
this : count U (↑p : List DyckStep) = count D (↑p : List DyckStep)
⊢ count U (List.take i (↑p : List DyckStep)) + count U (List.drop i (↑p : List DyckStep)) =
    count D (List.take i (↑p : List DyckStep)) + count D (List.drop i (↑p : List DyckStep))

Tactic:
rw [← take_append_drop i p.toList, count_append, count_append] at this

Premises used: List.take_append_drop, List.count_append, DyckWord.toList
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
this :
  count U (List.take i (↑p : List DyckStep)) + count U (List.drop i (↑p : List DyckStep)) =
    count D (List.take i (↑p : List DyckStep)) + count D (List.drop i (↑p : List DyckStep))
⊢ count U (List.drop i (↑p : List DyckStep)) = count D (List.drop i (↑p : List DyckStep))

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
k : ℕ
⊢ i = min i (i + k)

Tactic:
omega
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
hi : count U (List.take i (↑p : List DyckStep)) = count D (List.take i (↑p : List DyckStep))
k : ℕ
⊢ count U (List.take i (List.take (i + k) (↑p : List DyckStep))) =
    count D (List.take i (List.take (i + k) (↑p : List DyckStep)))

Tactic:
rw [show i = min i (i + k) by omega, ← take_take] at hi

Premises used: List.take_take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi :
  count U (List.take i (List.take (i + k) (↑p : List DyckStep))) =
    count D (List.take i (List.take (i + k) (↑p : List DyckStep)))
rw : count D (List.take (i + k) (↑p : List DyckStep)) ≤ count U (List.take (i + k) (↑p : List DyckStep))
⊢ count D (List.take k (List.drop i (↑p : List DyckStep))) ≤ count U (List.take k (List.drop i (↑p : List DyckStep)))

Tactic:
rw [take_drop, ← add_le_add_iff_left (((p.toList.take (i + k)).take i).count U),
      ← count_append, hi, ← count_append, take_append_drop]

Premises used: DyckStep.U, add_le_add_iff_left, List.take_append_drop, List.take_drop, List.count, List.count_append, HAdd.hAdd, DyckWord.toList, List.take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi :
  count U (List.take i (List.take (i + k) (↑p : List DyckStep))) =
    count D (List.take i (List.take (i + k) (↑p : List DyckStep)))
⊢ count D (List.take (i + k) (↑p : List DyckStep)) ≤ count U (List.take (i + k) (↑p : List DyckStep))

Tactic:
p.count_D_le_count_U _

Premises used: DyckWord.count_D_le_count_U
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i k : ℕ
hi :
  count U (List.take i (List.take (i + k) (↑p : List DyckStep))) =
    count D (List.take i (List.take (i + k) (↑p : List DyckStep)))
⊢ count D (List.take (i + k) (↑p : List DyckStep)) ≤ count U (List.take (i + k) (↑p : List DyckStep))

Tactic:
exact p.count_D_le_count_U _

Premises used: DyckWord.count_D_le_count_U
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
⊢ count U ([U] ++ (↑p : List DyckStep) ++ [D]) = count D ([U] ++ (↑p : List DyckStep) ++ [D])

Tactic:
simp [p.count_U_eq_count_D]

Premises used: DyckWord.count_U_eq_count_D
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
simp :
  count D (List.take i [U]) + count D (List.take (i - [U].length) (↑p : List DyckStep)) +
      count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) (↑p : List DyckStep)) +
      count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D])
⊢ count D (List.take i ([U] ++ (↑p : List DyckStep) ++ [D])) ≤
    count U (List.take i ([U] ++ (↑p : List DyckStep) ++ [D]))

Tactic:
simp only [take_append, count_append]

Premises used: List.take_append, List.count_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
rw :
  count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count D (List.take i [U]) +
      count D (List.take (i - [U].length) (↑p : List DyckStep)) ≤
    count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) + count U (List.take i [U]) +
      count U (List.take (i - [U].length) (↑p : List DyckStep))
⊢ count D (List.take i [U]) + count D (List.take (i - [U].length) (↑p : List DyckStep)) +
      count D (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D]) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) (↑p : List DyckStep)) +
      count U (List.take (i - ([U] ++ (↑p : List DyckStep)).length) [D])

Tactic:
rw [← add_rotate (count D _), ← add_rotate (count U _)]

Premises used: DyckStep.U, List.count, add_rotate, DyckStep.D