awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
have cons : ¬hd = hd'
Tactic: refine ⟨hd, hd', ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ ¬hd = hd'
have hl₁ : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
Tactic: simp only [not_or, mem_cons, nodup_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length
have obtain : ∀ (x y : α) (hxy : x ≠ y) (hx : x ∈ s) (hy : y ∈ s), 2 ≤ s.length
Tactic: obtain ⟨x, y, hxy, hx, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length
have h : ∀ (l : List α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x)
  (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y),
  2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
Tactic: induction s using Quot.inductionOn with | _ l
Cleared hypotheses: s, hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
have h : ∀ (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
  (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y),
  2 ≤ length.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y
h :
  ∀ (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y),
    2 ≤ length.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
have h₁ : ∀ (hd : α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x)
  (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y),
  2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) y
h :
  ∀ (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) []) y),
    2 ≤ length.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
h₁ :
  ∀ (hd : α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x)
    (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y),
    2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
have h₂ : ∀ (hd hd' : α) (tl : List α)
  (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) x)
  (hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl)) y),
  2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: hd' :: tl))
Tactic: rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
Cleared hypotheses: l, hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])
have hx₁ : x = hd
Tactic: simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) x
hy : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd]) y
hx₁ : x = hd
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [hd])
have hy₁ : y = hd
Tactic: simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup
have h₁ : ∀ (l : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)),
  Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
Tactic: induction s using Quot.inductionOn with | _ l
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
have h₁ : ∀ (h : Subsingleton.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])),
  Nodup.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
Tactic: obtain - | ⟨hd, tl⟩ := l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
h₁ :
  ∀ (h : Subsingleton.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])),
    Nodup.{u_1} (α := α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
have h₂ : ∀ (hd : α) (tl : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))),
  Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
