awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
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) ⋯
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯
have neg : ∀ (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
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
⊢ some ((x :: y :: tail).prev a ha) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tail) (idxOf a (x :: y :: tail) - 1)
have ih : ∀ (ha : a ∈ y :: tail) (ha₀ : a ≠ (y :: tail).head sorry),
  some ((y :: tail).prev a ha) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (y :: tail) - 1)
Tactic: have ih := (y :: tail).prev_eq_getElem?_idxOf_pred_of_ne_head (a := a)
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ [l.prev a ha, a] <:+: l
have this : idxOf a l = (idxOf a l.tail).succ
Tactic: have := cons_head_tail (ne_nil_of_mem ha) ▸ idxOf_cons_ne _ <| Ne.symm ha₀
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
⊢ [l.prev a ha, a] <:+: l
have refine : ∀ (i : ℕ) (hi : i < [l.prev a ha, a].length),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] i hi)
Tactic: refine infix_iff_getElem?.mpr ⟨l.idxOf a - 1, by grind, 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
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] i hi)
have pos : ∀ (hi₁ : i = 1),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] 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
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
pos :
  ∀ (hi₁ : i = 1),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
      some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] i hi)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] i hi)
have neg : ∀ (hi₁ : ¬i = 1),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] 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
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : i = 1
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (i + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] i hi)
have pos : ∀ (hi : 1 < [l.prev a ha, a].length),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (1 + (idxOf a l - 1)) =
    some (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [l.prev a ha, a] 1 hi)
Tactic: subst hi₁
Cleared hypotheses: i, hi, hi₁
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
⊢ (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
have pos : ∀ (ha₀ : a = head),
  (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) sorry
Tactic: by_cases ha₀ : a = head
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
pos :
  ∀ (ha₀ : a = head),
    (head :: tail).prev a ha =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
        ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
⊢ (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
have neg : ∀ (ha₀ : ¬a = head),
  (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) sorry
Tactic: by_cases ha₀ : a = head
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : a = head
⊢ (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
have pos : ∀ (ha : a ∈ a :: tail),
  (a :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail)
      ((idxOf a (a :: tail) + ((a :: tail).length - 1)) % (a :: tail).length) sorry
Tactic: subst ha₀
Cleared hypotheses: head, ha, ha₀
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
⊢ (a :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail)
      ((idxOf a (a :: tail) + ((a :: tail).length - 1)) % (a :: tail).length) ⋯
have pos : (a :: tail).getLast sorry = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) tail.length sorry
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
have neg : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (idxOf a (head :: tail) - 1) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
    ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) sorry
Tactic: rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail) (idxOf a (head :: tail) - 1) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) ⋯
have neg : idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
have neg : idxOf a (head :: tail) - 1 < (head :: tail).length
Tactic: rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
neg : idxOf a (head :: tail) - 1 < (head :: tail).length
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
have neg₁ : 1 ≤ idxOf a (head :: tail)
Tactic: rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
neg : idxOf a (head :: tail) - 1 < (head :: tail).length
neg₁ : 1 ≤ idxOf a (head :: tail)
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
have neg₂ : 1 ≤ (head :: tail).length
Tactic: rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + (l.length - 1)) % l.length) ⋯
have nil : ∀ (ha : Membership.mem (γ := List α) [] a),
  prev [] a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
      ((idxOf a [] + (length.{u_1} (α := α) [] - 1)) % length.{u_1} (α := α) []) sorry
Tactic: cases l with | nil => grind | cons head tail =>
  by_cases ha₀ : a = head
  · subst ha₀
    simp
    grind
  rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
  congr
  rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
  all_goals grind
Cleared hypotheses: l, ha
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
nil :
  ∀ (ha : Membership.mem (γ := List α) [] a),
    prev [] a ha =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
        ((idxOf a [] + (length.{u_1} (α := α) [] - 1)) % length.{u_1} (α := α) []) ⋯
⊢ l.prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + (l.length - 1)) % l.length) ⋯
have cons : ∀ (head : α) (tail : List α) (ha : a ∈ head :: tail),
  (head :: tail).prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (head :: tail)
      ((idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length) sorry
Tactic: cases l with | nil => grind | cons head tail =>
  by_cases ha₀ : a = head
  · subst ha₀
    simp
    grind
  rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
  congr
  rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
  all_goals grind
Cleared hypotheses: l, ha
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.next (l.getLast h) ⋯ = l.head h
have h1 : l.length - 1 + 1 = l.length
Tactic: have h1 : l.length - 1 + 1 = l.length := by grind [length_pos_iff]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap (P := Membership.mem l) l.next l ⋯ = l.rotate 1
have hl : (pmap (P := Membership.mem l) l.next l sorry).length = (l.rotate 1).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : (pmap (P := Membership.mem l) l.next l ⋯).length = (l.rotate 1).length
⊢ pmap (P := Membership.mem l) l.next l ⋯ = l.rotate 1
have h₁ : ∀ (i : ℕ) (h₁ : i < (pmap (P := Membership.mem l) l.next l sorry).length) (h₂ : i < (l.rotate 1).length),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l sorry) i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
h₁ : i < (pmap (P := Membership.mem l) l.next l ⋯).length
h₂ : i < (l.rotate 1).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l ⋯) i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂
have h₁ : l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂
Tactic: rw [getElem_pmap, getElem_rotate, next_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
h₁_1 : i < (pmap (P := Membership.mem l) l.next l ⋯).length
h₂ : i < (l.rotate 1).length
h₁ :
  l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l ⋯) i h₁_1 =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂
