awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
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
hm : ¬x = hd'
⊢ (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_of_mem _ (hl _ _)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x hd : α
tl : List α
h : x ∈ hd :: tl
cons : ∀ (hd : α) (h : x ∈ [hd]), [hd].prev x h ∈ [hd]
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
⊢ (hd :: tl).prev x h ∈ 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 _ _)

Premises used: List.mem_cons_of_mem, List.cons, List.prev_cons_cons_eq, List.prev, List.getLast_mem, List.mem_cons_self, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d : α
ha : Membership.mem (γ := List α) (dropLast []) a
⊢ some (nextOr [] a d) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (idxOf a [] + 1)

Tactic:
simp at ha
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d head : α
ha : a ∈ [head].dropLast
⊢ some ([head].nextOr a d) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [head] (idxOf a [head] + 1)

Tactic:
simp at ha
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
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))
⊢ 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)

Tactic:
rw [getElem?_cons_succ, nextOr]

Premises used: List.nextOr, List.getElem?_cons_succ
-- Module: Mathlib.Data.List.Cycle
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))
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))
⊢ 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:
split_ifs with hx
-- Module: Mathlib.Data.List.Cycle
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 = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
neg : a ∈ (y :: tail).dropLast
⊢ some ((y :: tail).nextOr a d) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (x :: y :: tail))

Tactic:
rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]

Premises used: Ne.symm, List.idxOf_cons_ne
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
hx : ¬a = x
⊢ a ∈ (y :: tail).dropLast

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ some (l.nextOr a d) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l + 1)

Tactic:
match l with
  | nil => simp at ha
  | [head] => simp at ha
  | x :: y :: tail =>
    rw [getElem?_cons_succ, nextOr]
    split_ifs with hx
    · grind
    rw [idxOf_cons_ne _ <| Ne.symm hx, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
    grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ l.nextOr a d = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l + 1) ⋯

Tactic:
Option.some_injective _ <| nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast ha d ▸ getElem?_pos ..

Premises used: Eq.rec, getElem?_pos, List.nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast, Option.some_injective, Eq.symm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d] <:+: l

Tactic:
infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, List.infix_iff_getElem?, List.idxOf
-- Module: Mathlib.Data.List.Cycle
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
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)
⊢ [a, l.nextOr a d] <:+: l

Tactic:
refine infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, List.infix_iff_getElem?, List.idxOf
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
refine_1 : ∀ (w : List α), l.dropLast ++ w = l → [a, l.nextOr a d].length + idxOf a l ≤ l.length
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

Tactic:
have ⟨_, _⟩ := l.dropLast_prefix
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
w : List α
h : l.dropLast ++ w = l
⊢ [a, l.nextOr a d].length + idxOf a l ≤ l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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)
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)
⊢ 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
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
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:
grind [next, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]

Premises used: List.next, List.nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
i : ℕ
hi : i < [a, l.nextOr a d].length
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:
grind [getElem?_idxOf, mem_of_mem_dropLast]

Premises used: List.mem_of_mem_dropLast, List.getElem?_idxOf
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
d : α
hl : Ne.{u_1 + 1} (α := List α) [] []
h : getLast [] hl ∉ dropLast []
⊢ nextOr [] (getLast [] hl) d = d

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
d head : α
hl : [head] ≠ []
h : [head].getLast hl ∉ [head].dropLast
⊢ [head].nextOr ([head].getLast hl) d = d

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
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
neg : ∀ (h' : ¬(x :: y :: tail).getLast hl = x), (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
⊢ (if (x :: y :: tail).getLast hl = x then y else (y :: tail).nextOr ((x :: y :: tail).getLast hl) d) = d

Tactic:
split_ifs with h'
-- Module: Mathlib.Data.List.Cycle
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 = d

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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
neg : (y :: tail).getLast ⋯ ∉ (y :: tail).dropLast
⊢ (y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d

Tactic:
apply nextOr_getLast_of_notMem_dropLast
-- Module: Mathlib.Data.List.Cycle
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).getLast ⋯ ∉ (y :: tail).dropLast

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l ≠ []
h : l.getLast hl ∉ l.dropLast
d : α
⊢ l.nextOr (l.getLast hl) d = d

Tactic:
match l with
  | nil | [_] => simp
  | x :: y :: tail =>
    unfold nextOr
    split_ifs with h'
    · grind
    apply nextOr_getLast_of_notMem_dropLast
    grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l ≠ []
h : l.getLast hl ∉ l.dropLast
⊢ l.get (⟨0, ⋯⟩ : Fin l.length) = l.head hl

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l_1 : List α
x : α
l : List α
a : α
ha : a ∈ l
⊢ 0 < l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l ≠ []

Tactic:
have hl := ne_nil_of_mem ha
-- Module: Mathlib.Data.List.Cycle
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) ⋯
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) ⋯
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯

