awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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_1 : List α
hl' : List.IsChain (flip r) l_1
l' l : List.chains r
h_1 : ∀ (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 α))
hm : List.IsChain (flip r) []
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hm)
have cons : ∀ (y : List.chains r),
  List.lex_chains r y (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) [] hm) → Acc (List.lex_chains r) y
Tactic: apply Acc.intro
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
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'
⊢ ∀ (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)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : Acc r a
⊢ Acc (List.lex_chains r) (Subtype.mk (p := fun (l : List α) ↦ List.IsChain (flip r) l) (a :: l) hl)
have 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)
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
Cleared hypotheses: l, hl, acc
-- Lean 4 proof step from Mathlib.Data.List.ChainOfFn (goal)
Goal:
α : Type u_1
n : ℕ
f : Fin n → α
r : α → α → Prop
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
have simp_rw : (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length),
    r (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) i sorry)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (ofFn f) (i + 1) _hi)) ↔
  ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, sorry⟩) (f ⟨i + 1, hi⟩)
Tactic: simp_rw [isChain_iff_getElem, List.getElem_ofFn, length_ofFn]
-- Lean 4 proof step from Mathlib.Data.List.ChainOfFn (goal)
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⟩)
⊢ IsChain r (ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)
have simp_rw₁ : (∀ (i : ℕ) (_hi : i + 1 < (ofFn f).length), r (f ⟨i, sorry⟩) (f ⟨i + 1, sorry⟩)) ↔
  ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, sorry⟩) (f ⟨i + 1, hi⟩)
