awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : n % (tl.length + 1) = n
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
have rw₃ : n = 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 (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
⊢ 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
have this : (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]
-- 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.next (l.prev 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.next (l.prev (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.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
have simp : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((n + (l.length - 1) + 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 + (l.length - 1) + 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 + (length.{u_1} (α := α) [] - 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 + (length.{u_1} (α := α) [] - 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 + (l.length - 1) + 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 + ((hd :: tl).length - 1) + 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 + tl.length + 1) % (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 + tl.length + 1) % (tl.length + 1) = n
have rw : (n + (tl.length + 1)) % (tl.length + 1) = n
Tactic: rw [add_assoc, 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 + (tl.length + 1)) % (tl.length + 1) = n
⊢ (n + tl.length + 1) % (tl.length + 1) = n
have rw₁ : n % (tl.length + 1) = n
Tactic: rw [add_assoc, 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 + (tl.length + 1)) % (tl.length + 1) = n
rw₁ : n % (tl.length + 1) = n
⊢ (n + tl.length + 1) % (tl.length + 1) = n
have rw₂ : n = n
Tactic: rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn]
-- 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
⊢ 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
have this : (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]
-- 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.reverse.prev x ⋯ = l.next x hx
have 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) sorry =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
Tactic: obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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
⊢ 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
have lpos : 0 < l.length
Tactic: have lpos : 0 < l.length := k.zero_le.trans_lt hk
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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.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
have key : l.length - 1 - k < l.length
Tactic: have key : l.length - 1 - k < l.length := by lia
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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.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
have rw : l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (pmap (P := Membership.mem l) l.next l sorry) k sorry
Tactic: rw [← getElem_pmap l.next (fun _ h => h) (by simpa using hk)]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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.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 ⋯
have simp_rw : l.reverse.prev (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l.reverse (l.length - 1 - k) sorry) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k sorry
Tactic: simp_rw [getElem_eq_getElem_reverse (l := l), pmap_next_eq_rotate_one _ h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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.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 ⋯
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
    (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse sorry) (l.length - 1 - k) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k sorry
Tactic: rw [← getElem_pmap l.reverse.prev fun _ h => h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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 ⋯
⊢ 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 ⋯
have rw₁ : l.length - 1 - k < (pmap (P := Membership.mem l.reverse) l.reverse.prev l.reverse sorry).length
Tactic: rw [← getElem_pmap l.reverse.prev fun _ h => h]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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)
      (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 ⋯
have simp_rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate (Nat.succ 0)).reverse (l.length - 1 - k) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k sorry
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)]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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 (l.length - 1 - k) ⋯ =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k ⋯
have 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)) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate 1) k sorry
Tactic: rw [getElem_eq_getElem_reverse]
-- 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.reverse.next x ⋯ = l.prev x hx
have h₁ : l = l.reverse.reverse
Tactic: convert! (prev_reverse_eq_next l.reverse (nodup_reverse.mpr h) x (mem_reverse.mpr hx)).symm
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.next x hx = l'.next x ⋯
have obtain : ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
  l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    l'.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) sorry
Tactic: obtain ⟨k, hk, 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 l' : List α
h : l ~r l'
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
⊢ l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    l'.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
have obtain : ∀ (n : ℕ) (h : l ~r l.rotate n),
  l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) sorry
Tactic: obtain ⟨n, rfl⟩ := id h
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) sorry =
  (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) sorry
Tactic: rw [next_getElem _ hn]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) ⋯
have simp_rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) sorry =
  (l.rotate n).next
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
      ((l.length - n % l.length + k) % l.length) sorry)
    sorry
Tactic: simp_rw [getElem_eq_getElem_rotate _ n k]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hn : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
n : ℕ
h : l ~r l.rotate n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯ =
    (l.rotate n).next
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
        ((l.length - n % l.length + k) % l.length) ⋯)
      ⋯
have rw : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
    ((l.length - n % l.length + (k + 1) % l.length) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.rotate n)
    (((l.length - n % l.length + k) % l.length + 1) % (l.rotate n).length) sorry
