awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f (↑l : Cycle α) = (↑(List.map f l) : Cycle β)

Tactic:
rfl

Premises used: Cycle.ofList, Quot.map, Quotient.map', rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α),
    b ∈ map f (Quotient.mk'' a) ↔ ∃ (a_1 : α), Membership.mem (γ := Cycle α) (Quotient.mk'' a) a_1 ∧ f a_1 = b

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α : List α → List α → Prop) l₁ l₂
⊢ Eq.{u_1 + 1} (α := Multiset (List α)) ((fun (l : List α) ↦ (↑l.cyclicPermutations : Multiset (List α))) l₁)
    ((fun (l : List α) ↦ (↑l.cyclicPermutations : Multiset (List α))) l₂)

Tactic:
simpa using h.cyclicPermutations.perm

Premises used: List.IsRotated.cyclicPermutations, List.IsRotated.perm
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
l : List α
⊢ (↑l : Cycle α).lists = (↑l.cyclicPermutations : Multiset (List α))

Tactic:
rfl

Premises used: Multiset.ofList, Cycle.lists, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
s : Cycle α
l_1 l : List α
⊢ l_1 ∈ (↑l.cyclicPermutations : Multiset (List α)) ↔ (↑l_1 : Cycle α) = Quotient.mk'' l

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
rw : Eq (α := Multiset (List α)) (lists (↑[] : Cycle α)) {[]}
rw₁ : Eq (α := Multiset (List α)) (↑(cyclicPermutations []) : Multiset (List α)) {[]}
rw₂ : Eq (α := Multiset (List α)) (↑[[]] : Multiset (List α)) {[]}
rw₃ rw₄ : Eq (α := Multiset (List α)) {[]} {[]}
⊢ Eq (α := Multiset (List α)) (lists nil) {[]}

Tactic:
rw [nil, lists_coe, cyclicPermutations_nil, Multiset.coe_singleton]

Premises used: List.cyclicPermutations_nil, Cycle.lists_coe, Multiset.coe_singleton, Cycle.nil
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
⊢ ¬Nontrivial.{u_1} (α := α) (↑[] : Cycle α)

Tactic:
simp [Nontrivial]

Premises used: Cycle.Nontrivial
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x : α
⊢ ¬(↑[x] : Cycle α).Nontrivial

Tactic:
simp [Nontrivial]

Premises used: Cycle.Nontrivial
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : x = y
⊢ (↑(x :: y :: l) : Cycle α).Nontrivial ↔ (↑(x :: l) : Cycle α).Nontrivial

Tactic:
simp [h, Nontrivial]

Premises used: Cycle.Nontrivial
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ x ∈ (↑(x :: y :: l) : Cycle α)

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ y ∈ (↑(x :: y :: l) : Cycle α)

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : { l : List α // l.Nodup }
⊢ (↑(↑l : List α) : Cycle α).Nodup

Tactic:
simpa using l.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : { s : Cycle α // s.Nodup }
s : Cycle α
hs : s.Nodup
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 α) ⋯)
          a =
        Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (Quotient.mk'' hs) hs_1
