awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
rw : p.insidePart.semilength + p.outsidePart.semilength + 1 = (p.insidePart.nest + p.outsidePart).semilength
rw₁ : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.nest.semilength + p.outsidePart.semilength
rw₂ : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.semilength + 1 + p.outsidePart.semilength
rw₃ rw₄ :
  p.insidePart.semilength + 1 + p.outsidePart.semilength = p.insidePart.semilength + 1 + p.outsidePart.semilength
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Tactic:
rw [← congrArg semilength (nest_insidePart_add_outsidePart h), semilength_add, semilength_nest,
    add_right_comm]

Premises used: DyckWord.semilength_add, DyckWord.nest_insidePart_add_outsidePart, congrArg, add_right_comm, DyckWord.semilength_nest, DyckWord.semilength
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength

Tactic:
have := semilength_insidePart_add_semilength_outsidePart_add_one h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.insidePart.semilength < p.semilength

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.outsidePart.semilength < p.semilength

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pos : ∀ (h : p = 0), q ≤ p + q
neg : ∀ (h : ¬p = 0), q ≤ p + q
⊢ q ≤ p + q

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
have := semilength_outsidePart_lt h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
this : p.outsidePart.semilength < p.semilength
⊢ q ≤ p + q

Tactic:
(le_add_self p.outsidePart q).trans
      (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))

Premises used: DyckWord.outsidePart_add, DyckWord.outsidePart, Relation.ReflTransGen.single, LE.le.trans, Eq.symm, Or.inr
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : ¬p = 0
this : p.outsidePart.semilength < p.semilength
⊢ q ≤ p + q

Tactic:
exact (le_add_self p.outsidePart q).trans
      (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))

Premises used: DyckWord.outsidePart_add, DyckWord.outsidePart, Relation.ReflTransGen.single, LE.le.trans, Eq.symm, Or.inr
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ 0 ≤ p

Tactic:
add_zero p ▸ le_add_self p 0

Premises used: Eq.rec, add_zero, OfNat.ofNat, DyckWord.le_add_self
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ (↑p : List DyckStep) <:+: (↑p : List DyckStep)

Tactic:
infix_refl _

Premises used: List.infix_refl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ (↑p : List DyckStep) <:+: (↑p : List DyckStep)

Tactic:
exact infix_refl _

Premises used: List.infix_refl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : (↑p : List DyckStep) <:+: (↑m : List DyckStep)
tail : ∀ (mq : m = insidePart 0 ∨ m = outsidePart 0), (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
tail₁ : ∀ (hr : r ≠ 0), (↑p : List DyckStep) <:+: (↑r : List DyckStep)
⊢ (↑p : List DyckStep) <:+: (↑r : List DyckStep)

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m : DyckWord
_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : (↑p : List DyckStep) <:+: (↑m : List DyckStep)
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ m = 0

Tactic:
rw [insidePart_zero, outsidePart_zero, or_self] at mq

Premises used: DyckWord.insidePart_zero, or_self, DyckWord.outsidePart_zero
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m : DyckWord
_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : (↑p : List DyckStep) <:+: (↑m : List DyckStep)
mq : m = 0
tail tail₁ tail₂ tail₃ :
  ∀ (ih : (↑p : List DyckStep) <:+: (↑0 : List DyckStep)) (mq : m = 0), (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
⊢ (↑p : List DyckStep) <:+: (↑0 : List DyckStep)

Tactic:
rwa [mq] at ih
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : (↑p : List DyckStep) <:+: (↑m : List DyckStep)
hr : r ≠ 0
⊢ [U] ++ (↑r.insidePart : List DyckStep) ++ [D] ++ (↑r.outsidePart : List DyckStep) = (↑r : List DyckStep)

Tactic:
have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r :=
        DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : (↑p : List DyckStep) <:+: (↑m : List DyckStep)
hr : r ≠ 0
this : [U] ++ (↑r.insidePart : List DyckStep) ++ [D] ++ (↑r.outsidePart : List DyckStep) = (↑r : List DyckStep)
⊢ (↑p : List DyckStep) <:+: (↑r : List DyckStep)

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : p ≤ q
refl : (↑p : List DyckStep) <:+: (↑p : List DyckStep)
tail :
  ∀ {b c : DyckWord} (_pm : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p b)
    (mq : b = c.insidePart ∨ b = c.outsidePart) (ih : (↑p : List DyckStep) <:+: (↑b : List DyckStep)),
    (↑p : List DyckStep) <:+: (↑c : List DyckStep)
⊢ (↑p : List DyckStep) <:+: (↑q : List DyckStep)

Tactic:
induction h with
  | refl => exact infix_refl _
  | tail _pm mq ih =>
    rename_i m r
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r :=
        DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)
      grind

Premises used: DyckWord.insidePart_zero, List.infix_refl, List.tail, or_self, DyckWord.outsidePart_zero, refl, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
h : (↑p : List DyckStep) <:+ (↑q : List DyckStep)
obtain : ∀ (r' : List DyckStep) (h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)), p ≤ q
⊢ p ≤ q

Tactic:
obtain ⟨r', h⟩ := h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
⊢ count U (↑q : List DyckStep) = count D (↑q : List DyckStep)

Tactic:
have hq := q.count_U_eq_count_D
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hq : count U (↑q : List DyckStep) = count D (↑q : List DyckStep)
rw :
  ∀ (hq : count U (r' ++ (↑p : List DyckStep)) = count D (r' ++ (↑p : List DyckStep))),
    count U
        (List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))) =
      count D
        (List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep)))