have h₂ : l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i sorry) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) sorry
Tactic: rw [getElem_pmap, getElem_rotate, next_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
h₁_1 : i < (pmap (P := Membership.mem l) l.next l ⋯).length
h₂_1 : i < (l.rotate 1).length
h₁ :
  l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂_1
h₂ :
  l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l ⋯) i h₁_1 =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) i h₂_1
have h₃ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) sorry
Tactic: rw [getElem_pmap, getElem_rotate, next_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap (P := Membership.mem l) l.prev l ⋯ = l.rotate (l.length - 1)
have hl : (pmap (P := Membership.mem l) l.prev l sorry).length = (l.rotate (l.length - 1)).length
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : (pmap (P := Membership.mem l) l.prev l ⋯).length = (l.rotate (l.length - 1)).length
⊢ pmap (P := Membership.mem l) l.prev l ⋯ = l.rotate (l.length - 1)
have h₁ : ∀ (i : ℕ) (h₁ : i < (pmap (P := Membership.mem l) l.prev l sorry).length) (h₂ : i < (l.rotate (l.length - 1)).length),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l sorry) i h₁ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (l.length - 1)) i h₂
Tactic: apply List.ext_getElem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap (P := Membership.mem l) l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l ⋯) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (l.length - 1)) n hn'
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l sorry) n hn =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) sorry
Tactic: rw [getElem_rotate, getElem_pmap, prev_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap (P := Membership.mem l) l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l ⋯) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l ⋯) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (l.length - 1)) n hn'
have h₂ : l.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n sorry) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) sorry
Tactic: rw [getElem_rotate, getElem_pmap, prev_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < (pmap (P := Membership.mem l) l.prev l ⋯).length
hn' : n < (l.rotate (l.length - 1)).length
h₁ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l ⋯) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) ⋯
h₂ :
  l.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.prev l ⋯) n hn =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (l.length - 1)) n hn'
have h₃ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1)) % l.length) sorry
Tactic: rw [getElem_rotate, getElem_pmap, prev_getElem _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev (l.next x hx) ⋯ = x
have obtain : ∀ (n : ℕ) (hn : n < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l),
  l.prev (l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn) hx) sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
Tactic: obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
⊢ l.prev (l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn) hx) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
have simp : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1 + (l.length - 1)) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
Tactic: simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1 + (l.length - 1)) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
have nil : ∀ (h : Nodup.{u_1} (α := α) []) (hn : n < length.{u_1} (α := α) [])
  (hx : Membership.mem (γ := List α) [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn)),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
      ((n + 1 + (length.{u_1} (α := α) [] - 1)) % length.{u_1} (α := α) []) sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, h, hn, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : n < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l
nil :
  ∀ (h : Nodup.{u_1} (α := α) []) (hn : n < length.{u_1} (α := α) [])
    (hx : Membership.mem (γ := List α) [] (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn)),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) []
        ((n + 1 + (length.{u_1} (α := α) [] - 1)) % length.{u_1} (α := α) []) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + 1 + (l.length - 1)) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
have cons : ∀ (hd : α) (tl : List α) (h : (hd :: tl).Nodup) (hn : n < (hd :: tl).length)
  (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn ∈ hd :: tl),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl)
      ((n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length) sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn
Tactic: rcases l with - | ⟨hd, tl⟩
Cleared hypotheses: l, h, hn, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
have hn₁ : n < tl.length + 1
Tactic: rw [length_cons] at hn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn_1 : n < (hd :: tl).length
hn : n < tl.length + 1
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn_1 ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
have rw : (n + (1 + tl.length)) % (tl.length + 1) = n
Tactic: rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn_1 : n < (hd :: tl).length
hn : n < tl.length + 1
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn_1 ∈ hd :: tl
rw : (n + (1 + tl.length)) % (tl.length + 1) = n
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
have rw₁ : (n + (tl.length + 1)) % (tl.length + 1) = n
Tactic: rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn_1 : n < (hd :: tl).length
hn : n < tl.length + 1
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn_1 ∈ hd :: tl
rw : (n + (1 + tl.length)) % (tl.length + 1) = n
rw₁ : (n + (tl.length + 1)) % (tl.length + 1) = n
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
have rw₂ : n % (tl.length + 1) = n
Tactic: rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]