⊢ ∃ (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

Tactic:
induction s using Quotient.inductionOn' with | _ hs
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : { s : Cycle α // s.Nodup }
hs_1 : List α
hs : Nodup (Quotient.mk'' hs_1)
⊢ (fun (l : { l : List α // l.Nodup }) ↦ Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (↑(↑l : List α) : Cycle α) ⋯)
      (Subtype.mk (p := fun (l : List α) ↦ l.Nodup) hs_1 hs) =
    Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup) (Quotient.mk'' hs_1) hs

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : { s : Cycle α // s.Nodup }
hs_1 : List α
hs : Nodup (Quotient.mk'' hs_1)
⊢ ∃ (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) (Quotient.mk'' hs_1) hs

Tactic:
exact ⟨⟨_, hs⟩, by simp⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ ∀ (x : Cycle α),
    Membership.mem (γ := Finset (Cycle α))
        (Finset.filter Nontrivial
          (Finset.map (α := { s : Cycle α // s.Nodup }) (Function.Embedding.subtype fun (s : Cycle α) ↦ s.Nodup)
            Finset.univ))
        x ↔
      x.Nodup ∧ x.Nontrivial

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
⊢ s.toMultiset.toFinset = s.toFinset

Tactic:
rfl

Premises used: Cycle.toFinset, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ (↑l : Cycle α).toFinset = l.toFinset

Tactic:
rfl

Premises used: Cycle.toMultiset, Cycle.toFinset, List.toFinset, Multiset.ofList, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset nil) ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Cycle.toFinset, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, rfl
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil

Tactic:
simp
-- Module: Mathlib.Data.List.Cycle
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
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
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x ↔
    Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y

Tactic:
rw [eq_of_heq hxy]

Premises used: eq_of_heq
-- Module: Mathlib.Data.List.Cycle
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₁) y ↔
    Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y

Tactic:
simpa [eq_of_heq hxy] using h.mem_iff

Premises used: List.IsRotated.mem_iff, eq_of_heq
-- Module: Mathlib.Data.List.Cycle
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'
⊢ x = y

Tactic:
rw [heq_iff_eq] at hxy

Premises used: heq_iff_eq
-- Module: Mathlib.Data.List.Cycle
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'
hxy₁ : x = y
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x

Tactic:
rw [heq_iff_eq] at hxy

Premises used: heq_iff_eq
-- Module: Mathlib.Data.List.Cycle
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'
hxy₁ : x = y
hm₁ : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₁) x
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y

Tactic:
rw [heq_iff_eq] at hxy

Premises used: heq_iff_eq
-- Module: Mathlib.Data.List.Cycle
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'
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
⊢ hm₁ ≍ hm'₁

Tactic:
rw [heq_iff_eq] at hxy

Premises used: heq_iff_eq
-- Module: Mathlib.Data.List.Cycle
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'
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')
⊢ 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')

Tactic:
subst x
-- Module: Mathlib.Data.List.Cycle
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₂
y : α
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
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:
simpa using isRotated_next_eq h h₁ _

Premises used: List.isRotated_next_eq
-- Module: Mathlib.Data.List.Cycle
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'
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')
⊢ 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')

Tactic:
subst x
-- Module: Mathlib.Data.List.Cycle
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₂
y : α
hm' : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l₂) y
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:
simpa using isRotated_prev_eq h h₁ _

Premises used: List.isRotated_prev_eq
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
⊢ ∀ (hs : s.Nodup) (x : α) (hx : x ∈ s), s.reverse.prev ⋯ x ⋯ = s.next hs x hx

Tactic:
Quotient.inductionOn' s prev_reverse_eq_next

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.prev hs x hx = s.next ⋯ x ⋯

Tactic:
prev_reverse_eq_next s (nodup_reverse_iff.mp hs) x (mem_reverse_iff.mp hx)

Premises used: Cycle.nodup_reverse_iff, Cycle.mem_reverse_iff, Iff.mp, Cycle.prev_reverse_eq_next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ = s.prev hs x hx

Tactic:
simp [← prev_reverse_eq_next]

Premises used: Cycle.prev_reverse_eq_next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.next hs x hx = s.prev ⋯ x ⋯

Tactic:
simp [← prev_reverse_eq_next]

Premises used: Cycle.prev_reverse_eq_next
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
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)
⊢ s.next hs x hx ∈ s

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.Data.List.Cycle
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
h : x ∈ a
⊢ Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)
    (next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) hs x hx)

Tactic:
apply next_mem

Premises used: Cycle.next_mem
-- Module: Mathlib.Data.List.Cycle
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
⊢ x ∈ a

Tactic:
assumption
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
rw : s.reverse.next ⋯ x ⋯ ∈ s.reverse
⊢ s.prev hs x hx ∈ s

Tactic:
rw [← next_reverse_eq_prev, ← mem_reverse_iff]

Premises used: Cycle.mem_reverse_iff, Cycle.next_reverse_eq_prev
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse

Tactic:
apply next_mem

Premises used: Cycle.next_mem
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
⊢ ∀ (hs : s.Nodup) (x : α) (hx : x ∈ s), s.prev hs (s.next hs x hx) ⋯ = x

Tactic:
Quotient.inductionOn' s prev_next

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
⊢ ∀ (hs : s.Nodup) (x : α) (hx : x ∈ s), s.next hs (s.prev hs x hx) ⋯ = x

Tactic:
Quotient.inductionOn' s next_prev

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.List.Cycle
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
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
⊢ (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

Tactic:
rcases a with - | ⟨a, l⟩
-- Module: Mathlib.Data.List.Cycle
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))
        []
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)
⊢ (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 b with - | ⟨b, m⟩
-- Module: Mathlib.Data.List.Cycle
Goal:
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) b
cons :
  ∀ (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) []),
    (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))
        []
cons₁ :
  ∀ (b : α) (m : List α) (hab : (IsRotated.setoid α : List α → List α → Prop) (a :: l) (b :: m)),
    (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 :: m)
⊢ (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 b with - | ⟨b, m⟩