awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
h₁ : (y :: l).getLast ⋯ ∈ l
⊢ (y :: l).getLast ⋯ ∉ (y :: l).dropLast
have h₂ : (y :: l).getLast sorry ∈ y :: l
Tactic: subst hx
Cleared hypotheses: x, h_1, h, hy, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
h₁ : (y :: l).getLast ⋯ ∈ l
h₂ : (y :: l).getLast ⋯ ∈ y :: l
⊢ (y :: l).getLast ⋯ ∉ (y :: l).dropLast
have hy₁ : (y :: l).getLast sorry ≠ y
Tactic: subst hx
Cleared hypotheses: x, h_1, h, hy, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
⊢ False
have h₁ : ∀ (hk : 0 < (y :: l).dropLast.length)
  (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast 0 hk = (y :: l).getLast sorry),
  False
Tactic: obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
h₁ :
  ∀ (hk : 0 < (y :: l).dropLast.length)
    (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast 0 hk = (y :: l).getLast ⋯),
    False
⊢ False
have h₂ : ∀ (k : ℕ) (hk : k + 1 < (y :: l).dropLast.length)
  (hk' :
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast sorry),
  False
Tactic: obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
⊢ False
have h₁ : k + 1 = l.length
Tactic: suffices k + 1 = l.length by simp [this] at hk
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
⊢ k + 1 = l.length
have h₁ : ∀ (hl : Nodup.{u_1} (α := α) []) (h : Membership.mem (γ := List α) [] ([y].getLast sorry)) (h : [y].getLast sorry ∈ [y])
  (hy : [y].getLast sorry ≠ y) (H : [y].getLast sorry ∈ [y].dropLast) (hk : k + 1 < [y].dropLast.length)
  (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [y].dropLast (k + 1) hk = [y].getLast sorry),
  k + 1 = length.{u_1} (α := α) []
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, hl, h_1, h, hy, H, hk, hk'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
h₁ :
  ∀ (hl : Nodup.{u_1} (α := α) []) (h : Membership.mem (γ := List α) [] ([y].getLast ⋯)) (h : [y].getLast ⋯ ∈ [y])
    (hy : [y].getLast ⋯ ≠ y) (H : [y].getLast ⋯ ∈ [y].dropLast) (hk : k + 1 < [y].dropLast.length)
    (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [y].dropLast (k + 1) hk = [y].getLast ⋯),
    k + 1 = length.{u_1} (α := α) []
⊢ k + 1 = l.length
have h₂ : ∀ (hd : α) (tl : List α) (hl : (hd :: tl).Nodup) (h : (y :: hd :: tl).getLast sorry ∈ hd :: tl)
  (h : (y :: hd :: tl).getLast sorry ∈ y :: hd :: tl) (hy : (y :: hd :: tl).getLast sorry ≠ y)
  (H : (y :: hd :: tl).getLast sorry ∈ (y :: hd :: tl).dropLast) (hk : k + 1 < (y :: hd :: tl).dropLast.length)
  (hk' :
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
      (y :: hd :: tl).getLast sorry),
  k + 1 = (hd :: tl).length
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, hl, h_1, h, hy, H, hk, hk'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ k + 1 = (hd :: tl).length
have hl₁ : Function.Injective (hd :: tl).get
Tactic: rw [nodup_iff_injective_get] at hl
Cleared hypotheses: hl, h_1, h, hy, H, hk, hk'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ k + 1 = (hd :: tl).length
have h₁ : k = tl.length
Tactic: rw [length, Nat.succ_inj]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hxy : x ∈ y :: l
hx : x = y
⊢ (y :: l).prev x hxy = (y :: l).getLast ⋯
have nil : ∀ (hxy : x ∈ [y]), [y].prev x hxy = [y].getLast sorry
Tactic: cases l
Cleared hypotheses: l, hxy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hxy : x ∈ y :: l
hx : x = y
nil : ∀ (hxy : x ∈ [y]), [y].prev x hxy = [y].getLast ⋯
⊢ (y :: l).prev x hxy = (y :: l).getLast ⋯
have cons : ∀ (head : α) (tail : List α) (hxy : x ∈ y :: head :: tail),
  (y :: head :: tail).prev x hxy = (y :: head :: tail).getLast sorry
