awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
rwa : (y :: l).nextOr x ((y :: l).get (⟨0, ⋯⟩ : Fin (y :: l).length)) = l.next x ⋯
rwa₁ : (y :: l).nextOr x ((y :: l).get (⟨0, ⋯⟩ : Fin (y :: l).length)) = l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length))
rwa₂ : l.nextOr x ((y :: l).get (⟨0, ⋯⟩ : Fin (y :: l).length)) = l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length))
rwa₃ : l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length)) = l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length))
d' : α
x_mem : x ∈ l.dropLast
rwa₄ : l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length)) = l.nextOr x (l.get (⟨0, ⋯⟩ : Fin l.length))
d'₁ : α
x_mem₁ x_mem₂ x_mem₃ : x ∈ l.dropLast
⊢ (y :: l).next x ⋯ = l.next x ⋯

Tactic:
rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]

Premises used: List.nextOr_eq_nextOr_of_mem_dropLast, List.nextOr_cons_of_ne, List.next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
rw : (y :: l ++ [x]).get (⟨0, ⋯⟩ : Fin (y :: l ++ [x]).length) = y
h₁ : x ∉ y :: l
⊢ (y :: l ++ [x]).next x h = y

Tactic:
rw [next, nextOr_concat]

Premises used: List.nextOr_concat, List.next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).get (⟨0, ⋯⟩ : Fin (y :: l ++ [x]).length) = y

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ x ∉ y :: l

Tactic:
simp [hy, hx]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
h₁ : (y :: l).getLast ⋯ ∉ (y :: l).dropLast
⊢ (y :: l).next x h = y

Tactic:
rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]

Premises used: List.nextOr_concat, List.get, List.next, List.cons_ne_nil, List.dropLast_append_getLast
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
⊢ (y :: l).getLast ⋯ ∈ l

Tactic:
subst hx
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
h₁ : (y :: l).getLast ⋯ ∈ l
⊢ (y :: l).getLast ⋯ ∈ y :: l

Tactic:
subst hx
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h_1 : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x = (y :: l).getLast ⋯
hl : l.Nodup
h₁ : (y :: l).getLast ⋯ ∈ l
h₂ : (y :: l).getLast ⋯ ∈ y :: l
⊢ (y :: l).getLast ⋯ ≠ y

Tactic:
subst hx
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
h₁ :
  ∀ (hk : 0 < (y :: l).dropLast.length)
    (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast 0 hk = (y :: l).getLast ⋯),
    False
h₂ :
  ∀ (k : ℕ) (hk : k + 1 < (y :: l).dropLast.length)
    (hk' :
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯),
    False
⊢ False

Tactic:
obtain ⟨_ | k, hk, hk'⟩ := getElem_of_mem H

Premises used: List.getElem_of_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
hk : 0 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast 0 hk = (y :: l).getLast ⋯
⊢ False

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
this : k + 1 = l.length
⊢ False

Tactic:
simp [this] at hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
h₁ : k + 1 = l.length
⊢ False

Tactic:
suffices k + 1 = l.length by simp [this] at hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
y : α
hl : l.Nodup
h_1 : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: l).dropLast (k + 1) hk = (y :: l).getLast ⋯
h₁ :
  ∀ (hl : Nodup.{u_1} (α := α) []) (h : Membership.mem (γ := List α) [] ([y].getLast ⋯)) (h : [y].getLast ⋯ ∈ [y])
    (hy : [y].getLast ⋯ ≠ y) (H : [y].getLast ⋯ ∈ [y].dropLast) (hk : k + 1 < [y].dropLast.length)
    (hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [y].dropLast (k + 1) hk = [y].getLast ⋯),
    k + 1 = length.{u_1} (α := α) []
h₂ :
  ∀ (hd : α) (tl : List α) (hl : (hd :: tl).Nodup) (h : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl)
    (h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl) (hy : (y :: hd :: tl).getLast ⋯ ≠ y)
    (H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast) (hk : k + 1 < (y :: hd :: tl).dropLast.length)
    (hk' :
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
        (y :: hd :: tl).getLast ⋯),
    k + 1 = (hd :: tl).length
⊢ k + 1 = l.length

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hl : Nodup.{u_1} (α := α) []
h_1 : Membership.mem (γ := List α) [] ([y].getLast ⋯)
h : [y].getLast ⋯ ∈ [y]
hy : [y].getLast ⋯ ≠ y
H : [y].getLast ⋯ ∈ [y].dropLast
hk : k + 1 < [y].dropLast.length
hk' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [y].dropLast (k + 1) hk = [y].getLast ⋯
⊢ k + 1 = length.{u_1} (α := α) []