Tactic:
by_cases ha' : a ∈ l.dropLast

Premises used: List.dropLast
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∈ l.dropLast
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯

Tactic:
simp [next, nextOr_eq_getElem_idxOf_succ_of_mem_dropLast ha',
      Nat.mod_eq_of_lt <| succ_idxOf_lt_length_of_mem_dropLast ha']

Premises used: Nat.mod_eq_of_lt, List.succ_idxOf_lt_length_of_mem_dropLast, List.next, List.nextOr_eq_getElem_idxOf_succ_of_mem_dropLast
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
hl : l ≠ []
ha' : a ∉ l.dropLast
⊢ l.next a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + 1) % l.length) ⋯

Tactic:
grind [dropLast_append_getLast, next_getLast_eq_head_of_notMem_dropLast, Nat.mod_self]

Premises used: Nat.mod_self, List.next_getLast_eq_head_of_notMem_dropLast, List.dropLast_append_getLast
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) ⋯

Tactic:
grind [next_eq_getElem]

Premises used: List.next_eq_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : Membership.mem (γ := List α) [] a
ha₀ : a ≠ head [] ⋯
⊢ some (prev [] a ha) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (idxOf a [] - 1)

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a head : α
ha : a ∈ [head]
ha₀ : a ≠ [head].head ⋯
⊢ some ([head].prev a ha) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [head] (idxOf a [head] - 1)

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
⊢ ∀ (ha : a ∈ y :: tail) (ha₀ : a ≠ (y :: tail).head ⋯),
    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)
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
ih :
  ∀ (ha : a ∈ y :: tail) (ha₀ : a ≠ (y :: tail).head ⋯),
    some ((y :: tail).prev a ha) =
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tail) (idxOf a (y :: tail) - 1)
⊢ 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)

Tactic:
grind [prev]

Premises used: List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ some (l.prev a ha) = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l - 1)

Tactic:
match l with
  | nil | [_] => grind
  | x :: y :: tail =>
    have ih := (y :: tail).prev_eq_getElem?_idxOf_pred_of_ne_head (a := a)
    grind [prev]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l_1 : List α
x : α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ idxOf a l - 1 < l.length

Tactic:
grind [idxOf_lt_length_of_mem]

Premises used: List.idxOf_lt_length_of_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ l.prev a ha = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (idxOf a l - 1) ⋯

Tactic:
Option.some_injective _ <| prev_eq_getElem?_idxOf_pred_of_ne_head ha ha₀ ▸ getElem?_pos ..

Premises used: List.prev_eq_getElem?_idxOf_pred_of_ne_head, Eq.rec, getElem?_pos, Option.some_injective, Eq.symm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ idxOf a l = (idxOf a l.tail).succ

Tactic:
have := cons_head_tail (ne_nil_of_mem ha) ▸ idxOf_cons_ne _ <| Ne.symm ha₀
-- Module: Mathlib.Data.List.Cycle
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].length + (idxOf a l - 1) ≤ l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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
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)
⊢ [l.prev a ha, a] <:+: l

Tactic:
refine infix_iff_getElem?.mpr ⟨l.idxOf a - 1, by grind, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat, List.infix_iff_getElem?, List.idxOf
-- Module: Mathlib.Data.List.Cycle
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)
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)
⊢ 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
-- Module: Mathlib.Data.List.Cycle
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
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)
⊢ 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:
subst hi₁
-- Module: Mathlib.Data.List.Cycle
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
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:
grind
-- Module: Mathlib.Data.List.Cycle
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)

Tactic:
grind [prev_eq_getElem?_idxOf_pred_of_ne_head]

Premises used: List.prev_eq_getElem?_idxOf_pred_of_ne_head
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a : α
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} (α := α) []) ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
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) ⋯
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) ⋯
⊢ (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) ⋯

Tactic:
by_cases ha₀ : a = head
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : a = head
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) ⋯
⊢ (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) ⋯

Tactic:
subst ha₀
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
pos : (a :: tail).getLast ⋯ = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) tail.length ⋯
⊢ (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) ⋯

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
⊢ (a :: tail).getLast ⋯ = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) tail.length ⋯

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
neg :
  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) ⋯
⊢ (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) ⋯

Tactic:
rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]

Premises used: List.prev_eq_getElem_idxOf_pred_of_ne_head
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
neg : idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length
⊢ 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) ⋯

Tactic:
congr
-- Module: Mathlib.Data.List.Cycle
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)
neg₂ : 1 ≤ (head :: tail).length
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + ((head :: tail).length - 1)) % (head :: tail).length

Tactic:
rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]

Premises used: Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 < (head :: tail).length

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length

Tactic:
grind