Tactic: cases l
Cleared hypotheses: l, hxy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l ≠ []
⊢ l.prev (l.head hl) ⋯ = l.getLast hl
have nil : ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), prev [] (head [] hl) sorry = getLast [] hl
Tactic: cases l with
  | nil => contradiction
  | cons head tail => apply prev_getLast_cons
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l ≠ []
nil : ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), prev [] (head [] hl) ⋯ = getLast [] hl
⊢ l.prev (l.head hl) ⋯ = l.getLast hl
have cons : ∀ (head : α) (tail : List α) (hl : head :: tail ≠ []),
  (head :: tail).prev ((head :: tail).head hl) sorry = (head :: tail).getLast hl
Tactic: cases l with
  | nil => contradiction
  | cons head tail => apply prev_getLast_cons
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯
have rw : (if hx : x = y then (z :: l).getLast sorry else if x = z then y else (z :: l).prev x sorry) = (z :: l).getLast sorry
Tactic: rw [prev, dif_pos hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
rw : (if hx : x = y then (z :: l).getLast ⋯ else if x = z then y else (z :: l).prev x ⋯) = (z :: l).getLast ⋯
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯
have rw₁ : (z :: l).getLast sorry = (z :: l).getLast sorry
Tactic: rw [prev, dif_pos hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x = z
⊢ (y :: z :: l).prev x h = y
have nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = y
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x = z
nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = y
⊢ (y :: z :: l).prev x h = y
have cons : ∀ (head : α) (tail : List α) (h : x ∈ y :: z :: head :: tail), (y :: z :: head :: tail).prev x h = y
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
⊢ (y :: z :: head :: tail).prev x h = y
have cons : (if hx : x = y then (z :: head :: tail).getLast sorry else if x = z then y else (z :: head :: tail).prev x sorry) = y
Tactic: rw [prev, dif_neg hy, if_pos hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons : (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) = y
⊢ (y :: z :: head :: tail).prev x h = y
have cons₁ : (if x = z then y else (z :: head :: tail).prev x sorry) = y
Tactic: rw [prev, dif_neg hy, if_pos hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons : (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) = y
cons₁ : (if x = z then y else (z :: head :: tail).prev x ⋯) = y
⊢ (y :: z :: head :: tail).prev x h = y
have cons₂ : y = y
Tactic: rw [prev, dif_neg hy, if_pos hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ (y :: z :: l).prev x h = (z :: l).prev x ⋯
have nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = [z].prev x sorry
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = [z].prev x ⋯
⊢ (y :: z :: l).prev x h = (z :: l).prev x ⋯
have cons : ∀ (head : α) (tail : List α) (h : x ∈ y :: z :: head :: tail),
  (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x sorry
Tactic: cases l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
⊢ (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x ⋯
have cons : (if hx : x = y then (z :: head :: tail).getLast sorry else if x = z then y else (z :: head :: tail).prev x sorry) =
  (z :: head :: tail).prev x sorry
Tactic: rw [prev, dif_neg hy, if_neg hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons :
  (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) =
    (z :: head :: tail).prev x ⋯
⊢ (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x ⋯
have cons₁ : (if x = z then y else (z :: head :: tail).prev x sorry) = (z :: head :: tail).prev x sorry
Tactic: rw [prev, dif_neg hy, if_neg hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons :
  (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) =
    (z :: head :: tail).prev x ⋯
cons₁ : (if x = z then y else (z :: head :: tail).prev x ⋯) = (z :: head :: tail).prev x ⋯
⊢ (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x ⋯
have cons₂ : (z :: head :: tail).prev x sorry = (z :: head :: tail).prev x sorry
Tactic: rw [prev, dif_neg hy, if_neg hz]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.prev x h ∈ l
have nil : ∀ (h : Membership.mem (γ := List α) [] x), Membership.mem (γ := List α) [] (prev [] x h)
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
nil : ∀ (h : Membership.mem (γ := List α) [] x), Membership.mem (γ := List α) [] (prev [] x h)
⊢ l.prev x h ∈ l
have cons : ∀ (hd : α) (tl : List α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
have pos : ∀ (hx : x = hd), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
Tactic: by_cases hx : x = hd
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
pos : ∀ (hx : x = hd), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
have neg : ∀ (hx : ¬x = hd), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
Tactic: by_cases hx : x = hd
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
have pos : (hd' :: tl).getLast sorry ∈ hd :: hd' :: tl
Tactic: simp only [hx, prev_cons_cons_eq]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
have neg : (if x = hd' then hd else (hd' :: tl).prev x sorry) ∈ hd :: hd' :: tl
Tactic: rw [prev, dif_neg hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
have pos : ∀ (hm : x = hd'), hd ∈ hd :: hd' :: tl
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd' : α
tl : List α
hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
hd : α
h : x ∈ hd :: hd' :: tl
hx : ¬x = hd
pos : ∀ (hm : x = hd'), hd ∈ hd :: hd' :: tl
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
have neg : ∀ (hm : ¬x = hd'), (hd' :: tl).prev x sorry ∈ hd :: hd' :: tl
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
⊢ (hd :: tl).prev x h ∈ hd :: tl
have cons : ∀ (hd : α) (h : x ∈ [hd]), [hd].prev x h ∈ [hd]
Tactic: induction tl generalizing hd with
  | nil => simp
  | cons hd' tl hl =>
    by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)
Cleared hypotheses: hd, tl, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
cons : ∀ (hd : α) (h : x ∈ [hd]), [hd].prev x h ∈ [hd]
⊢ (hd :: tl).prev x h ∈ hd :: tl
have cons₁ : ∀ (hd' : α) (tl : List α) (hl : ∀ (hd : α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl) (hd : α)
  (h : x ∈ hd :: hd' :: tl), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
Tactic: induction tl generalizing hd with
  | nil => simp
  | cons hd' tl hl =>
    by_cases hx : x = hd
    · simp only [hx, prev_cons_cons_eq]
      exact mem_cons_of_mem _ (getLast_mem _)
    · rw [prev, dif_neg hx]
      split_ifs with hm
      · exact mem_cons_self
      · exact mem_cons_of_mem _ (hl _ _)
Cleared hypotheses: hd, tl, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
⊢ some ((x :: y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tail) (idxOf a (x :: y :: tail) + 1)
have rw : some (if a = x then y else (y :: tail).nextOr a d) =
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
Tactic: rw [getElem?_cons_succ, nextOr]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
⊢ some (if a = x then y else (y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
have pos : ∀ (hx : a = x),
  some y = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
pos :
  ∀ (hx : a = x),
    some y = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
⊢ some (if a = x then y else (y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
have neg : ∀ (hx : ¬a = x),
  some ((y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ some ((y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))
have neg : a ∈ (y :: tail).dropLast
Tactic: rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d] <:+: l
have refine_1 : [a, l.nextOr a d].length + idxOf a l ≤ l.length
Tactic: refine infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
refine_1 : [a, l.nextOr a d].length + idxOf a l ≤ l.length
⊢ [a, l.nextOr a d] <:+: l
have refine_2 : ∀ (i : ℕ) (hi : i < [a, l.nextOr a d].length),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
Tactic: refine infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length
have refine_1 : ∀ (w : List α), l.dropLast ++ w = l → [a, l.nextOr a d].length + idxOf a l ≤ l.length
Tactic: have ⟨_, _⟩ := l.dropLast_prefix
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
have pos : ∀ (hi₁ : i = 1),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
Tactic: by_cases hi₁ : i = 1
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
pos :
  ∀ (hi₁ : i = 1),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
      some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
have neg : ∀ (hi₁ : ¬i = 1),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + idxOf a l) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a, l.nextOr a d] i hi)
Tactic: by_cases hi₁ : i = 1
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (if (x :: y :: tail).getLast hl = x then y else (y :: tail).nextOr ((x :: y :: tail).getLast hl) d) = d
have pos : ∀ (h' : (x :: y :: tail).getLast hl = x), y = d
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
pos : ∀ (h' : (x :: y :: tail).getLast hl = x), y = d
⊢ (if (x :: y :: tail).getLast hl = x then y else (y :: tail).nextOr ((x :: y :: tail).getLast hl) d) = d
have neg : ∀ (h' : ¬(x :: y :: tail).getLast hl = x), (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
h' : ¬(x :: y :: tail).getLast hl = x
⊢ (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
have neg : (y :: tail).getLast sorry ∉ (y :: tail).dropLast
Tactic: apply nextOr_getLast_of_notMem_dropLast
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯
have hl : l ≠ []
Tactic: have hl := ne_nil_of_mem ha
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯
have pos : ∀ (ha' : a ∈ l.dropLast),
  l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) sorry
Tactic: by_cases ha' : a ∈ l.dropLast