awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
l₁ w : List (Option α)
h : l = l₁ ++ w
hl₁ : l₁.reduceOption = l'
m n : ℕ
hl₂ : w = replicate m none ++ some a :: replicate n none
h₁ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₂ :
  l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    l₁.reduceOption ++ reduceOption (replicate m none) = l' ∧
      Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []
h₃ : l₁ ++ w = l₁ ++ replicate m none ++ some a :: replicate n none ∧ l₁.reduceOption ++ [] = l' ∧ True
h₄ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption ++ [] = l' ∧ True
h₅ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ l₁.reduceOption = l' ∧ True
h₆ : l₁ ++ w = l₁ ++ (replicate m none ++ some a :: replicate n none) ∧ True ∧ True
h₇ : True ∧ True ∧ True
⊢ l = l₁ ++ replicate m none ++ some a :: replicate n none ∧
    (l₁ ++ replicate m none).reduceOption = l' ∧ Eq.{u_1 + 1} (α := List α) (reduceOption (replicate n none)) []

Tactic:
simp_rw [h, reduceOption_append, reduceOption_replicate_none, append_assoc, append_nil, hl₁,
      hl₂, and_self]

Premises used: List.reduceOption_replicate_none, List.append_assoc, and_self, List.append_nil, List.reduceOption_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
l' : List α
a : α
w w_1 : List (Option α)
h : l = w ++ some a :: w_1
hl₁ : w.reduceOption = l'
hl₂ : w_1.reduceOption = []
mpr : (w ++ some a :: w_1).reduceOption = l' ++ [a]
mpr₁ : w.reduceOption ++ (some a :: w_1).reduceOption = l' ++ [a]
mpr₂ : w.reduceOption ++ a :: w_1.reduceOption = l' ++ [a]
mpr₃ : l' ++ a :: w_1.reduceOption = l' ++ [a]
mpr₄ mpr₅ : l' ++ [a] = l' ++ [a]
⊢ l.reduceOption = l' ++ [a]

Tactic:
rw [h, reduceOption_append, reduceOption_cons_of_some, hl₁, hl₂]

Premises used: List.reduceOption_cons_of_some, List.reduceOption_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
nil : length.{u_1} (α := α) [] = length.{u_1} (α := Option α) (filter Option.isSome [])
nil₁ : length.{u_1} (α := α) [] = length.{u_1} (α := Option α) []
⊢ length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])

Tactic:
simp_rw [reduceOption_nil, filter_nil, length]

