awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih :
  ∀ (y : α),
    r y a →
      ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl)
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r
this : Acc (List.lex_chains r) l'
cons :
  ∀ (l : List.chains r),
    (∀ (y : List.chains r), List.lex_chains r y l → Acc (List.lex_chains r) y) →
      ∀
        (ihl :
          ∀ (y : List.chains r),
            List.lex_chains r y l →
              ∀ (hl : List.IsChain (flip r) (a :: (↑y : List α))),
                Acc (List.lex_chains r)
                  (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑y : List α)) hl))
        (hl : List.IsChain (flip r) (a :: (↑l : List α))),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l : List α)) hl)
⊢ ∀ (hl : List.IsChain (flip r) (a :: (↑l' : List α))),
    Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: (↑l' : List α)) hl)

Tactic:
induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : Acc r a
cons :
  ∀ (a : α),
    (∀ (y : α), r y a → Acc r y) →
      ∀
        (ih :
          ∀ (y : α),
            r y a →
              ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)),
                Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (y :: l) hl))
        (l : List α) (hl : List.IsChain (flip r) (a :: l)),
        Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)

Tactic:
induction acc generalizing l with
  | intro a _ ih =>
    /- Bundle l with a proof that it is r-decreasing to form l' -/
    have hl' := (List.isChain_cons.1 hl).2
    let l' : List.chains r := ⟨l, hl'⟩
    have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.isChain_cons_cons.1 hl).1
    /- make l' a free variable and induct on l' -/
    revert hl
    rw [(by rfl : l = l'.1)]
    clear_value l'
    induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

Premises used: Acc.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
hwf : WellFounded r
⊢ WellFounded (List.lex_chains r)

Tactic:
⟨fun _ ↦ Acc.list_chain' (fun _ _ => hwf.apply _)⟩

Premises used: WellFounded.apply, WellFounded.intro, Acc.list_chain'
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u_1
r : α → α → Prop
hwf : IsWellFounded α r
⊢ IsWellFounded (List.chains r) (List.lex_chains r)

Tactic:
⟨hwf.wf.list_chain'⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, WellFounded.list_chain'
-- Module: Mathlib.Data.List.ChainOfFn
Goal:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
simp_rw :
  (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length),
      r (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i ⋯)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) (i + 1) _hi)) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
simp_rw₁ :
  (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length), r (f ⟨i, ⋯⟩) (f ⟨i + 1, ⋯⟩)) ↔
    ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)

Tactic:
simp_rw [isChain_iff_getElem, List.getElem_ofFn, length_ofFn]

Premises used: List.length_ofFn, List.isChain_iff_getElem, List.getElem_ofFn
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
l : List α
p : α → Bool
⊢ countP p l < l.length ↔ ∃ (a : α), a ∈ l ∧ p a = false

Tactic:
simp [Nat.lt_iff_le_and_ne, countP_le_length]

Premises used: Nat.lt_iff_le_and_ne, List.countP_le_length
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l : List α
a : α
⊢ count a l < l.length ↔ ∃ (b : α), b ∈ l ∧ b ≠ a

Tactic:
simp [count]

Premises used: List.count
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
p : α → Bool
l : List α
a : α
⊢ countP p (l.erase a) = countP p l - if a ∈ l ∧ p a = true then 1 else 0

Tactic:
grind [countP_eq_length_filter]

Premises used: List.countP_eq_length_filter
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ count a (l₁.diff (b :: l₂)) = count a l₁ - count a (b :: l₂)

Tactic:
simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons,
      Nat.sub_add_eq]

Premises used: List.count_erase, Nat.sub_add_eq, beq_iff_eq, List.diff_cons, List.count_cons, Nat.sub_right_comm
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
(Nat.sub_eq_of_eq_add ?_).symm

Premises used: Nat.sub_eq_of_eq_add, Eq.symm
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
refine : countP p l₁ = countP p (l₁.diff l₂) + countP p l₂
⊢ countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
refine (Nat.sub_eq_of_eq_add ?_).symm

Premises used: Nat.sub_eq_of_eq_add, Eq.symm
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
rw : countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
⊢ countP p l₁ = countP p (l₁.diff l₂) + countP p l₂

Tactic:
rw [← countP_append]

Premises used: List.countP_append
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)

