awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
head : α
tail : List α
⊢ s₁.length < s₂.length + (tail.length + 1)

Tactic:
lia
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
inr : Shortlex r s₁ (s₂ ++ [])
inr₁ : ∀ (head : α) (tail : List α), Shortlex r s₁ (s₂ ++ head :: tail)
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
cases t with
  | nil =>
    rw [List.append_nil]
    exact h
  | cons head tail =>
    apply of_length_lt
    rw [List.length_append, List.length_cons]
    lia

Premises used: List.head, List.length_cons, List.length_append, List.Shortlex.of_length_lt, List.tail, List.append_nil, List.Shortlex.cons, List.nil
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
inl : ∀ (h1 : t₁.length < t₂.length), Shortlex r (s ++ t₁) (s ++ t₂)
inr : ∀ (h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂), Shortlex r (s ++ t₁) (s ++ t₂)
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
rcases shortlex_def.mp h with h1 | h2

Premises used: List.shortlex_def, Iff.mp
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
inl : (s ++ t₁).length < (s ++ t₂).length
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
apply of_length_lt

Premises used: List.Shortlex.of_length_lt
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
inl : s.length + t₁.length < s.length + t₂.length
⊢ (s ++ t₁).length < (s ++ t₂).length

Tactic:
rw [List.length_append, List.length_append]

Premises used: List.length_append
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ s.length + t₁.length < s.length + t₂.length

Tactic:
lia
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
inr : Shortlex r t₁ t₂
⊢ Shortlex r ([] ++ t₁) ([] ++ t₂)

Tactic:
rw [List.nil_append, List.nil_append]

Premises used: List.nil_append
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ t₂

Tactic:
h
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r t₁ t₂

Tactic:
exact h
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
inr : (head :: tail ++ t₁).length = (head :: tail ++ t₂).length
inr₁ : Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)
⊢ Shortlex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
apply of_lex

Premises used: List.Shortlex.of_lex
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
inr : t₁.length = t₂.length
⊢ (head :: tail ++ t₁).length = (head :: tail ++ t₂).length

Tactic:
simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]

Premises used: List.length_cons, List.length_append, add_left_inj, List.cons_append, add_right_inj
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ t₁.length = t₂.length

Tactic:
h2.1

Premises used: And.left
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ t₁.length = t₂.length

Tactic:
exact h2.1

Premises used: And.left
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
List.Lex.append_left r h2.2 (head :: tail)

Premises used: List.cons, And.right, List.Lex.append_left
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
head : α
tail : List α
⊢ Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)

Tactic:
exact List.Lex.append_left r h2.2 (head :: tail)

Premises used: List.cons, And.right, List.Lex.append_left
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
inr : Shortlex r ([] ++ t₁) ([] ++ t₂)
inr₁ : ∀ (head : α) (tail : List α), Shortlex r (head :: tail ++ t₁) (head :: tail ++ t₂)
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
cases s with
  | nil =>
    rw [List.nil_append, List.nil_append]
    exact h
  | cons head tail =>
    apply of_lex
    · simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1
    exact List.Lex.append_left r h2.2 (head :: tail)

Premises used: List.head, List.length_cons, List.Shortlex.of_lex, List.length_append, add_left_inj, List.tail, List.Shortlex.cons, And.left, List.nil_append, List.cons_append, add_right_inj, List.nil
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: xb)

Tactic:
Acc.intro (xa :: xb) fun p lt => ?_

Premises used: List.cons, Acc.intro
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
intro : ∀ (p : List α) (lt : Shortlex r p (xa :: xb)), Acc (Shortlex r) p
⊢ Acc (Shortlex r) (xa :: xb)

Tactic:
refine Acc.intro (xa :: xb) fun p lt => ?_

Premises used: List.cons, Acc.intro
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
intro : ∀ (h1 : p.length < (xa :: xb).length), Acc (Shortlex r) p
intro₁ : ∀ (h2len : p.length = (xa :: xb).length) (h2lex : Lex r p (xa :: xb)), Acc (Shortlex r) p
⊢ Acc (Shortlex r) p

Tactic:
rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩

Premises used: List.shortlex_def, Iff.mp
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p

Tactic:
ih _ h1
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h1 : p.length < (xa :: xb).length
⊢ Acc (Shortlex r) p

Tactic:
exact ih _ h1
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
lt : Shortlex r [] (xa :: xb)
h2len : length.{u_1} (α := α) [] = (xa :: xb).length
⊢ Acc (Shortlex r) []

Tactic:
simp at h2len
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h2len : (xa :: xs).length = (xa :: xb).length
h : Lex r xs xb
⊢ xs.length = xb.length

Tactic:
simp only [length_cons, add_left_inj] at h2len

Premises used: List.length_cons, add_left_inj
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
⊢ Acc (Shortlex r) (xa :: xs)

Tactic:
ihb _ (of_lex h2len h) fun l hl => ?_

Premises used: List.Shortlex.of_lex
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
intro : ∀ (l : List α) (hl : l.length < (xa :: xs).length), Acc (Shortlex r) l
⊢ Acc (Shortlex r) (xa :: xs)

Tactic:
refine ihb _ (of_lex h2len h) fun l hl => ?_

Premises used: List.Shortlex.of_lex
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
intro : l.length < (xa :: xb).length
⊢ Acc (Shortlex r) l

Tactic:
apply ih
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
intro : l.length < xs.length + 1
⊢ l.length < (xa :: xb).length

Tactic:
rw [List.length_cons, ← h2len]

Premises used: List.length_cons
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1

Tactic:
hl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1

Tactic:
exact hl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h2len : (x :: xs).length = (xa :: xb).length
h : r x xa
⊢ xs.length = xb.length

Tactic:
simp only [List.length_cons, add_left_inj] at h2len

Premises used: List.length_cons, add_left_inj
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
rw : xb.length < (xa :: xb).length
⊢ xs.length < (xa :: xb).length

Tactic:
rw [h2len]
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xb.length < (xa :: xb).length

Tactic:
simp
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
intro : ∀ (l : List α) (hl : l.length < (x :: xs).length), Acc (Shortlex r) l
⊢ Acc (Shortlex r) (x :: xs)

Tactic:
refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
intro : l.length < (xa :: xb).length
⊢ Acc (Shortlex r) l

Tactic:
apply ih
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
intro : l.length < xs.length + 1
⊢ l.length < (xa :: xb).length

Tactic:
rw [List.length_cons, ← h2len]

Premises used: List.length_cons
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1

Tactic:
hl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1

Tactic:
exact hl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
intro : ∀ (lt : Shortlex r [] (xa :: xb)) (h2len : length.{u_1} (α := α) [] = (xa :: xb).length), Acc (Shortlex r) []
intro₁ :
  ∀ {xs : List α} (lt : Shortlex r (xa :: xs) (xa :: xb)) (h2len : (xa :: xs).length = (xa :: xb).length)
    (h : Lex r xs xb), Acc (Shortlex r) (xa :: xs)
intro₂ :
  ∀ {x : α} {xs : List α} (lt : Shortlex r (x :: xs) (xa :: xb)) (h2len : (x :: xs).length = (xa :: xb).length)
    (h : r x xa), Acc (Shortlex r) (x :: xs)
⊢ Acc (Shortlex r) p

Tactic:
cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

Premises used: List.length_cons, add_left_inj, List.Shortlex.cons, List.nil