awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
have rw : (filter Option.isSome l).length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
Tactic: rw [reduceOption_length_eq, List.length_filter_eq_length_iff]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
rw : (filter Option.isSome l).length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
⊢ l.reduceOption.length = l.length ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
have rw₁ : (∀ (a : Option α), a ∈ l → a.isSome = true) ↔ ∀ (x : Option α), x ∈ l → x.isSome = true
Tactic: rw [reduceOption_length_eq, List.length_filter_eq_length_iff]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length < l.length ↔ none ∈ l
have rw : (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
Tactic: rw [Nat.lt_iff_le_and_ne, and_iff_right (reduceOption_length_le l), Ne,
    reduceOption_length_eq_iff]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
have nil : (¬∀ (x : Option α), Membership.mem (γ := List (Option α)) [] x → x.isSome = true) ↔
  Membership.mem (γ := List (Option α)) [] none
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
nil :
  (¬∀ (x : Option α), Membership.mem (γ := List (Option α)) [] x → x.isSome = true) ↔
    Membership.mem (γ := List (Option α)) [] none
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
have 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)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
x : Option α
⊢ [x].reduceOption = x.toList
have none : Eq.{u_1 + 1} (α := List α) (reduceOption [none]) (Option.toList none)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
x : Option α
none : Eq.{u_1 + 1} (α := List α) (reduceOption [Option.none]) (Option.toList Option.none)
⊢ [x].reduceOption = x.toList
have some : ∀ (val : α), [some val].reduceOption = (some val).toList
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
x : Option α
⊢ (concat [] x).reduceOption = reduceOption [] ++ x.toList
have nil : reduceOption (concat [] none) = HAppend.hAppend (α := List α) (reduceOption []) (Option.toList none)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
x : Option α
nil : reduceOption (concat [] none) = HAppend.hAppend (α := List α) (reduceOption []) (Option.toList none)
⊢ (concat [] x).reduceOption = reduceOption [] ++ x.toList
have nil₁ : ∀ (val : α), (concat [] (some val)).reduceOption = reduceOption [] ++ (some val).toList
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (hypothesis)
Goal:
α : Type u_1
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
have hl₁ : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
Tactic: simp only [concat_eq_append, reduceOption_append] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList
have cons : ((none :: tl).concat x).reduceOption = (none :: tl).reduceOption ++ x.toList
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
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
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList
have cons₁ : ∀ (val : α), ((some val :: tl).concat x).reduceOption = (some val :: tl).reduceOption ++ x.toList
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
x : Option α
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList
have nil : ∀ (x : Option α), (concat [] x).reduceOption = 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]
Cleared hypotheses: l, x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
x : Option α
nil : ∀ (x : Option α), (concat [] x).reduceOption = reduceOption [] ++ x.toList
⊢ (l.concat x).reduceOption = l.reduceOption ++ x.toList
have 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
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]
Cleared hypotheses: l, x
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
Goal:
α : Type u_1
l : List (Option α)
x : α
⊢ (∃ (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
have rw : some x ∈ l ↔ ∃ (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]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
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
⊢ (∃ (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
have rw₁ : some x ∈ l ↔ x ∈ l.reduceOption
Tactic: rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]
-- Lean 4 proof step from Mathlib.Data.List.ReduceOption (goal)
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
⊢ (∃ (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
have rw₂ : some x ∈ l ↔ some x ∈ l
Tactic: rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
Goal:
α : Type u_1
L : List (List α)
f : List α
⊢ f ∈ L.sections ↔ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
have refine_1 : ∀ (h : f ∈ L.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
Goal:
α : Type u_1
L : List (List α)
f : List α
refine_1 : ∀ (h : f ∈ L.sections), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections ↔ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
have refine_2 : ∀ (h : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L), f ∈ L.sections
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
Goal:
α : Type u_1
L : List (List α)
f : List α
h : f ∈ L.sections
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
have refine_1 : ∀ {f : List α} (h : Membership.mem (γ := List (List α)) (sections []) f),
  Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f []
Tactic: induction L generalizing f
Cleared hypotheses: L, f, h
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
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 []
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
have 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)
Tactic: induction L generalizing f
Cleared hypotheses: L, f, h
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
Goal:
α : Type u_1
f : List α
h : Membership.mem (γ := List (List α)) (sections []) f
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f []
have refine_1 : ∀ (h : Membership.mem (γ := List (List α)) (sections []) []), Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) [] []
Tactic: cases mem_singleton.1 h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Data.List.Sections (hypothesis)
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
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f (head :: tail)
have h₁ : ∃ (a : List α), a ∈ tail.sections ∧ ∃ (a_1 : α), a_1 ∈ head ∧ a_1 :: a = f
Tactic: simp only [sections, mem_flatMap, mem_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
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
⊢ Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f (head :: tail)
have refine_1 : ∀ (w : List α),
  w ∈ tail.sections → ∀ (w_1 : α), w_1 ∈ head → Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) (w_1 :: w) (head :: tail)
Tactic: rcases h with ⟨_, _, _, _, rfl⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
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 :: f ∈ (l :: L).sections
have refine_2 : ∃ (a_1 : List α), a_1 ∈ L.sections ∧ ∃ (a_2 : α), a_2 ∈ l ∧ a_2 :: a_1 = a :: f
Tactic: simp only [sections, mem_flatMap, mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
Goal:
α : Type u_1
L : List (List α)
f : List α
h : Forall₂ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) f L
⊢ f ∈ L.sections
have refine_2 : Membership.mem (γ := List (List α)) (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⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sections (goal)
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 []) []
⊢ f ∈ L.sections
have 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
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⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ Shortlex r s t
have 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
Tactic: apply Prod.lex_def.mpr
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : List α
len_eq : s.length = t.length
h_lex : Lex r s t
⊢ 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
have 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
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)
have inl : ∀ (h1 : s₁.length < s₂.length), Shortlex r s₁ (s₂ ++ t)
Tactic: rcases shortlex_def.mp h with h1 | h2
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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)
⊢ Shortlex r s₁ (s₂ ++ t)
have inr : ∀ (h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂), Shortlex r s₁ (s₂ ++ t)
Tactic: rcases shortlex_def.mp h with h1 | h2
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ Shortlex r s₁ (s₂ ++ t)
have inl : s₁.length < (s₂ ++ t).length
Tactic: apply of_length_lt
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h1 : s₁.length < s₂.length
⊢ s₁.length < (s₂ ++ t).length
have inl : s₁.length < s₂.length + t.length
Tactic: rw [List.length_append]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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 α
⊢ Shortlex r s₁ (s₂ ++ head :: tail)
have inr : s₁.length < (s₂ ++ head :: tail).length
Tactic: apply of_length_lt
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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₂ ++ head :: tail).length
have inr : s₁.length < s₂.length + (tail.length + 1)
Tactic: rw [List.length_append, List.length_cons]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)
have inr : Shortlex r s₁ (s₂ ++ [])
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
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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₂ ++ [])
⊢ Shortlex r s₁ (s₂ ++ t)
have inr₁ : ∀ (head : α) (tail : List α), Shortlex r s₁ (s₂ ++ head :: tail)
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
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
have inl : ∀ (h1 : t₁.length < t₂.length), Shortlex r (s ++ t₁) (s ++ t₂)
Tactic: rcases shortlex_def.mp h with h1 | h2
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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₂)
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
have inr : ∀ (h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂), Shortlex r (s ++ t₁) (s ++ t₂)
Tactic: rcases shortlex_def.mp h with h1 | h2
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
have inl : (s ++ t₁).length < (s ++ t₂).length
Tactic: apply of_length_lt
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ (s ++ t₁).length < (s ++ t₂).length
have inl : s.length + t₁.length < s.length + t₂.length
Tactic: rw [List.length_append, List.length_append]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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 α
⊢ Shortlex r (head :: tail ++ t₁) (head :: tail ++ t₂)
have inr : (head :: tail ++ t₁).length = (head :: tail ++ t₂).length
Tactic: apply of_lex
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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
⊢ Shortlex r (head :: tail ++ t₁) (head :: tail ++ t₂)
have inr₁ : Lex r (head :: tail ++ t₁) (head :: tail ++ t₂)
Tactic: apply of_lex
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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 α
⊢ (head :: tail ++ t₁).length = (head :: tail ++ t₂).length
have inr : t₁.length = t₂.length
Tactic: simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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₂
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
have inr : Shortlex r ([] ++ t₁) ([] ++ 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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₂)
⊢ Shortlex r (s ++ t₁) (s ++ t₂)
have inr₁ : ∀ (head : α) (tail : List α), Shortlex r (head :: tail ++ t₁) (head :: tail ++ 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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)
have intro : ∀ (p : List α) (lt : Shortlex r p (xa :: xb)), Acc (Shortlex r) p
Tactic: refine Acc.intro (xa :: xb) fun p lt => ?_
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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)
⊢ Acc (Shortlex r) p
have intro : ∀ (h1 : p.length < (xa :: xb).length), Acc (Shortlex r) p
Tactic: rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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
⊢ Acc (Shortlex r) p
have intro₁ : ∀ (h2len : p.length = (xa :: xb).length) (h2lex : Lex r p (xa :: xb)), Acc (Shortlex r) p
Tactic: rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (hypothesis)
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
⊢ Acc (Shortlex r) (xa :: xs)
have h2len₁ : xs.length = xb.length
Tactic: simp only [length_cons, add_left_inj] at h2len
Cleared hypotheses: h2len
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
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)
have intro : ∀ (l : List α) (hl : l.length < (xa :: xs).length), Acc (Shortlex r) l
Tactic: refine ihb _ (of_lex h2len h) fun l hl => ?_