Tactic: rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.prev x hx = l'.prev x ⋯
have rw : l.reverse.next x sorry = l'.reverse.next x sorry
Tactic: rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
a : α
⊢ (a :: l).rotate 1 = l ++ [a]
have rw : (l ++ [a]).rotate 0 = l ++ [a]
Tactic: rw [rotate_cons_succ, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
a : α
rw : (l ++ [a]).rotate 0 = l ++ [a]
⊢ (a :: l).rotate 1 = l ++ [a]
have rw₁ : l ++ [a] = l ++ [a]
Tactic: rw [rotate_cons_succ, rotate_zero]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
⊢ motive (Quotient.mk'' l)
have refine_1 : motive (Quotient.mk'' [])
Tactic: refine List.recOn l ?_ ?_
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive (↑l : Cycle α) → motive (↑(a :: l) : Cycle α)
l : List α
refine_1 : motive (Quotient.mk'' [])
⊢ motive (Quotient.mk'' l)
have refine_2 : ∀ (head : α) (tail : List α) (tail_ih : motive (Quotient.mk'' tail)), motive (Quotient.mk'' (head :: tail))
Tactic: refine List.recOn l ?_ ?_
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄ (_hx : x ∈ s) ⦃y : α⦄ (_hy : y ∈ s), x = y
have h₁ : ∀ (l : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) ⦃x : α⦄
  (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
  (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y
Tactic: induction s using Quot.inductionOn with | _ l
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y
have h₁ : l = [] ∨ ∃ (a : α), l = [a]
Tactic: simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
    length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
h : l = [] ∨ ∃ (a : α), l = [a]
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y
have h₁ : ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x) ⦃y : α⦄
  (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y), x = y
Tactic: rcases h with (rfl | ⟨z, rfl⟩)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
h : l = [] ∨ ∃ (a : α), l = [a]
h₁ :
  ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    ⦃y : α⦄ (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y), x = y
⊢ ∀ ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ⦃y : α⦄
    (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y), x = y
have h₂ : ∀ (z : α) ⦃x : α⦄ (_hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) x)
  ⦃y : α⦄ (_hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [z]) y), x = y
Tactic: rcases h with (rfl | ⟨z, rfl⟩)
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑l : Cycle α) ∧ y ∈ (↑l : Cycle α)) ↔ 2 ≤ l.length
have nil : ∀ (hl : Nodup.{u_1} (α := α) []),
  (∃ (x : α) (y : α),
      x ≠ y ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) x ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) y) ↔
    2 ≤ List.length.{u_1} (α := α) []
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
hl : l.Nodup
nil :
  ∀ (hl : Nodup.{u_1} (α := α) []),
    (∃ (x : α) (y : α),
        x ≠ y ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) x ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) y) ↔
      2 ≤ List.length.{u_1} (α := α) []
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑l : Cycle α) ∧ y ∈ (↑l : Cycle α)) ↔ 2 ≤ l.length
have cons : ∀ (hd : α) (hl : [hd].Nodup),
  (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑[hd] : Cycle α) ∧ y ∈ (↑[hd] : Cycle α)) ↔ 2 ≤ [hd].length
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
hl : l.Nodup
nil :
  ∀ (hl : Nodup.{u_1} (α := α) []),
    (∃ (x : α) (y : α),
        x ≠ y ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) x ∧ Membership.mem (γ := Cycle α) (↑[] : Cycle α) y) ↔
      2 ≤ List.length.{u_1} (α := α) []
cons :
  ∀ (hd : α) (hl : [hd].Nodup),
    (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑[hd] : Cycle α) ∧ y ∈ (↑[hd] : Cycle α)) ↔ 2 ≤ [hd].length
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑l : Cycle α) ∧ y ∈ (↑l : Cycle α)) ↔ 2 ≤ l.length
have cons₁ : ∀ (hd hd' : α) (tl : List α) (hl : (hd :: hd' :: tl).Nodup),
  (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑(hd :: hd' :: tl) : Cycle α) ∧ y ∈ (↑(hd :: hd' :: tl) : Cycle α)) ↔
    2 ≤ (hd :: hd' :: tl).length
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ (x : α) (y : α), x ≠ y ∧ x ∈ (↑(hd :: hd' :: tl) : Cycle α) ∧ y ∈ (↑(hd :: hd' :: tl) : Cycle α)) ↔
    2 ≤ (hd :: hd' :: tl).length
have cons : ∃ (x : α) (y : α), ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
Tactic: simp only [mem_cons, mem_coe_iff, List.length, Ne, Nat.succ_le_succ_iff,
      Nat.zero_le, iff_true]