Tactic: obtain - | ⟨hd, tl⟩ := l
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) (hd :: tl))
have this : tl = []
Tactic: have : tl = [] := by simpa [Subsingleton, length_eq_zero_iff, Nat.succ_le_succ_iff] using h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
s : Cycle α
h : s.Nodup
⊢ s.Nontrivial ↔ ¬s.length ≤ 1
have h₁ : ∀ (a : List α) (h : Nodup (Quotient.mk'' a)), Nontrivial (Quotient.mk'' a) ↔ ¬length (Quotient.mk'' a) ≤ 1
Tactic: induction s using Quotient.inductionOn'
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
a : List α
h : Nodup (Quotient.mk'' a)
⊢ Nontrivial (Quotient.mk'' a) ↔ ¬length (Quotient.mk'' a) ≤ 1
have h₁ : a.Nodup
Tactic: simp only [mk''_eq_coe, nodup_coe_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
⊢ Eq (α := Multiset (List α)) (lists nil) {[]}
have rw : Eq (α := Multiset (List α)) (lists (↑[] : Cycle α)) {[]}
Tactic: rw [nil, lists_coe, cyclicPermutations_nil, Multiset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
rw : Eq (α := Multiset (List α)) (lists (↑[] : Cycle α)) {[]}
⊢ Eq (α := Multiset (List α)) (lists nil) {[]}
have rw₁ : Eq (α := Multiset (List α)) (↑(cyclicPermutations []) : Multiset (List α)) {[]}
Tactic: rw [nil, lists_coe, cyclicPermutations_nil, Multiset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
rw : Eq (α := Multiset (List α)) (lists (↑[] : Cycle α)) {[]}
rw₁ : Eq (α := Multiset (List α)) (↑(cyclicPermutations []) : Multiset (List α)) {[]}
⊢ Eq (α := Multiset (List α)) (lists nil) {[]}
have rw₂ : Eq (α := Multiset (List α)) (↑[[]] : Multiset (List α)) {[]}
Tactic: rw [nil, lists_coe, cyclicPermutations_nil, Multiset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
rw : Eq (α := Multiset (List α)) (lists (↑[] : Cycle α)) {[]}
rw₁ : Eq (α := Multiset (List α)) (↑(cyclicPermutations []) : Multiset (List α)) {[]}
rw₂ : Eq (α := Multiset (List α)) (↑[[]] : Multiset (List α)) {[]}
⊢ Eq (α := Multiset (List α)) (lists nil) {[]}
have rw₃ : Eq (α := Multiset (List α)) {[]} {[]}
Tactic: rw [nil, lists_coe, cyclicPermutations_nil, Multiset.coe_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : { s : Cycle α // s.Nodup }
s : Cycle α
hs : s.Nodup
⊢ ∃ (a : { l : List α // l.Nodup }),
    (fun (l : { l : List α // l.Nodup }) ↦ Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (↑(↑l : List α) : Cycle α) ⋯)
        a =
      Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) s hs
have h : ∀ (hs : List α) (hs_1 : Nodup (Quotient.mk'' hs)),
  ∃ (a : { l : List α // l.Nodup }),
    (fun (l : { l : List α // l.Nodup }) ↦ Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (↑(↑l : List α) : Cycle α) sorry)
        a =
      Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (Quotient.mk'' hs) hs_1
Tactic: induction s using Quotient.inductionOn' with | _ hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x ↔
    Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
have rw : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) y ↔
  Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
Tactic: rw [eq_of_heq hxy]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
he' : hm ≍ hm'
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₁ h₁ x hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₂ h₂ y hm')
have hxy₁ : x = y
Tactic: rw [heq_iff_eq] at hxy
Cleared hypotheses: hxy, hm, hm', he'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
he' : hm ≍ hm'
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₁ h₁ x hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₂ h₂ y hm')
have subst : ∀ (hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) y) (he' : hm ≍ hm'),
  Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₁ h₁ y hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.next x hx)
      l₂ h₂ y hm')
Tactic: subst x
Cleared hypotheses: x, hxy, hm, he'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
he' : hm ≍ hm'
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₁ h₁ x hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₂ h₂ y hm')
have hxy₁ : x = y
Tactic: rw [heq_iff_eq] at hxy
Cleared hypotheses: hxy, hm, hm', he'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
he' : hm ≍ hm'
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₁ h₁ x hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₂ h₂ y hm')
have subst : ∀ (hm : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) y) (he' : hm ≍ hm'),
  Eq.{u_1 + 1} (α := α)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₁ h₁ y hm)
    ((fun (l : List α) (_hn : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)) (x : α)
          (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) x) ↦
        l.prev x hx)
      l₂ h₂ y hm')
Tactic: subst x
Cleared hypotheses: x, hxy, hm, he'
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.next hs x hx ∈ s
have h : ∀ (a : List α) (hs : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
  (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x),
  Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
    (next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) hs x hx)
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, hs, hx
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
a : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
    (next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) hs x hx)
have h : x ∈ a
Tactic: apply next_mem
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.prev hs x hx ∈ s
have rw : s.reverse.next sorry x sorry ∈ s.reverse
Tactic: rw [← next_reverse_eq_prev, ← mem_reverse_iff]
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a b : List α
hab : (IsRotated.setoid α : List α → List α → Prop) a b
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      a ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have nil : ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) [] b),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
Tactic: rcases a with - | ⟨a, l⟩
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
a b : List α
hab : (IsRotated.setoid α : List α → List α → Prop) a b
nil :
  ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) [] b),
    (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        [] ↔
      (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        b
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      a ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have cons : ∀ (a : α) (l : List α) (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) b),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (a :: l) ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
Tactic: rcases a with - | ⟨a, l⟩
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
hab : (IsRotated.setoid α : List α → List α → Prop) [] b
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have nil : ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) [] []),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      []
Tactic: rcases b with - | ⟨b, m⟩
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.Data.List.Cycle (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
hab : (IsRotated.setoid α : List α → List α → Prop) [] b
nil :
  ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) [] []),
    (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        [] ↔
      (fun (l : List α) ↦
          (match (motive := List α → Prop) l with
            | [] => True
            | a :: m => IsChain r (a :: m ++ [a]) :
            Prop))
        []
⊢ (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      b
have nil₁ : ∀ (b : α) (m : List α) (hab : (IsRotated.setoid α : List α → List α → Prop) [] (b :: m)),
  (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      [] ↔
    (fun (l : List α) ↦
        (match (motive := List α → Prop) l with
          | [] => True
          | a :: m => IsChain r (a :: m ++ [a]) :
          Prop))
      (b :: m)
Tactic: rcases b with - | ⟨b, m⟩
Cleared hypotheses: b, hab