Tactic:
((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

Premises used: List.Perm.countP_eq, List.Perm.trans, List.subperm_append_diff_self_of_count_le, List.perm_append_comm, Iff.mp, List.Perm.symm, List.subperm_ext_iff
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)

Tactic:
exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

Premises used: List.Perm.countP_eq, List.Perm.trans, List.subperm_append_diff_self_of_count_le, List.perm_append_comm, Iff.mp, List.Perm.symm, List.subperm_ext_iff
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
simp : countP ((fun (x_1 : β) ↦ x_1 == f x) ∘ f) l = countP (fun (x_1 : α) ↦ x_1 == x) l
⊢ count (f x) (map f l) = count x l

Tactic:
simp only [count, countP_map]

Premises used: List.countP_map, List.count
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
unfold : countP (fun (x_1 : α) ↦ (fun (x_2 : β) ↦ x_2 == f x) (f x_1)) l = countP (fun (x_1 : α) ↦ x_1 == x) l
⊢ countP ((fun (x_1 : β) ↦ x_1 == f x) ∘ f) l = countP (fun (x_1 : α) ↦ x_1 == x) l

Tactic:
unfold Function.comp

Premises used: Function.comp
-- Module: Mathlib.Data.List.Count
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ countP (fun (x_1 : α) ↦ (fun (x_2 : β) ↦ x_2 == f x) (f x_1)) l = countP (fun (x_1 : α) ↦ x_1 == x) l

Tactic:
simp only [hf.beq_eq]

Premises used: Function.Injective.beq_eq
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
⊢ nextOr [] x d = d

Tactic:
rfl

Premises used: List.nextOr, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y d : α
⊢ [y].nextOr x d = d

Tactic:
rfl

Premises used: List.nextOr, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x y d : α
⊢ (x :: y :: xs).nextOr x d = y

Tactic:
if_pos rfl

Premises used: List.nextOr, if_pos, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
nil : [y].nextOr x d = nextOr [] x d
cons : ∀ (z : α) (zs : List α), (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d
⊢ (y :: xs).nextOr x d = xs.nextOr x d

Tactic:
rcases xs with - | ⟨z, zs⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = nextOr [] x d

Tactic:
rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
if_neg h

Premises used: List.nextOr, if_neg
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
exact if_neg h

Premises used: if_neg
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' : α
x_mem : Membership.mem (γ := List α) (dropLast []) x
⊢ nextOr [] x d = nextOr [] x d'

Tactic:
cases x_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y : α
ys : List α
IH : ∀ (x_mem : x ∈ ys.dropLast), ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Tactic:
?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
cons :
  ∀ (y : α) (ys : List α) (IH : ∀ (x_mem : x ∈ ys.dropLast), ys.nextOr x d = ys.nextOr x d')
    (x_mem : x ∈ (y :: ys).dropLast), (y :: ys).nextOr x d = (y :: ys).nextOr x d'
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y : α
ys : List α
IH : ∀ (x_mem : x ∈ ys.dropLast), ys.nextOr x d = ys.nextOr x d'
x_mem : x ∈ (y :: ys).dropLast
cons :
  ∀ (IH : ∀ (x_mem : Membership.mem (γ := List α) (dropLast []) x), nextOr [] x d = nextOr [] x d')
    (x_mem : x ∈ [y].dropLast), [y].nextOr x d = [y].nextOr x d'
cons₁ :
  ∀ (z : α) (zs : List α) (IH : ∀ (x_mem : x ∈ (z :: zs).dropLast), (z :: zs).nextOr x d = (z :: zs).nextOr x d')
    (x_mem : x ∈ (y :: z :: zs).dropLast), (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'

Tactic:
rcases ys with - | ⟨z, zs⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y : α
IH : ∀ (x_mem : Membership.mem (γ := List α) (dropLast []) x), nextOr [] x d = nextOr [] x d'
x_mem : x ∈ [y].dropLast
⊢ [y].nextOr x d = [y].nextOr x d'

Tactic:
simp at x_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ (z :: zs).dropLast), (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
pos : ∀ (h : x = y), (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
neg : ∀ (h : ¬x = y), (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
by_cases h : x = y
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ (z :: zs).dropLast), (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
pos : (y :: z :: zs).nextOr y d = (y :: z :: zs).nextOr y d'
pos₁ : z = (y :: z :: zs).nextOr y d'
pos₂ pos₃ : z = z
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]

Premises used: List.nextOr_self_cons_cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ (z :: zs).dropLast), (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
neg : x ∈ (z :: zs).dropLast
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [nextOr, nextOr, IH]

Premises used: List.nextOr
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d d' y z : α
zs : List α
IH : ∀ (x_mem : x ∈ (z :: zs).dropLast), (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ x ∈ (z :: zs).dropLast

Tactic:
simpa [h] using x_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
h : nextOr [] x d ≠ d
⊢ Membership.mem (γ := List α) [] x

Tactic:
simp at h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y : α
ys : List α
IH : ∀ (h : ys.nextOr x d ≠ d), x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys

Tactic:
?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
cons : ∀ (y : α) (ys : List α) (IH : ∀ (h : ys.nextOr x d ≠ d), x ∈ ys) (h : (y :: ys).nextOr x d ≠ d), x ∈ y :: ys
⊢ x ∈ xs

Tactic:
induction xs with
  | nil => simp at h
  | cons y ys IH => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y : α
ys : List α
IH : ∀ (h : ys.nextOr x d ≠ d), x ∈ ys
h : (y :: ys).nextOr x d ≠ d
cons : ∀ (IH : ∀ (h : nextOr [] x d ≠ d), Membership.mem (γ := List α) [] x) (h : [y].nextOr x d ≠ d), x ∈ [y]
cons₁ :
  ∀ (z : α) (zs : List α) (IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs) (h : (y :: z :: zs).nextOr x d ≠ d),
    x ∈ y :: z :: zs
⊢ x ∈ y :: ys

Tactic:
rcases ys with - | ⟨z, zs⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y : α
IH : ∀ (h : nextOr [] x d ≠ d), Membership.mem (γ := List α) [] x
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

Tactic:
simp at h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y z : α
zs : List α
IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
pos : ∀ (hx : x = y), x ∈ y :: z :: zs
neg : ∀ (hx : ¬x = y), x ∈ y :: z :: zs
⊢ x ∈ y :: z :: zs

Tactic:
by_cases hx : x = y
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y z : α
zs : List α
IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs

Tactic:
simp [hx]
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y z : α
zs : List α
IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ (z :: zs).nextOr x d ≠ d

Tactic:
rw [nextOr_cons_of_ne _ _ _ _ hx] at h

Premises used: List.nextOr_cons_of_ne
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y z : α
zs : List α
IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
h₁ : (z :: zs).nextOr x d ≠ d
⊢ ¬x = y

Tactic:
rw [nextOr_cons_of_ne _ _ _ _ hx] at h

Premises used: List.nextOr_cons_of_ne
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d y z : α
zs : List α
IH : ∀ (h : (z :: zs).nextOr x d ≠ d), x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
simpa [hx] using IH h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
h : x ∉ []
⊢ ([] ++ [x]).nextOr x d = d

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d z : α
zs : List α
IH : ∀ (h : x ∉ zs), (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
⊢ ¬x = z

Tactic:
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)

Premises used: Iff.mpr, mt, not_or, Iff.mp, List.mem_cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d z : α
zs : List α
IH : ∀ (h : x ∉ zs), (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
⊢ x ∉ zs

Tactic:
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)

Premises used: Iff.mpr, mt, not_or, Iff.mp, List.mem_cons
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d z : α
zs : List α
IH : ∀ (h : x ∉ zs), (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
cons : (z :: (zs ++ [x])).nextOr x d = d
cons₁ : (zs ++ [x]).nextOr x d = d
cons₂ cons₃ : d = d
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

Premises used: List.nextOr_cons_of_ne, List.cons_append
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
nil : ∀ (h : x ∉ []), ([] ++ [x]).nextOr x d = d
cons :
  ∀ (z : α) (zs : List α) (IH : ∀ (h : x ∉ zs), (zs ++ [x]).nextOr x d = d) (h : x ∉ z :: zs),
    (z :: zs ++ [x]).nextOr x d = d
⊢ (xs ++ [x]).nextOr x d = d

Tactic:
induction xs with
  | nil => simp
  | cons z zs IH =>
    obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
    rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

Premises used: Iff.mpr, mt, not_or, List.cons, Iff.mp, List.mem_cons, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
hd : d ∈ xs
revert : ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs
⊢ xs.nextOr x d ∈ xs

Tactic:
revert hd
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
this : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
⊢ ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs

Tactic:
this xs fun _ => id

Premises used: id
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
this : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
⊢ ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs

Tactic:
exact this xs fun _ => id

Premises used: id
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
suffices : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'
⊢ ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs

Tactic:
suffices ∀ xs' : List α, (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → nextOr xs x d ∈ xs' by
    exact this xs fun _ => id
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'
⊢ nextOr [] x d ∈ xs'

Tactic:
hd

Premises used: List.nextOr
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'
⊢ nextOr [] x d ∈ xs'

Tactic:
exact hd
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ys : List α
ih : ∀ (hxs' : ∀ x ∈ ys, x ∈ xs'), ys.nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: ys, x ∈ xs'
⊢ (y :: ys).nextOr x d ∈ xs'

Tactic:
?_
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
hd : d ∈ xs'
cons :
  ∀ (y : α) (ys : List α) (ih : ∀ (hxs' : ∀ x ∈ ys, x ∈ xs'), ys.nextOr x d ∈ xs') (hxs' : ∀ x ∈ y :: ys, x ∈ xs'),
    (y :: ys).nextOr x d ∈ xs'
⊢ xs.nextOr x d ∈ xs'

Tactic:
induction xs with
  | nil => exact hd
  | cons y ys ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ys : List α
ih : ∀ (hxs' : ∀ x ∈ ys, x ∈ xs'), ys.nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: ys, x ∈ xs'
cons :
  ∀ (ih : ∀ (hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'), nextOr [] x d ∈ xs')
    (hxs' : ∀ x ∈ [y], x ∈ xs'), [y].nextOr x d ∈ xs'
cons₁ :
  ∀ (z : α) (zs : List α) (ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs')
    (hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'), (y :: z :: zs).nextOr x d ∈ xs'
⊢ (y :: ys).nextOr x d ∈ xs'

Tactic:
rcases ys with - | ⟨z, zs⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ih : ∀ (hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'), nextOr [] x d ∈ xs'
hxs' : ∀ x ∈ [y], x ∈ xs'
⊢ [y].nextOr x d ∈ xs'

Tactic:
hd

Premises used: List.nextOr
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ih : ∀ (hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'), nextOr [] x d ∈ xs'
hxs' : ∀ x ∈ [y], x ∈ xs'
⊢ [y].nextOr x d ∈ xs'

Tactic:
exact hd
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
pos : ∀ (h : x = y), z ∈ xs'
neg : ∀ (h : ¬x = y), (z :: zs).nextOr x d ∈ xs'
⊢ (if x = y then z else (z :: zs).nextOr x d) ∈ xs'

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

Tactic:
hxs' _ (mem_cons_of_mem _ mem_cons_self)

Premises used: List.mem_cons_of_mem, List.mem_cons_self
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

Tactic:
exact hxs' _ (mem_cons_of_mem _ mem_cons_self)

Premises used: List.mem_cons_of_mem, List.mem_cons_self
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'

Tactic:
ih fun _ h => hxs' _ (mem_cons_of_mem _ h)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : ∀ (hxs' : ∀ x ∈ z :: zs, x ∈ xs'), (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'

Tactic:
exact ih fun _ h => hxs' _ (mem_cons_of_mem _ h)

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x : α
h : Membership.mem (γ := List α) [] x
⊢ α

Tactic:
simp at h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
y z : α
xs : List α
x : α
h : x ∈ y :: z :: xs
hx : ¬x = y
⊢ x ∈ z :: xs

Tactic:
simpa [hx] using h
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : x ∈ [y]
⊢ [y].next x h = y

Tactic:
rfl

Premises used: List.nextOr, List.get, List.next, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : x ∈ [y]
⊢ [y].prev x h = y

Tactic:
rfl

Premises used: List.prev, rfl
-- 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 : (y :: z :: l).nextOr x ((y :: z :: l).get (⟨0, ⋯⟩ : Fin (y :: z :: l).length)) = z
rw₁ : (if x = y then z else (z :: l).nextOr x ((y :: z :: l).get (⟨0, ⋯⟩ : Fin (y :: z :: l).length))) = z
rw₂ rw₃ : z = z
⊢ (y :: z :: l).next x h = z

Tactic:
rw [next, nextOr, if_pos hx]

Premises used: List.nextOr, if_pos, List.next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x z : α
h : x ∈ x :: z :: l
⊢ (x :: z :: l).next x h = z

Tactic:
next_cons_cons_eq' l x x z h rfl

Premises used: List.next_cons_cons_eq', rfl