Premises used: List.filter_nil, List.reduceOption_nil, List.length
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
cons : (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length
cons₁ : ∀ (val : α), (some val :: tl).reduceOption.length = (filter Option.isSome (some val :: tl)).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length

Tactic:
cases hd
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (none :: tl).reduceOption.length = (filter Option.isSome (none :: tl)).length

Tactic:
simp [hl]
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
val : α
⊢ (some val :: tl).reduceOption.length = (filter Option.isSome (some val :: tl)).length

Tactic:
simp [hl]
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
nil : length.{u_1} (α := α) (reduceOption []) = length.{u_1} (α := Option α) (filter Option.isSome [])
cons :
  ∀ (hd : Option α) (tl : List (Option α)) (hl : tl.reduceOption.length = (filter Option.isSome tl).length),
    (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length
⊢ l.reduceOption.length = (filter Option.isSome l).length

Tactic:
induction l with
  | nil => simp_rw [reduceOption_nil, filter_nil, length]
  | cons hd tl hl => cases hd <;> simp [hl]

Premises used: List.filter_nil, List.cons, List.reduceOption_nil, List.length, List.nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
simp_rw : l.length = (filter Option.isSome l).length + (filter Option.isNone l).length
simp_rw₁ :
  (filter Option.isSome l).length + (filter (fun (x : Option α) ↦ !x.isSome) l).length =
    (filter Option.isSome l).length + (filter Option.isNone l).length
⊢ l.length = l.reduceOption.length + (filter Option.isNone l).length

Tactic:
simp_rw [reduceOption_length_eq, l.length_eq_length_filter_add Option.isSome, Option.not_isSome]

Premises used: List.reduceOption_length_eq, List.length_eq_length_filter_add, Option.not_isSome, Option.isSome
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
rw : l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length
⊢ l.reduceOption.length ≤ l.length

Tactic:
rw [length_eq_reduceOption_length_add_filter_none]

Premises used: List.length_eq_reduceOption_length_add_filter_none
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length ≤ l.reduceOption.length + (filter Option.isNone l).length

Tactic:
apply Nat.le_add_right

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
rw : (filter Option.isSome l).length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
rw₁ rw₂ : (∀ (a : Option α), a ∈ l → a.isSome = true) ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true

Tactic:
rw [reduceOption_length_eq, List.length_filter_eq_length_iff]

Premises used: List.reduceOption_length_eq, List.length_filter_eq_length_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
rw : (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
⊢ l.reduceOption.length < l.length ↔ none ∈ l

Tactic:
rw [Nat.lt_iff_le_and_ne, and_iff_right (reduceOption_length_le l), Ne,
    reduceOption_length_eq_iff]

Premises used: Nat.lt_iff_le_and_ne, List.reduceOption_length_le, Ne, and_iff_right, List.reduceOption_length_eq_iff
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
nil :
  (¬∀ (x : Option α), Membership.mem (γ := List (Option α)) [] x → x.isSome = true) ↔
    Membership.mem (γ := List (Option α)) [] none
cons :
  ∀ (head : Option α) (tail : List (Option α)),
    ((¬∀ (x : Option α), x ∈ tail → x.isSome = true) ↔ none ∈ tail) →
      ((¬∀ (x : Option α), x ∈ head :: tail → x.isSome = true) ↔ none ∈ head :: tail)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l

Tactic:
induction l
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
⊢ (¬∀ (x : Option α), Membership.mem (γ := List (Option α)) [] x → x.isSome = true) ↔
    Membership.mem (γ := List (Option α)) [] none

Tactic:
simp
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
head : Option α
tail : List (Option α)
tail_ih : (¬∀ (x : Option α), x ∈ tail → x.isSome = true) ↔ none ∈ tail
⊢ (¬∀ (x : Option α), x ∈ head :: tail → x.isSome = true) ↔ none ∈ head :: tail

Tactic:
grind [cases Option]

Premises used: Option
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
x : Option α
none : Eq.{u_1 + 1} (α := List α) (reduceOption [Option.none]) (Option.toList Option.none)
some : ∀ (val : α), [Option.some val].reduceOption = (Option.some val).toList
⊢ [x].reduceOption = x.toList

Tactic:
cases x
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) (reduceOption [none]) (Option.toList none)

Tactic:
rfl
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
val : α
⊢ [some val].reduceOption = (some val).toList

Tactic:
rfl
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
x : Option α
nil : reduceOption (concat [] none) = HAppend.hAppend (α := List α) (reduceOption []) (Option.toList none)
nil₁ : ∀ (val : α), (concat [] (some val)).reduceOption = reduceOption [] ++ (some val).toList
⊢ (concat [] x).reduceOption = reduceOption [] ++ x.toList

Tactic:
cases x
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
⊢ reduceOption (concat [] none) = HAppend.hAppend (α := List α) (reduceOption []) (Option.toList none)

Tactic:
simp [Option.toList]

Premises used: Option.toList
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
val : α
⊢ (concat [] (some val)).reduceOption = reduceOption [] ++ (some val).toList

Tactic:
simp [Option.toList]

Premises used: Option.toList
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList
x : Option α
⊢ ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList

Tactic:
simp only [concat_eq_append, reduceOption_append] at hl

Premises used: List.concat_eq_append, List.reduceOption_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
cons : ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList
cons₁ : ∀ (val : α), ((some val :: tl).concat x).reduceOption = (some val :: tl).reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
cases hd
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList

Tactic:
simp [hl, reduceOption_append]

Premises used: List.reduceOption_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
val : α
⊢ ((some val :: tl).concat x).reduceOption = (some val :: tl).reduceOption ++ x.toList

Tactic:
simp [hl, reduceOption_append]

Premises used: List.reduceOption_append
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
x : Option α
nil : ∀ (x : Option α), (concat [] x).reduceOption = reduceOption [] ++ x.toList
cons :
  ∀ (hd : Option α) (tl : List (Option α))
    (hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList) (x : Option α),
    ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList

Tactic:
induction l generalizing x with
  | nil => cases x <;> simp [Option.toList]
  | cons hd tl hl =>
    simp only [concat_eq_append, reduceOption_append] at hl
    cases hd <;> simp [hl, reduceOption_append]

Premises used: Option.toList, List.concat_eq_append, List.cons, List.reduceOption_append, List.nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
x : α
⊢ (l.concat (some x)).reduceOption = l.reduceOption.concat x

Tactic:
simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some]

Premises used: List.concat_eq_append, List.reduceOption_cons_of_some, List.reduceOption_append, List.reduceOption_nil
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
x : α
⊢ x ∈ l.reduceOption ↔ some x ∈ l

Tactic:
simp only [reduceOption, id, mem_filterMap, exists_eq_right]

Premises used: exists_eq_right, id, List.mem_filterMap, List.reduceOption
-- Module: Mathlib.Data.List.ReduceOption
Goal:
α : Type u_1
l : List (Option α)
x : α
rw : some x ∈ l ↔ ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l.reduceOption i = some x
rw₁ : some x ∈ l ↔ x ∈ l.reduceOption
rw₂ rw₃ : some x ∈ l ↔ some x ∈ l
⊢ (∃ (i : ℕ), getElem? (valid := fun (as : List (Option α)) (i : ℕ) ↦ i < as.length) l i = some (some x)) ↔
    ∃ (i : ℕ), getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l.reduceOption i = some x

Tactic:
rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]