Tactic:
simp at hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ Function.Injective (hd :: tl).get

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
⊢ (y :: hd :: tl).getLast ⋯ ∈ hd :: tl

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
h₁ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
⊢ (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
h₁ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h₂ : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
⊢ (y :: hd :: tl).getLast ⋯ ≠ y

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
h₁ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h₂ : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy₁ : (y :: hd :: tl).getLast ⋯ ≠ y
⊢ (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
h₁ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h₂ : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy₁ : (y :: hd :: tl).getLast ⋯ ≠ y
H₁ : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
⊢ k + 1 < (y :: hd :: tl).dropLast.length

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
hl₁ : Function.Injective (hd :: tl).get
h₁ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h₂ : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy₁ : (y :: hd :: tl).getLast ⋯ ≠ y
H₁ : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk₁ : k + 1 < (y :: hd :: tl).dropLast.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk₁ =
    (y :: hd :: tl).getLast ⋯

Tactic:
rw [nodup_iff_injective_get] at hl

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
h₁ : k = tl.length
⊢ k + 1 = (hd :: tl).length

Tactic:
rw [length, Nat.succ_inj]

Premises used: Nat.succ_inj, List.length
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ k.succ < (hd :: tl).length

Tactic:
simpa using hk
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ tl.length < (hd :: tl).length

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ (hd :: tl).get (⟨k, ⋯⟩ : Fin (hd :: tl).length) = (hd :: tl).get ⟨tl.length, ⋯⟩

Tactic:
grind
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h_1 : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' :
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: hd :: tl).dropLast (k + 1) hk =
    (y :: hd :: tl).getLast ⋯
⊢ k = tl.length

Tactic:
exact Fin.val_eq_of_eq <| @hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩
      ⟨tl.length, by simp⟩ (by grind)

Premises used: Fin.val_eq_of_eq
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hxy : x ∈ y :: l
hx : x = y
nil : ∀ (hxy : x ∈ [y]), [y].prev x hxy = [y].getLast ⋯
cons :
  ∀ (head : α) (tail : List α) (hxy : x ∈ y :: head :: tail),
    (y :: head :: tail).prev x hxy = (y :: head :: tail).getLast ⋯
⊢ (y :: l).prev x hxy = (y :: l).getLast ⋯

Tactic:
cases l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
hx : x = y
hxy : x ∈ [y]
⊢ [y].prev x hxy = [y].getLast ⋯

Tactic:
simp [prev, hx]

Premises used: List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
hx : x = y
head : α
tail : List α
hxy : x ∈ y :: head :: tail
⊢ (y :: head :: tail).prev x hxy = (y :: head :: tail).getLast ⋯

Tactic:
simp [prev, hx]

Premises used: List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ x :: l
⊢ (x :: l).prev x h = (x :: l).getLast ⋯

Tactic:
prev_getLast_cons' l x x h rfl

Premises used: List.prev_getLast_cons', rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
hl : Ne.{u_1 + 1} (α := List α) [] []
⊢ prev [] (head [] hl) ⋯ = getLast [] hl

Tactic:
contradiction
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
hl : head :: tail ≠ []
⊢ (head :: tail).prev ((head :: tail).head hl) ⋯ = (head :: tail).getLast hl

Tactic:
apply prev_getLast_cons

Premises used: List.prev_getLast_cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l ≠ []
nil : ∀ (hl : Ne.{u_1 + 1} (α := List α) [] []), prev [] (head [] hl) ⋯ = getLast [] hl
cons :
  ∀ (head : α) (tail : List α) (hl : head :: tail ≠ []),
    (head :: tail).prev ((head :: tail).head hl) ⋯ = (head :: tail).getLast hl
⊢ l.prev (l.head hl) ⋯ = l.getLast hl

Tactic:
cases l with
  | nil => contradiction
  | cons head tail => apply prev_getLast_cons

Premises used: List.head, List.tail, List.prev_getLast_cons, List.cons, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
rw : (if hx : x = y then (z :: l).getLast ⋯ else if x = z then y else (z :: l).prev x ⋯) = (z :: l).getLast ⋯
rw₁ rw₂ : (z :: l).getLast ⋯ = (z :: l).getLast ⋯
⊢ (y :: z :: l).prev x h = (z :: l).getLast ⋯

Tactic:
rw [prev, dif_pos hx]

Premises used: dif_pos, List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x z : α
h : x ∈ x :: z :: l
⊢ (x :: z :: l).prev x h = (z :: l).getLast ⋯

Tactic:
prev_cons_cons_eq' l x x z h rfl

Premises used: List.prev_cons_cons_eq', rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x = z
nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = y
cons : ∀ (head : α) (tail : List α) (h : x ∈ y :: z :: head :: tail), (y :: z :: head :: tail).prev x h = y
⊢ (y :: z :: l).prev x h = y

Tactic:
cases l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
h : x ∈ [y, z]
⊢ [y, z].prev x h = y

Tactic:
simp [prev, hz]

Premises used: List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x = z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons : (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) = y
cons₁ : (if x = z then y else (z :: head :: tail).prev x ⋯) = y
cons₂ cons₃ : y = y
⊢ (y :: z :: head :: tail).prev x h = y

Tactic:
rw [prev, dif_neg hy, if_pos hz]

Premises used: if_pos, dif_neg, List.prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
h : x ∈ y :: x :: l
hy : x ≠ y
⊢ (y :: x :: l).prev x h = y

Tactic:
prev_cons_cons_of_ne' _ _ _ _ _ hy rfl

Premises used: List.prev_cons_cons_of_ne', rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x ∈ z :: l

Tactic:
simpa [hy] using h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
nil : ∀ (h : x ∈ [y, z]), [y, z].prev x h = [z].prev x ⋯
cons :
  ∀ (head : α) (tail : List α) (h : x ∈ y :: z :: head :: tail),
    (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x ⋯
⊢ (y :: z :: l).prev x h = (z :: l).prev x ⋯

Tactic:
cases l
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
h : x ∈ [y, z]
⊢ [y, z].prev x h = [z].prev x ⋯

Tactic:
simp [hy, hz] at h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y z : α
hy : x ≠ y
hz : x ≠ z
head : α
tail : List α
h : x ∈ y :: z :: head :: tail
cons :
  (if hx : x = y then (z :: head :: tail).getLast ⋯ else if x = z then y else (z :: head :: tail).prev x ⋯) =
    (z :: head :: tail).prev x ⋯
cons₁ : (if x = z then y else (z :: head :: tail).prev x ⋯) = (z :: head :: tail).prev x ⋯
cons₂ cons₃ : (z :: head :: tail).prev x ⋯ = (z :: head :: tail).prev x ⋯
⊢ (y :: z :: head :: tail).prev x h = (z :: head :: tail).prev x ⋯

Tactic:
rw [prev, dif_neg hy, if_neg hz]

Premises used: dif_neg, List.prev, if_neg
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.next x h ∈ l

Tactic:
nextOr_mem (get_mem _ _)

Premises used: List.nextOr_mem, List.next, List.get_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
nil : ∀ (h : Membership.mem (γ := List α) [] x), Membership.mem (γ := List α) [] (prev [] x h)
cons : ∀ (hd : α) (tl : List α) (h : x ∈ hd :: tl), (hd :: tl).prev x h ∈ hd :: tl
⊢ l.prev x h ∈ l

Tactic:
rcases l with - | ⟨hd, tl⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x : α
h : Membership.mem (γ := List α) [] x
⊢ Membership.mem (γ := List α) [] (prev [] x h)

Tactic:
simp at h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x hd : α
h : x ∈ [hd]
⊢ [hd].prev x h ∈ [hd]

Tactic:
simp
-- 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
pos : ∀ (hx : x = hd), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
neg : ∀ (hx : ¬x = hd), (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
by_cases hx : x = hd
-- 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
pos : (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
simp only [hx, prev_cons_cons_eq]

Premises used: List.prev_cons_cons_eq
-- 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
⊢ (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl

Tactic:
mem_cons_of_mem _ (getLast_mem _)

Premises used: List.mem_cons_of_mem, List.getLast_mem
-- 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
⊢ (hd' :: tl).getLast ⋯ ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_of_mem _ (getLast_mem _)

Premises used: List.mem_cons_of_mem, List.getLast_mem
-- 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
neg : (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl
⊢ (hd :: hd' :: tl).prev x h ∈ hd :: hd' :: tl

Tactic:
rw [prev, dif_neg hx]

Premises used: dif_neg, List.prev
-- 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
pos : ∀ (hm : x = hd'), hd ∈ hd :: hd' :: tl
neg : ∀ (hm : ¬x = hd'), (hd' :: tl).prev x ⋯ ∈ hd :: hd' :: tl
⊢ (if x = hd' then hd else (hd' :: tl).prev x ⋯) ∈ hd :: hd' :: tl

Tactic:
split_ifs with hm
-- 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 ∈ hd :: hd' :: tl

Tactic:
mem_cons_self

Premises used: List.mem_cons_self
-- 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 ∈ hd :: hd' :: tl

Tactic:
exact mem_cons_self

Premises used: List.mem_cons_self
-- 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:
mem_cons_of_mem _ (hl _ _)

Premises used: List.mem_cons_of_mem