awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
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} (α := α) []) ⋯
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) ⋯
⊢ l.prev a ha =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((idxOf a l + (l.length - 1)) % l.length) ⋯

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

Premises used: List.head, Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt, List.tail, List.cons, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l_1 : List α
x : α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ 0 < l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
⊢ l.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + (l.length - 1)) % l.length) ⋯

Tactic:
grind [prev_eq_getElem]

Premises used: List.prev_eq_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.length - 1 + 1 = l.length

Tactic:
grind [length_pos_iff]

Premises used: List.length_pos_iff
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
⊢ l.length - 1 + 1 = l.length

Tactic:
have h1 : l.length - 1 + 1 = l.length := by grind [length_pos_iff]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
h1 : l.length - 1 + 1 = l.length
⊢ l.length - 1 < l.length

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l ≠ []
hn : l.Nodup
h1 : l.length - 1 + 1 = l.length
⊢ l.next (l.getLast h) ⋯ = l.head h

Tactic:
simp [getLast_eq_getElem h, head_eq_getElem h, next_getElem l hn (l.length - 1) (by grind), h1]

Premises used: List.head_eq_getElem, HSub.hSub, List.next_getElem, List.getLast_eq_getElem, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Cycle
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
h₁ :
  ∀ (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₂
⊢ pmap (P := Membership.mem l) l.next l ⋯ = l.rotate 1

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap (P := Membership.mem l) l.next l ⋯).length = (l.rotate 1).length

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
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) ⋯
h₃ h₄ :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((i + 1) % l.length) ⋯ =
    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

Tactic:
rw [getElem_pmap, getElem_rotate, next_getElem _ h]

Premises used: List.getElem_pmap, List.getElem_rotate, List.next_getElem
-- Module: Mathlib.Data.List.Cycle
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
h₁ :
  ∀ (i : ℕ) (h₁ : i < (pmap (P := Membership.mem l) l.prev l ⋯).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 ⋯) i h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (l.length - 1)) i h₂
⊢ pmap (P := Membership.mem l) l.prev l ⋯ = l.rotate (l.length - 1)

Tactic:
apply List.ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap (P := Membership.mem l) l.prev l ⋯).length = (l.rotate (l.length - 1)).length

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
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) ⋯
h₃ h₄ :
  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) 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'

Tactic:
rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

Premises used: List.getElem_pmap, List.getElem_rotate, List.prev_getElem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
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) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
⊢ l.prev (l.next x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.Data.List.Cycle
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
simp :
  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
⊢ 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

Tactic:
simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]

Premises used: Nat.mod_add_mod, List.prev_getElem, List.next_getElem
-- Module: Mathlib.Data.List.Cycle
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
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) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) 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

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
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

Tactic:
simp at hn
-- Module: Mathlib.Data.List.Cycle
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 < tl.length + 1

Tactic:
rw [length_cons] at hn

Premises used: List.length_cons
-- Module: Mathlib.Data.List.Cycle
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
hn₁ : n < tl.length + 1
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn ∈ hd :: tl

Tactic:
rw [length_cons] at hn

Premises used: List.length_cons
-- Module: Mathlib.Data.List.Cycle
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
rw₂ : n % (tl.length + 1) = n
rw₃ rw₄ : n = n
⊢ (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]

Premises used: add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt, add_comm, OfNat.ofNat
-- Module: Mathlib.Data.List.Cycle
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

Tactic:
have : (n + 1 + length tl) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
-- Module: Mathlib.Data.List.Cycle
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
this : (n + 1 + tl.length) % (tl.length + 1) = n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl)
      ((n + 1 + ((hd :: tl).length - 1)) % (hd :: tl).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn

Tactic:
simp only [length_cons, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, this]

Premises used: List.length_cons, Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
obtain :
  ∀ (n : ℕ) (hn : n < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn ∈ l),
    l.next (l.prev (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
⊢ l.next (l.prev x hx) ⋯ = x

Tactic:
obtain ⟨n, hn, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.Data.List.Cycle
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
simp :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1) + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn
⊢ l.next (l.prev (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

Tactic:
simp only [next_getElem, prev_getElem, h, Nat.mod_add_mod]

Premises used: Nat.mod_add_mod, List.prev_getElem, List.next_getElem
-- Module: Mathlib.Data.List.Cycle
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 + (length.{u_1} (α := α) [] - 1) + 1) % length.{u_1} (α := α) []) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn
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 + ((hd :: tl).length - 1) + 1) % (hd :: tl).length) ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1) + 1) % l.length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
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 + (length.{u_1} (α := α) [] - 1) + 1) % length.{u_1} (α := α) []) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n hn