⊢ count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))

Tactic:
rw [← h] at hq ⊢
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hq : count U (r' ++ (↑p : List DyckStep)) = count D (r' ++ (↑p : List DyckStep))
⊢ count U r' = count D r'

Tactic:
rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq

Premises used: Nat.add_right_cancel_iff, DyckWord.count_U_eq_count_D, List.count_append
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hq : count U r' = count D r'
⊢ count U (List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))) =
    count D (List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep)))

Tactic:
simp [hq]
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
⊢ count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))

Tactic:
have hc : (q.toList.take (q.toList.length - p.toList.length)).count U =
      (q.toList.take (q.toList.length - p.toList.length)).count D := by
    have hq := q.count_U_eq_count_D
    rw [← h] at hq ⊢
    rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq
    simp [hq]
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
simp_rw : r' = (↑(q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc) : List DyckStep)
simp_rw₁ : r' = List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)
simp_rw₂ :
  r' = List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))
simp_rw₃ :
  r' = List.take (r'.length + (↑p : List DyckStep).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))
simp_rw₄ : r' = List.take r'.length (r' ++ (↑p : List DyckStep))
⊢ r' = (↑r : List DyckStep)

Tactic:
simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']

Premises used: List.length_append, add_tsub_cancel_right, List.take_left', DyckWord.take
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
⊢ r' = (↑r : List DyckStep)

Tactic:
have e : r' = r := by
    simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
e : r' = (↑r : List DyckStep)
⊢ (↑r : List DyckStep) ++ (↑p : List DyckStep) = (↑q : List DyckStep)

Tactic:
rw [e] at h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
e : r' = (↑r : List DyckStep)
h₁ : (↑r : List DyckStep) ++ (↑p : List DyckStep) = (↑q : List DyckStep)
⊢ r' = (↑r : List DyckStep)

Tactic:
rw [e] at h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
h : (↑r : List DyckStep) ++ (↑p : List DyckStep) = (↑q : List DyckStep)
e : r' = (↑r : List DyckStep)
⊢ r + p = q

Tactic:
replace h : r + p = q := DyckWord.ext h
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
e : r' = (↑r : List DyckStep)
h : r + p = q
rw : p ≤ r + p
⊢ p ≤ q

Tactic:
rw [← h]
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
e : r' = (↑r : List DyckStep)
h : r + p = q
⊢ p ≤ r + p

Tactic:
le_add_self ..

Premises used: DyckWord.le_add_self
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
r' : List DyckStep
hc :
  count U (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)) =
    count D (List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep))
r : DyckWord := q.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) hc
e : r' = (↑r : List DyckStep)
h : r + p = q
⊢ p ≤ r + p

Tactic:
exact le_add_self ..

Premises used: DyckWord.le_add_self
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p_1 q_1 : DyckWord
h : p_1 ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
⊢ (↑p : List DyckStep) <:+: (↑q : List DyckStep)

Tactic:
have h₁ := infix_of_le pq
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p_1 q_1 : DyckWord
h : p_1 ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : (↑p : List DyckStep) <:+: (↑q : List DyckStep)
⊢ (↑q : List DyckStep) <:+: (↑p : List DyckStep)

Tactic:
have h₂ := infix_of_le qp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p_1 q_1 : DyckWord
h : p_1 ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : (↑p : List DyckStep) <:+: (↑q : List DyckStep)
h₂ : (↑q : List DyckStep) <:+: (↑p : List DyckStep)
⊢ p = q

Tactic:
DyckWord.ext <| h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

Premises used: List.IsInfix.length_le, LE.le.antisymm, List.IsInfix.eq_of_length, DyckWord.ext
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p_1 q_1 : DyckWord
h : p_1 ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
h₁ : (↑p : List DyckStep) <:+: (↑q : List DyckStep)
h₂ : (↑q : List DyckStep) <:+: (↑p : List DyckStep)
⊢ p = q

Tactic:
exact DyckWord.ext <| h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

Premises used: List.IsInfix.length_le, LE.le.antisymm, List.IsInfix.eq_of_length, DyckWord.ext
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
rw : 0 ≤ p
⊢ 0 < p ↔ p ≠ 0

Tactic:
rw [ne_comm, iff_comm, ne_iff_lt_iff_le]

Premises used: iff_comm, ne_comm, ne_iff_lt_iff_le
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ 0 ≤ p

Tactic:
DyckWord.zero_le p

Premises used: DyckWord.zero_le
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
⊢ 0 ≤ p

Tactic:
exact DyckWord.zero_le p

