awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
⊢ q ≤ p + q
have pos : ∀ (h : p = 0), q ≤ p + q
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
pos : ∀ (h : p = 0), q ≤ p + q
⊢ q ≤ p + q
have neg : ∀ (h : ¬p = 0), q ≤ p + q
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q
have this : p.outsidePart.semilength < p.semilength
Tactic: have := semilength_outsidePart_lt h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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)
⊢ (↑p : List DyckStep) <:+: (↑r : List DyckStep)
have tail : ∀ (mq : m = insidePart 0 ∨ m = outsidePart 0), (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r, mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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)
⊢ (↑p : List DyckStep) <:+: (↑r : List DyckStep)
have tail₁ : ∀ (hr : r ≠ 0), (↑p : List DyckStep) <:+: (↑r : List DyckStep)
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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
⊢ (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
have mq₁ : m = 0
Tactic: rw [insidePart_zero, outsidePart_zero, or_self] at mq
Cleared hypotheses: mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
have tail : ∀ (ih : (↑p : List DyckStep) <:+: (↑0 : List DyckStep)) (mq : m = 0), (↑p : List DyckStep) <:+: (↑0 : List DyckStep)
Tactic: rwa [mq] at ih
Cleared hypotheses: ih, mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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
⊢ (↑p : List DyckStep) <:+: (↑r : List DyckStep)
have this : [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)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≤ q
⊢ (↑p : List DyckStep) <:+: (↑q : List DyckStep)
have refl : (↑p : List DyckStep) <:+: (↑p : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : p ≤ q
refl : (↑p : List DyckStep) <:+: (↑p : List DyckStep)
⊢ (↑p : List DyckStep) <:+: (↑q : List DyckStep)
have 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)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
h : (↑p : List DyckStep) <:+ (↑q : List DyckStep)
⊢ p ≤ q
have obtain : ∀ (r' : List DyckStep) (h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)), p ≤ q
Tactic: obtain ⟨r', h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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))
have hq : count U (↑q : List DyckStep) = count D (↑q : List DyckStep)
Tactic: have hq := q.count_U_eq_count_D
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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)
⊢ 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))
have 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)))
Tactic: rw [← h] at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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 (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)))
have hq₁ : 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
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
r' : List DyckStep
h : r' ++ (↑p : List DyckStep) = (↑q : List DyckStep)
⊢ p ≤ q
have 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))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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)
⊢ r' = (↑r : List DyckStep)
have simp_rw₁ : r' = List.take ((↑q : List DyckStep).length - (↑p : List DyckStep).length) (↑q : List DyckStep)
Tactic: simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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)
⊢ r' = (↑r : List DyckStep)
have simp_rw₂ : r' = List.take ((r' ++ (↑p : List DyckStep)).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))
Tactic: simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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))
⊢ r' = (↑r : List DyckStep)
have simp_rw₃ : r' = List.take (r'.length + (↑p : List DyckStep).length - (↑p : List DyckStep).length) (r' ++ (↑p : List DyckStep))
Tactic: simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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))
⊢ r' = (↑r : List DyckStep)
have simp_rw₄ : r' = List.take r'.length (r' ++ (↑p : List DyckStep))
Tactic: simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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
⊢ p ≤ q
have e : r' = (↑r : List DyckStep)
Tactic: have e : r' = r := by
    simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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)