Tactic:
simp at hn
-- Module: Mathlib.Data.List.Cycle
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 + (tl.length + 1)) % (tl.length + 1) = n
rw₁ : n % (tl.length + 1) = n
rw₂ rw₃ : n = n
⊢ (n + tl.length + 1) % (tl.length + 1) = n

Tactic:
rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]

Premises used: add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt
-- Module: Mathlib.Data.List.Cycle
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 + tl.length + 1) % (tl.length + 1) = n

Tactic:
have : (n + length tl + 1) % (length tl + 1) = n := by
      rw [length_cons] at hn
      rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
-- Module: Mathlib.Data.List.Cycle
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
this : (n + tl.length + 1) % (tl.length + 1) = n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl)
      ((n + ((hd :: tl).length - 1) + 1) % (hd :: tl).length) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (hd :: tl) n hn

Tactic:
simp [this]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
obtain :
  ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
    l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯ =
      l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
⊢ l.reverse.prev x ⋯ = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Premises used: List.getElem_of_mem, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
⊢ 0 < l.length

Tactic:
have lpos : 0 < l.length := k.zero_le.trans_lt hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
⊢ l.length - 1 - k < l.length

Tactic:
lia
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
⊢ l.length - 1 - k < l.length

Tactic:
have key : l.length - 1 - k < l.length := by lia
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < (pmap (P := Membership.mem l) l.next l ⋯).length

Tactic:
simpa using hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
rw :
  l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l ⋯) k ⋯
⊢ l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯ =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx

Tactic:
rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]

Premises used: List.getElem_pmap, List.next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
simp_rw :
  l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l.reverse (l.length - 1 - k) ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯
⊢ l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l ⋯) k ⋯

Tactic:
simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]

Premises used: List.getElem_eq_getElem_reverse, List.pmap_next_eq_rotate_one
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse ⋯) (l.length - 1 - k) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯
rw₁ : l.length - 1 - k < (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse ⋯).length
⊢ l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l.reverse (l.length - 1 - k) ⋯) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯

Tactic:
rw [← getElem_pmap l.reverse.prev fun _ h => h]

Premises used: List.getElem_pmap, List.prev, List.reverse
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
simp_rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (Nat.succ 0)).reverse (l.length - 1 - k) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse ⋯) (l.length - 1 - k) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯

Tactic:
simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]

Premises used: Iff.mpr, Nat.succ_pos', Nat.sub_sub_self, List.nodup_reverse, Nat.succ_le_of_lt, List.length_reverse, Nat.sub_lt, Nat.mod_eq_of_lt, List.rotate_reverse, List.pmap_prev_eq_rotate_length_sub_one
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
rw :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (Nat.succ 0)).reverse.reverse
      ((l.rotate (Nat.succ 0)).reverse.length - 1 - (l.length - 1 - k)) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (Nat.succ 0)).reverse (l.length - 1 - k) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯

Tactic:
rw [getElem_eq_getElem_reverse]

Premises used: List.getElem_eq_getElem_reverse
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (Nat.succ 0)).reverse.reverse
      ((l.rotate (Nat.succ 0)).reverse.length - 1 - (l.length - 1 - k)) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯

Tactic:
simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

Premises used: Nat.sub_sub_self, Nat.le_sub_one_of_lt
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse ⋯).length

Tactic:
simpa
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
⊢ l.reverse.next x ⋯ = l.reverse.reverse.prev x ⋯

Tactic:
(prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm

Premises used: Iff.mpr, List.nodup_reverse, List.mem_reverse, List.prev_reverse_eq_next, List.reverse, Eq.symm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
x : α
hx : x ∈ l
h₁ : l = l.reverse.reverse
⊢ l.reverse.next x ⋯ = l.prev x hx

Tactic:
convert! (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm

Premises used: Iff.mpr, List.nodup_reverse, List.mem_reverse, List.prev_reverse_eq_next, List.reverse, Eq.symm