Premises used: DyckWord.zero_le
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
⊢ p.semilength ≤ p.semilength

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
tail : ∀ (mq : m = insidePart 0 ∨ m = outsidePart 0), p.semilength ≤ semilength 0
tail₁ : ∀ (hr : r ≠ 0), p.semilength ≤ r.semilength
⊢ p.semilength ≤ r.semilength

Tactic:
rcases eq_or_ne r 0 with rfl | hr

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = insidePart 0 ∨ m = outsidePart 0
⊢ m = 0

Tactic:
rw [insidePart_zero, outsidePart_zero, or_self] at mq

Premises used: DyckWord.insidePart_zero, or_self, DyckWord.outsidePart_zero
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
mq : m = 0
tail tail₁ tail₂ tail₃ : ∀ (ih : p.semilength ≤ semilength 0) (mq : m = 0), p.semilength ≤ semilength 0
⊢ p.semilength ≤ semilength 0

Tactic:
rwa [mq] at ih
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
mq : m = r.insidePart ∨ m = r.outsidePart
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
tail : ∀ (hm : m = r.insidePart), p.semilength ≤ r.semilength
tail₁ : ∀ (hm : m = r.outsidePart), p.semilength ≤ r.semilength
⊢ p.semilength ≤ r.semilength

Tactic:
rcases mq with hm | hm
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

Tactic:
ih.trans (hm ▸ semilength_insidePart_lt hr).le

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.insidePart
⊢ p.semilength ≤ r.semilength

Tactic:
exact ih.trans (hm ▸ semilength_insidePart_lt hr).le

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Tactic:
ih.trans (hm ▸ semilength_outsidePart_lt hr).le

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q m r : DyckWord
h : Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p m
ih : p.semilength ≤ m.semilength
hr : r ≠ 0
hm : m = r.outsidePart
⊢ p.semilength ≤ r.semilength

Tactic:
exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p ≤ q
refl : p.semilength ≤ p.semilength
tail :
  ∀ {b c : DyckWord},
    Relation.ReflTransGen (fun (p q : DyckWord) ↦ p = q.insidePart ∨ p = q.outsidePart) p b →
      ∀ (mq : b = c.insidePart ∨ b = c.outsidePart) (ih : p.semilength ≤ b.semilength), p.semilength ≤ c.semilength
⊢ p.semilength ≤ q.semilength

Tactic:
induction pq with
  | refl => rfl
  | tail _ mq ih =>
    rename_i m r _
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · rcases mq with hm | hm
      · exact ih.trans (hm ▸ semilength_insidePart_lt hr).le
      · exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

Premises used: DyckWord.insidePart_zero, List.tail, or_self, DyckWord.outsidePart_zero, refl, rfl
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
⊢ p ≤ q

Tactic:
obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq

Premises used: lt_iff_le_and_ne, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
⊢ p ≠ q

Tactic:
obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq

Premises used: lt_iff_le_and_ne, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
apply : p.semilength ≠ q.semilength
⊢ p.semilength < q.semilength

Tactic:
apply lt_of_le_of_ne (monotone_semilength plq)

Premises used: DyckWord.monotone_semilength, lt_of_le_of_ne
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
contrapose : ∀ (pnq : p.semilength = q.semilength), p = q
⊢ p.semilength ≠ q.semilength

Tactic:
contrapose pnq
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p.semilength = q.semilength
⊢ 2 * p.semilength = 2 * q.semilength

Tactic:
replace pnq := congr(2 * $(pnq))
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ (↑p : List DyckStep).length = (↑q : List DyckStep).length

Tactic:
simp_rw [two_mul_semilength_eq_length] at pnq

Premises used: DyckWord.two_mul_semilength_eq_length
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : (↑p : List DyckStep).length = (↑q : List DyckStep).length
⊢ p = q

Tactic:
DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

Premises used: List.IsInfix.eq_of_length, DyckWord.infix_of_le, DyckWord.ext
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : (↑p : List DyckStep).length = (↑q : List DyckStep).length
⊢ p = q

Tactic:
exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq)

Premises used: List.IsInfix.eq_of_length, DyckWord.infix_of_le, DyckWord.ext
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
semilength_insidePart_lt ‹_›

Premises used: DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.outsidePart.semilength < p.semilength

Tactic:
semilength_outsidePart_lt ‹_›

Premises used: DyckWord.semilength_outsidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_lt ‹_›]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
decreasing_by exacts [semilength_insidePart_lt ‹_›, semilength_outsidePart_lt ‹_›]

Premises used: DyckWord.semilength_outsidePart_lt, DyckWord.semilength_insidePart_lt
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
pos : ∀ (h : p = 0), ofTree p.toTree = p
neg : ∀ (h : ¬p = 0), ofTree p.toTree = p
⊢ ofTree p.toTree = p

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : p = 0
⊢ ofTree p.toTree = p

Tactic:
simp [h, toTree, ofTree]

Premises used: DyckWord.toTree, DyckWord.ofTree
-- Module: Mathlib.Combinatorics.Enumerative.DyckWord
Goal:
p : DyckWord
h : ¬p = 0
neg : ofTree (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p
⊢ ofTree p.toTree = p

Tactic:
rw [toTree]

Premises used: DyckWord.toTree