Premises used: List.reduceOption_mem_iff, List.mem_iff_getElem?
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
refine_1 : ∀ (h : f ∈ L.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
refine_2 : ∀ (h : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L), f ∈ L.sections
⊢ f ∈ L.sections ↔ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
refine_1 :
  ∀ {f : List α} (h : Membership.mem (γ := List (List α)) (sections []) f),
    Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f []
refine_1₁ :
  ∀ (head : List α) (tail : List (List α)),
    (∀ {f : List α} (h : f ∈ tail.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f tail) →
      ∀ {f : List α} (h : f ∈ (head :: tail).sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f (head :: tail)
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L

Tactic:
induction L generalizing f
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
f : List α
h : Membership.mem (γ := List (List α)) (sections []) f
refine_1 :
  ∀ (h : Membership.mem (γ := List (List α)) (sections []) []), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) [] []
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f []

Tactic:
cases mem_singleton.1 h

Premises used: List.mem_singleton, Iff.mp
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
h : Membership.mem (γ := List (List α)) (sections []) []
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) [] []

Tactic:
Forall₂.nil

Premises used: List.Forall₂.nil
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
h : Membership.mem (γ := List (List α)) (sections []) []
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) [] []

Tactic:
exact Forall₂.nil

Premises used: List.Forall₂.nil
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
head : List α
tail : List (List α)
tail_ih : ∀ {f : List α} (h : f ∈ tail.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f tail
f : List α
h : f ∈ (head :: tail).sections
⊢ ∃ (a : List α), a ∈ tail.sections ∧ ∃ (a_1 : α), a_1 ∈ head ∧ a_1 :: a = f

Tactic:
simp only [sections, mem_flatMap, mem_map] at h

Premises used: List.mem_flatMap, List.sections, List.mem_map
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
head : List α
tail : List (List α)
tail_ih : ∀ {f : List α} (h : f ∈ tail.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f tail
f : List α
h : ∃ (a : List α), a ∈ tail.sections ∧ ∃ (a_1 : α), a_1 ∈ head ∧ a_1 :: a = f
refine_1 :
  ∀ (w : List α),
    w ∈ tail.sections →
      ∀ (w_1 : α), w_1 ∈ head → Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) (w_1 :: w) (head :: tail)
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f (head :: tail)

Tactic:
rcases h with ⟨_, _, _, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
head : List α
tail : List (List α)
tail_ih : ∀ {f : List α} (h : f ∈ tail.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f tail
w : List α
left : w ∈ tail.sections
w_1 : α
left_1 : w_1 ∈ head
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) (w_1 :: w) (head :: tail)

Tactic:
simp only [*, forall₂_cons, true_and]

Premises used: List.forall₂_cons, true_and
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
⊢ Membership.mem (γ := List (List α)) (sections []) []

Tactic:
simp only [sections, mem_singleton]

Premises used: List.mem_singleton, List.sections
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L_1 : List (List α)
f_1 : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
refine_2 : ∃ (a_1 : List α), a_1 ∈ L.sections ∧ ∃ (a_2 : α), a_2 ∈ l ∧ a_2 :: a_1 = a :: f
⊢ a :: f ∈ (l :: L).sections

Tactic:
simp only [sections, mem_flatMap, mem_map]

Premises used: List.mem_flatMap, List.sections, List.mem_map
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L_1 : List (List α)
f_1 : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ ∃ (a_1 : List α), a_1 ∈ L.sections ∧ ∃ (a_2 : α), a_2 ∈ l ∧ a_2 :: a_1 = a :: f

Tactic:
⟨f, fs, a, al, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L_1 : List (List α)
f_1 : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ ∃ (a_1 : List α), a_1 ∈ L.sections ∧ ∃ (a_2 : α), a_2 ∈ l ∧ a_2 :: a_1 = a :: f

Tactic:
exact ⟨f, fs, a, al, rfl⟩
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
refine_2 : Membership.mem (γ := List (List α)) (sections []) []
refine_2₁ :
  ∀ {a : α} {l f : List α} {L : List (List α)} (al : a ∈ l) (fL : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L)
    (fs : f ∈ L.sections), a :: f ∈ (l :: L).sections
⊢ f ∈ L.sections

Tactic:
induction h with
    | nil => simp only [sections, mem_singleton]
    | @cons a l f L al fL fs =>
      simp only [sections, mem_flatMap, mem_map]
      exact ⟨f, fs, a, al, rfl⟩

Premises used: List.mem_singleton, List.cons, List.mem_flatMap, List.sections, List.mem_map, List.nil
-- Module: Mathlib.Data.List.Sections
Goal:
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ f.length = L.length

Tactic:
(mem_sections.1 h).length_eq

Premises used: Iff.mp, List.mem_sections, List.Forall₂.length_eq
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
h : s.length < t.length
⊢ Shortlex r s t

Tactic:
Prod.Lex.left _ _ h

Premises used: InvImage, List.Shortlex, Prod.Lex.left
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
apply :
  LT.lt (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∨
    Eq (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∧
      Lex r ((fun (a : List α) ↦ (a.length, a)) s).2 ((fun (a : List α) ↦ (a.length, a)) t).2
⊢ Shortlex r s t

Tactic:
apply Prod.lex_def.mpr

Premises used: Iff.mpr, Prod.lex_def
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
h :
  Eq (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∧
    Lex r ((fun (a : List α) ↦ (a.length, a)) s).2 ((fun (a : List α) ↦ (a.length, a)) t).2
⊢ LT.lt (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∨
    Eq (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∧
      Lex r ((fun (a : List α) ↦ (a.length, a)) s).2 ((fun (a : List α) ↦ (a.length, a)) t).2

Tactic:
right
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Eq (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∧
    Lex r ((fun (a : List α) ↦ (a.length, a)) s).2 ((fun (a : List α) ↦ (a.length, a)) t).2

Tactic:
⟨len_eq, h_lex⟩

Premises used: And.intro
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Eq (α := ℕ) ((fun (a : List α) ↦ (a.length, a)) s).1 ((fun (a : List α) ↦ (a.length, a)) t).1 ∧
    Lex r ((fun (a : List α) ↦ (a.length, a)) s).2 ((fun (a : List α) ↦ (a.length, a)) t).2

Tactic:
exact ⟨len_eq, h_lex⟩
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
⊢ Shortlex r s t ↔ s.length < t.length ∨ s.length = t.length ∧ Lex r s t

Tactic:
Prod.lex_def

Premises used: Prod.lex_def, InvImage, List.Shortlex
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
h : s.length = t.length
⊢ Shortlex r s t ↔ Lex r s t

Tactic:
simp [shortlex_def, h]

Premises used: List.shortlex_def
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s t : List α
⊢ Shortlex r (a :: s) (a :: t) ↔ Shortlex r s t

Tactic:
simp only [shortlex_def, length_cons, add_lt_add_iff_right, add_left_inj, List.lex_cons_iff]

Premises used: List.length_cons, add_left_inj, List.shortlex_def, List.lex_cons_iff, add_lt_add_iff_right
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s : List α
⊢ ¬Shortlex r s []

Tactic:
simp [shortlex_def]

Premises used: List.shortlex_def
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Shortlex r [a] [b] ↔ r a b

Tactic:
simp only [shortlex_def, length_singleton, lt_self_iff_false, lex_singleton_iff, true_and,
    false_or]

Premises used: List.length_singleton, false_or, List.shortlex_def, lt_self_iff_false, List.lex_singleton_iff, true_and
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Trichotomous r
⊢ Function.Injective (β := ℕ × List α) fun (a : List α) ↦ (a.length, a)

Tactic:
simp [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Asymm r
⊢ Std.Asymm (Shortlex r)

Tactic:
inferInstanceAs <| Std.Asymm (InvImage _ _)

Premises used: _private.0.List.Shortlex.asymm._proof_1
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
inl : ∀ (h1 : s₁.length < s₂.length), Shortlex r s₁ (s₂ ++ t)
inr : ∀ (h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂), Shortlex r s₁ (s₂ ++ t)
⊢ Shortlex r s₁ (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
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
inl : s₁.length < (s₂ ++ t).length
⊢ Shortlex r s₁ (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
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
inl : s₁.length < s₂.length + t.length
⊢ s₁.length < (s₂ ++ t).length

Tactic:
rw [List.length_append]

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

Tactic:
lia
-- 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₂
inr : Shortlex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ [])

Tactic:
rw [List.append_nil]

Premises used: List.append_nil
-- 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₂
⊢ Shortlex r s₁ s₂

Tactic:
h
-- 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₂
⊢ Shortlex r s₁ s₂

Tactic:
exact h
-- 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 α
inr : s₁.length < (s₂ ++ head :: tail).length
⊢ Shortlex r s₁ (s₂ ++ head :: tail)

Tactic:
apply of_length_lt

Premises used: List.Shortlex.of_length_lt
-- 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 α
inr : s₁.length < s₂.length + (tail.length + 1)
⊢ s₁.length < (s₂ ++ head :: tail).length

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

Premises used: List.length_cons, List.length_append