awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q r : DyckWord
h : Eq (α := DyckWord) ((fun (x : DyckWord) ↦ x + p) q) ((fun (x : DyckWord) ↦ x + p) r)
⊢ q = r
have rw : ∀ (h : (↑((fun (x : DyckWord) ↦ x + p) q) : List DyckStep) = (↑((fun (x : DyckWord) ↦ x + p) r) : List DyckStep)),
  (↑q : List DyckStep) = (↑r : List DyckStep)
Tactic: rw [DyckWord.ext_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ (↑p : List DyckStep) = [] ↔ p = 0
have rw : (↑p : List DyckStep) = [] ↔ (↑p : List DyckStep) = (↑0 : List DyckStep)
Tactic: rw [DyckWord.ext_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p_1 q : DyckWord
p : AddUnits DyckWord
⊢ p = default
have obtain : ∀ (a b : DyckWord) (h : a + b = 0) (neg_val : b + a = 0),
  { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
Tactic: obtain ⟨a, b, h, -⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
have ha : (↑a : List DyckStep) = []
Tactic: obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
have hb : (↑b : List DyckStep) = []
Tactic: obtain ⟨ha, hb⟩ := append_eq_nil_iff.mp (toList_eq_nil.mpr h)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q a b : DyckWord
h : a + b = 0
neg_val : b + a = 0
ha : (↑a : List DyckStep) = []
hb : (↑b : List DyckStep) = []
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
have e_val : a = 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ { val := a, neg := b, val_neg := h, neg_val := neg_val : AddUnits DyckWord } = default
have e_neg : b = 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
⊢ (↑p : List DyckStep).head h = U
have 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
Tactic: rcases p with - | s
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ (↑p : List DyckStep).head h = U
have 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
Tactic: rcases p with - | s
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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) ≠
    []
⊢ (↑{ 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
have cons : s = U
Tactic: rw [head_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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) ≠
    []
⊢ s = U
have cons : ∀ (f : ¬s = U), False
Tactic: by_contra f
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
⊢ (↑p : List DyckStep).getLast h = D
have by_contra : ∀ (f : ¬(↑p : List DyckStep).getLast h = D), False
Tactic: by_contra f
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p : DyckWord
h : (↑p : List DyckStep) ≠ []
f : ¬(↑p : List DyckStep).getLast h = D
⊢ False
have s : count U (↑p : List DyckStep) = count D (↑p : List DyckStep)
Tactic: have s := p.count_U_eq_count_D
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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)
⊢ False
have s₁ : 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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])
⊢ False
have 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
Tactic: simp_rw [dropLast_eq_take, count_append, count_singleton', ite_true, reduceCtorEq, ite_false] at s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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
⊢ False
have this : 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)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p : DyckWord
h : p ≠ 0
⊢ U :: (↑p : List DyckStep).dropLast.tail ++ [D] = (↑p : List DyckStep)
have h' : (↑p : List DyckStep) ≠ []
Tactic: have h' := toList_ne_nil.mpr h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
⊢ take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
have 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']
Tactic: rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
Cleared hypotheses: p, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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']
⊢ take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
have 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']
Tactic: rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
Cleared hypotheses: p, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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']
⊢ take 1 (↑p : List DyckStep).dropLast = [(↑p : List DyckStep).head h']
have 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']
Tactic: rcases p with - | ⟨s, ⟨- | ⟨t, r⟩⟩⟩
Cleared hypotheses: p, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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) ≠
    []
⊢ 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']
have 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']
Tactic: cases s
Cleared hypotheses: s, bal, count_D_le_count_U, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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']
⊢ 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']
have 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']
Tactic: cases s
Cleared hypotheses: s, bal, count_D_le_count_U, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p : DyckWord
h : p ≠ 0
h' : (↑p : List DyckStep) ≠ []
⊢ U :: (↑p : List DyckStep).dropLast.tail ++ [D] = (↑p : List DyckStep)
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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] = (↑p : List DyckStep)
have 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']
Tactic: nth_rw 2 [← p.toList.dropLast_append_getLast h', ← p.toList.dropLast.take_append_drop 1]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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] =
    take 1 (↑p : List DyckStep).dropLast ++ drop 1 (↑p : List DyckStep).dropLast ++ [(↑p : List DyckStep).getLast h']
have rw : U :: (↑p : List DyckStep).dropLast.tail ++ [D] = [U] ++ (↑p : List DyckStep).dropLast.tail ++ [D]
Tactic: rw [getLast_eq_D, drop_one, this, head_eq_U]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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 k (List.take i (↑p : List DyckStep))) ≤ count U (List.take k (List.take i (↑p : List DyckStep)))
have rw : count D (List.take (min k i) (↑p : List DyckStep)) ≤ count U (List.take (min k i) (↑p : List DyckStep))
Tactic: rw [take_take]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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 (List.drop i (↑p : List DyckStep)) = count D (List.drop i (↑p : List DyckStep))
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
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.drop i (↑p : List DyckStep)) = count D (List.drop i (↑p : List DyckStep))
have 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))
Tactic: rw [← take_append_drop i p.toList, count_append, count_append] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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 k (List.drop i (↑p : List DyckStep))) ≤ count U (List.take k (List.drop i (↑p : List DyckStep)))
have 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)))
Tactic: rw [show i = min i (i + k) by omega, ← take_take] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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 k (List.drop i (↑p : List DyckStep))) ≤ count U (List.take k (List.drop i (↑p : List DyckStep)))
have rw : count D (List.take (i + k) (↑p : List DyckStep)) ≤ count U (List.take (i + k) (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take i ([U] ++ (↑p : List DyckStep) ++ [D])) ≤
    count U (List.take i ([U] ++ (↑p : List DyckStep) ++ [D]))
have 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])
Tactic: simp only [take_append, count_append]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ 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])
have 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))
Tactic: rw [← add_rotate (count D _), ← add_rotate (count U _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ 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))
have apply : 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: apply add_le_add _ (p.count_D_le_count_U _)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ 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 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])
Tactic: rcases i.eq_zero_or_pos with hi | hi