⊢ p ≤ q
have h₁ : (↑r : List DyckStep) ++ (↑p : List DyckStep) = (↑q : List DyckStep)
Tactic: rw [e] at h
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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)
⊢ p ≤ q
have h₁ : r + p = q
Tactic: replace h : r + p = q := DyckWord.ext h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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 ≤ q
have rw : p ≤ r + p
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p_1 q_1 : DyckWord
h : p_1 ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
⊢ p = q
have h₁ : (↑p : List DyckStep) <:+: (↑q : List DyckStep)
Tactic: have h₁ := infix_of_le pq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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)
⊢ p = q
have h₂ : (↑q : List DyckStep) <:+: (↑p : List DyckStep)
Tactic: have h₂ := infix_of_le qp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ 0 < p ↔ p ≠ 0
have rw : 0 ≤ p
Tactic: rw [ne_comm, iff_comm, ne_iff_lt_iff_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ p.semilength ≤ r.semilength
have tail : ∀ (mq : m = insidePart 0 ∨ m = outsidePart 0), p.semilength ≤ semilength 0
Tactic: rcases eq_or_ne r 0 with rfl | hr
Cleared hypotheses: r, mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ p.semilength ≤ r.semilength
have tail₁ : ∀ (hr : r ≠ 0), p.semilength ≤ r.semilength
Tactic: rcases eq_or_ne r 0 with rfl | hr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
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
⊢ p.semilength ≤ semilength 0
have mq₁ : m = 0
Tactic: rw [insidePart_zero, outsidePart_zero, or_self] at mq
Cleared hypotheses: mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ p.semilength ≤ semilength 0
have tail : ∀ (ih : p.semilength ≤ semilength 0) (mq : m = 0), p.semilength ≤ semilength 0
Tactic: rwa [mq] at ih
Cleared hypotheses: ih, mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ p.semilength ≤ r.semilength
have tail : ∀ (hm : m = r.insidePart), p.semilength ≤ r.semilength
Tactic: rcases mq with hm | hm
Cleared hypotheses: mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
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
⊢ p.semilength ≤ r.semilength
have tail₁ : ∀ (hm : m = r.outsidePart), p.semilength ≤ r.semilength
Tactic: rcases mq with hm | hm
Cleared hypotheses: mq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
pq : p ≤ q
⊢ p.semilength ≤ q.semilength
have refl : p.semilength ≤ p.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
Cleared hypotheses: pq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
pq : p ≤ q
refl : p.semilength ≤ p.semilength
⊢ p.semilength ≤ q.semilength
have 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
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
Cleared hypotheses: pq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
pq : p < q
⊢ p.semilength < q.semilength
have plq : p ≤ q
Tactic: obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
⊢ p.semilength < q.semilength
have pnq : p ≠ q
Tactic: obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength < q.semilength
have apply : p.semilength ≠ q.semilength
Tactic: apply lt_of_le_of_ne (monotone_semilength plq)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p ≠ q
⊢ p.semilength ≠ q.semilength
have contrapose : ∀ (pnq : p.semilength = q.semilength), p = q
Tactic: contrapose pnq
Cleared hypotheses: pnq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : p.semilength = q.semilength
⊢ p = q
have pnq₁ : 2 * p.semilength = 2 * q.semilength
Tactic: replace pnq := congr(2 * $(pnq))
Cleared hypotheses: pnq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (hypothesis)
Goal:
p q : DyckWord
pq : p < q
plq : p ≤ q
pnq : 2 * p.semilength = 2 * q.semilength
⊢ p = q
have pnq₁ : (↑p : List DyckStep).length = (↑q : List DyckStep).length
Tactic: simp_rw [two_mul_semilength_eq_length] at pnq
Cleared hypotheses: pnq
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ ofTree p.toTree = p
have pos : ∀ (h : p = 0), ofTree p.toTree = p
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
pos : ∀ (h : p = 0), ofTree p.toTree = p
⊢ ofTree p.toTree = p
have neg : ∀ (h : ¬p = 0), ofTree p.toTree = p
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ ofTree p.toTree = p
have neg : ofTree (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p
Tactic: rw [toTree]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ ofTree (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree) = p
have neg : (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p
Tactic: simp_rw [h, ite_false, ofTree]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ (ofTree p.insidePart.toTree).nest + ofTree p.outsidePart.toTree = p
have neg : p.insidePart.nest + p.outsidePart = p
Tactic: rw [ofTree_toTree p.insidePart, ofTree_toTree p.outsidePart]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
⊢ p.toTree.numNodes = p.semilength
have pos : ∀ (h : p = 0), p.toTree.numNodes = p.semilength
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
pos : ∀ (h : p = 0), p.toTree.numNodes = p.semilength
⊢ p.toTree.numNodes = p.semilength
have neg : ∀ (h : ¬p = 0), p.toTree.numNodes = p.semilength
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.toTree.numNodes = p.semilength
have neg : (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength
Tactic: rw [toTree]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ (if p = 0 then Tree.nil else node () p.insidePart.toTree p.outsidePart.toTree).numNodes = p.semilength
have neg : p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
Tactic: simp_rw [h, ite_false, numNodes]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
have neg : p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 =
  p.insidePart.semilength + p.outsidePart.semilength + 1
Tactic: rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
      numNodes_toTree p.insidePart, numNodes_toTree p.outsidePart]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
neg :
  p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 =
    p.insidePart.semilength + p.outsidePart.semilength + 1
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
have neg₁ : p.insidePart.semilength + p.outsidePart.toTree.numNodes + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
Tactic: rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
      numNodes_toTree p.insidePart, numNodes_toTree p.outsidePart]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.DyckWord (goal)
Goal:
p : DyckWord
h : ¬p = 0
neg :
  p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 =
    p.insidePart.semilength + p.outsidePart.semilength + 1
neg₁ :
  p.insidePart.semilength + p.outsidePart.toTree.numNodes + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
⊢ p.insidePart.toTree.numNodes + p.outsidePart.toTree.numNodes + 1 = p.semilength
have neg₂ : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.insidePart.semilength + p.outsidePart.semilength + 1
Tactic: rw [← semilength_insidePart_add_semilength_outsidePart_add_one h,
      numNodes_toTree p.insidePart, numNodes_toTree p.outsidePart]