Tactic: simp_rw [isChain_iff_getElem, List.getElem_ofFn, length_ofFn]
-- Lean 4 proof step from Mathlib.Data.List.Count (goal)
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₂
have refine : countP p l₁ = countP p (l₁.diff l₂) + countP p l₂
Tactic: refine (Nat.sub_eq_of_eq_add ?_).symm
-- Lean 4 proof step from Mathlib.Data.List.Count (goal)
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₂) + countP p l₂
have rw : countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
Tactic: rw [← countP_append]
-- Lean 4 proof step from Mathlib.Data.List.Count (goal)
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 : α
⊢ count (f x) (map f l) = count x l
have simp : countP ((fun (x_1 : β) ↦ x_1 == f x) ∘ f) l = countP (fun (x_1 : α) ↦ x_1 == x) l
Tactic: simp only [count, countP_map]
-- Lean 4 proof step from Mathlib.Data.List.Count (goal)
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 : β) ↦ x_1 == f x) ∘ f) l = countP (fun (x_1 : α) ↦ x_1 == x) l
have unfold : countP (fun (x_1 : α) ↦ (fun (x_2 : β) ↦ x_2 == f x) (f x_1)) l = countP (fun (x_1 : α) ↦ x_1 == x) l
Tactic: unfold Function.comp
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
⊢ (y :: xs).nextOr x d = xs.nextOr x d
have nil : [y].nextOr x d = nextOr [] x d
Tactic: rcases xs with - | ⟨z, zs⟩
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
y x d : α
h : x ≠ y
nil : [y].nextOr x d = nextOr [] x d
⊢ (y :: xs).nextOr x d = xs.nextOr x d
have cons : ∀ (z : α) (zs : List α), (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d
Tactic: rcases xs with - | ⟨z, zs⟩
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
⊢ xs.nextOr x d = xs.nextOr x d'
have 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'
Tactic: induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_
Cleared hypotheses: xs, x_mem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
have 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'
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, IH, x_mem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (y :: ys).nextOr x d = (y :: ys).nextOr x d'
have 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'
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, IH, x_mem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have pos : ∀ (h : x = y), (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have neg : ∀ (h : ¬x = y), (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have pos : (y :: z :: zs).nextOr y d = (y :: z :: zs).nextOr y d'
Tactic: rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have pos₁ : z = (y :: z :: zs).nextOr y d'
Tactic: rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have pos₂ : z = z
Tactic: rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
have neg : x ∈ (z :: zs).dropLast
Tactic: rw [nextOr, nextOr, IH]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
⊢ x ∈ xs
have cons : ∀ (y : α) (ys : List α) (IH : ∀ (h : ys.nextOr x d ≠ d), x ∈ ys) (h : (y :: ys).nextOr x d ≠ d), x ∈ y :: ys
Tactic: induction xs with
  | nil => simp at h
  | cons y ys IH => ?_
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
have cons : ∀ (IH : ∀ (h : nextOr [] x d ≠ d), Membership.mem (γ := List α) [] x) (h : [y].nextOr x d ≠ d), x ∈ [y]
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, IH, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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]
⊢ x ∈ y :: ys
have 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
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, IH, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ x ∈ y :: z :: zs
have pos : ∀ (hx : x = y), x ∈ y :: z :: zs
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ x ∈ y :: z :: zs
have neg : ∀ (hx : ¬x = y), x ∈ y :: z :: zs
Tactic: by_cases hx : x = y
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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
have h₁ : (z :: zs).nextOr x d ≠ d
Tactic: rw [nextOr_cons_of_ne _ _ _ _ hx] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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
⊢ (z :: zs ++ [x]).nextOr x d = d
have hz : ¬x = z
Tactic: obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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
⊢ (z :: zs ++ [x]).nextOr x d = d
have hzs : x ∉ zs
Tactic: obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (z :: zs ++ [x]).nextOr x d = d
have cons : (z :: (zs ++ [x])).nextOr x d = d
Tactic: rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (z :: zs ++ [x]).nextOr x d = d
have cons₁ : (zs ++ [x]).nextOr x d = d
Tactic: rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (z :: zs ++ [x]).nextOr x d = d
have cons₂ : d = d
Tactic: rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
⊢ (xs ++ [x]).nextOr x d = d
have nil : ∀ (h : x ∉ []), ([] ++ [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]
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
nil : ∀ (h : x ∉ []), ([] ++ [x]).nextOr x d = d
⊢ (xs ++ [x]).nextOr x d = d
have 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
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]
Cleared hypotheses: xs, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
hd : d ∈ xs
⊢ xs.nextOr x d ∈ xs
have revert : ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs
Tactic: revert hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
⊢ ∀ (hd : d ∈ xs), xs.nextOr x d ∈ xs
have suffices : ∀ (xs' : List α), (∀ x ∈ xs, x ∈ xs') → 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
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
hd : d ∈ xs'
⊢ xs.nextOr x d ∈ xs'
have 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'
Tactic: induction xs with
  | nil => exact hd
  | cons y ys ih => ?_
Cleared hypotheses: xs, hxs'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
have cons : ∀ (ih : ∀ (hxs' : ∀ (x : α), Membership.mem (γ := List α) [] x → x ∈ xs'), nextOr [] x d ∈ xs')
  (hxs' : ∀ x ∈ [y], x ∈ xs'), [y].nextOr x d ∈ xs'
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, ih, hxs'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (y :: ys).nextOr x d ∈ xs'
have 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'
Tactic: rcases ys with - | ⟨z, zs⟩
Cleared hypotheses: ys, ih, hxs'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (if x = y then z else (z :: zs).nextOr x d) ∈ xs'
have pos : ∀ (h : x = y), z ∈ xs'
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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'
⊢ (if x = y then z else (z :: zs).nextOr x d) ∈ xs'
have neg : ∀ (h : ¬x = y), (z :: zs).nextOr x d ∈ xs'
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hx : x = y
⊢ (y :: z :: l).next x h = z
have rw : (y :: z :: l).nextOr x ((y :: z :: l).get (⟨0, sorry⟩ : Fin (y :: z :: l).length)) = z
Tactic: rw [next, nextOr, if_pos hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: z :: l).next x h = z
have rw₁ : (if x = y then z else (z :: l).nextOr x ((y :: z :: l).get (⟨0, sorry⟩ : Fin (y :: z :: l).length))) = z
Tactic: rw [next, nextOr, if_pos hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: z :: l).next x h = z
have rw₂ : z = z
Tactic: rw [next, nextOr, if_pos hx]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ (y :: l).next x ⋯ = l.next x ⋯
have rwa : (y :: l).nextOr x ((y :: l).get (⟨0, sorry⟩ : Fin (y :: l).length)) = l.next x sorry
Tactic: rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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 ⋯
⊢ (y :: l).next x ⋯ = l.next x ⋯
have rwa₁ : (y :: l).nextOr x ((y :: l).get (⟨0, sorry⟩ : Fin (y :: l).length)) = l.nextOr x (l.get (⟨0, sorry⟩ : Fin l.length))
Tactic: rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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))
⊢ (y :: l).next x ⋯ = l.next x ⋯
have rwa₂ : l.nextOr x ((y :: l).get (⟨0, sorry⟩ : Fin (y :: l).length)) = l.nextOr x (l.get (⟨0, sorry⟩ : Fin l.length))
Tactic: rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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))
⊢ (y :: l).next x ⋯ = l.next x ⋯
have rwa₃ : l.nextOr x (l.get (⟨0, sorry⟩ : Fin l.length)) = l.nextOr x (l.get (⟨0, sorry⟩ : Fin l.length))
Tactic: rwa [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_dropLast]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).next x h = y
have rw : (y :: l ++ [x]).get (⟨0, sorry⟩ : Fin (y :: l ++ [x]).length) = y
Tactic: rw [next, nextOr_concat]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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
⊢ (y :: l ++ [x]).next x h = y
have h₁ : x ∉ y :: l
Tactic: rw [next, nextOr_concat]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
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).next x h = y
have h₁ : (y :: l).getLast sorry ∉ (y :: l).dropLast
Tactic: rw [next, get, ← dropLast_append_getLast (cons_ne_nil y l), hx, nextOr_concat]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
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 ⋯ ∉ (y :: l).dropLast
have h₁ : (y :: l).getLast sorry ∈ l
Tactic: subst hx
Cleared hypotheses: x, h_1, h, hy, hx