awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
pos : ∀ (hx : (f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y), s = s
neg :
  ∀ (hx : (f : (a : α) → α) x = x) (hy : ¬(f : (a : α) → α) y = y),
    (↑(f.toList y) : Cycle α) = (↑(f.toList y) : Cycle α)
pos₁ :
  ∀ (hx : ¬(f : (a : α) → α) x = x) (hy : (f : (a : α) → α) y = y),
    (↑(f.toList x) : Cycle α) = (↑(f.toList x) : Cycle α)
⊢ (if (f : (a : α) → α) x = x then if (f : (a : α) → α) y = y then s else (↑(f.toList y) : Cycle α)
    else (↑(f.toList x) : Cycle α)) =
    if (f : (a : α) → α) y = y then if (f : (a : α) → α) x = x then s else (↑(f.toList x) : Cycle α)
    else (↑(f.toList y) : Cycle α)
have neg₁ : ∀ (hx : ¬(f : (a : α) → α) x = x) (hy : ¬(f : (a : α) → α) y = y), (↑(f.toList x) : Cycle α) = (↑(f.toList y) : Cycle α)
Tactic: split_ifs with hx hy hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
f : Perm α
hf : f.IsCycle
x y : α
m : Multiset α
s : Cycle α
hx : ¬(f : (a : α) → α) x = x
hy : ¬(f : (a : α) → α) y = y
⊢ (↑(f.toList x) : Cycle α) = (↑(f.toList y) : Cycle α)
have hc : f.SameCycle x y
Tactic: have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
⊢ f.toCycle hf = (↑(f.toList x) : Cycle α)
have key : Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x
Tactic: have key : (Finset.univ : Finset α).val = x ::ₘ Finset.univ.val.erase x := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : (f : (a : α) → α) x ≠ x
key : Finset.val Finset.univ = x ::ₘ Multiset.erase (Finset.val Finset.univ) x
⊢ f.toCycle hf = (↑(f.toList x) : Cycle α)
have rw : (x ::ₘ Multiset.erase (Finset.val Finset.univ) x).recOn (C := fun (x : Multiset α) ↦ Cycle α)
    (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) [])
    (fun (x : α) (x_1 : Multiset α) (l : Cycle α) ↦ if (f : (a : α) → α) x = x then l else (↑(f.toList x) : Cycle α))
    sorry =
  (↑(f.toList x) : Cycle α)
Tactic: rw [toCycle, key]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ (f.toCycle hf).Nodup
have obtain : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (f.toCycle hf).Nodup
Tactic: obtain ⟨x, hx, -⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ (f.toCycle hf).Nontrivial
have obtain : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x), (f.toCycle hf).Nontrivial
Tactic: obtain ⟨x, hx, -⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf ↔ (f : (a : α) → α) x ≠ x
have mp : x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
mp : x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
⊢ x ∈ f.toCycle hf ↔ (f : (a : α) → α) x ≠ x
have mpr : (f : (a : α) → α) x ≠ x → x ∈ f.toCycle hf
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
⊢ x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
have mp : ∀ (l : α) (hl : f.toCycle hf = (↑(f.toList l) : Cycle α)), x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
Tactic: have ⟨l, hl⟩ := exists_toCycle_toList f hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
⊢ x ∈ f.toCycle hf → (f : (a : α) → α) x ≠ x
have mp : x ∈ f.toList l → ¬(f : (a : α) → α) x = x
Tactic: simp only [hl, Cycle.mem_coe_iff, ne_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
⊢ ¬(f : (a : α) → α) x = x
have h1 : f.SameCycle l x
Tactic: have ⟨h1, h2⟩ := mem_toList_iff.mp h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
h : x ∈ f.toList l
h1 : f.SameCycle l x
⊢ ¬(f : (a : α) → α) x = x
have h2 : l ∈ f.support
Tactic: have ⟨h1, h2⟩ := mem_toList_iff.mp h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
⊢ x ∈ f.toCycle hf
have mpr : ∃ m < (f.cycleOf x).support.card, x = (f ^ m : (a : α) → α) x
Tactic: simp only [toCycle_eq_toList f hf x h, Cycle.mem_coe_iff, toList, mem_iterate, iterate_eq_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
h : (f : (a : α) → α) x ≠ x
⊢ ∃ m < (f.cycleOf x).support.card, x = (f ^ m : (a : α) → α) x
have h₁ : 0 < (f.cycleOf x).support.card ∧ x = (HPow.hPow (β := ℕ) f 0 : (a : α) → α) x
Tactic: use 0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
⊢ (f.toCycle hf).next ⋯ x hx = (f : (a : α) → α) x
have have : ∀ (l : α) (hl : f.toCycle hf = (↑(f.toList l) : Cycle α)), (f.toCycle hf).next sorry x hx = (f : (a : α) → α) x
Tactic: have ⟨l, hl⟩ := exists_toCycle_toList f hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
x : α
f : Perm α
hf : f.IsCycle
hx : x ∈ f.toCycle hf
l : α
hl : f.toCycle hf = (↑(f.toList l) : Cycle α)
⊢ (f.toCycle hf).next ⋯ x hx = (f : (a : α) → α) x
have simp : ∀ (hx_1 : x ∈ f.toList l), (↑(f.toList l) : Cycle α).next sorry x sorry = (f : (a : α) → α) x
Tactic: simp only [hl, Cycle.mem_coe_iff] at ⊢ hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
f : { f : Perm α // f.IsCycle }
⊢ (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
        Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        f) =
    f
have obtain : ∀ (x : α) (hx : ((↑f : Perm α) : (a : α) → α) x ≠ x),
  (fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
        Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm sorry) sorry)
      ((fun (f : { f : Perm α // f.IsCycle }) ↦
          (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle sorry) sorry :
            { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
        f) =
    f
Tactic: obtain ⟨x, hx, -⟩ := id f.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }
⊢ (fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        s) =
    s
have mk : ∀ (val : Cycle α) (s : List α) (hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s))
  (ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
  Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle sorry) sorry :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm sorry) sorry)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) sorry)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) sorry)
Tactic: rcases s with ⟨⟨s⟩, hn, ht⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)
have mk : ∀ (x : α) (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x),
  Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle sorry) sorry :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm sorry) sorry)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) sorry)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) sorry)
Tactic: obtain ⟨x, -, -, hx, -⟩ := id ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)
have hl : 2 ≤ s.length
Tactic: have hl : 2 ≤ s.length := by simpa using Cycle.length_nontrivial ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) x
hl : 2 ≤ s.length
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    ((fun (f : { f : Perm α // f.IsCycle }) ↦
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) ((↑f : Perm α).toCycle ⋯) ⋯ :
          { s : Cycle α // s.Nodup ∧ s.Nontrivial }))
      ((fun (s : { s : Cycle α // s.Nodup ∧ s.Nontrivial }) ↦
          Subtype.mk (p := fun (f : Perm α) ↦ f.IsCycle) ((↑s : Cycle α).formPerm ⋯) ⋯)
        (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
          (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)))
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial)
      (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯)
have mk : ∀ (hn_1 : s.Nodup) (hx : x ∈ s),
  Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle sorry) sorry)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) sorry)
Tactic: simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff,
      Cycle.formPerm_coe] at hn hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ Eq (α := { s : Cycle α // s.Nodup ∧ s.Nontrivial })
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯)
    (Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯)
have mk : (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle sorry) sorry) : Cycle α) =
  (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) sorry) : Cycle α)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (s.formPerm.toCycle ⋯) ⋯) : Cycle α) =
    (↑(Subtype.mk (p := fun (s : Cycle α) ↦ s.Nodup ∧ s.Nontrivial) (↑s : Cycle α) ⋯) : Cycle α)
have mk : s.formPerm.toCycle sorry = (↑s : Cycle α)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ s.formPerm.toCycle ⋯ = (↑s : Cycle α)
have mk : (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)
Tactic: rw [toCycle_eq_toList _ _ x]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)
⊢ s.formPerm.toCycle ⋯ = (↑s : Cycle α)
have mk₁ : (s.formPerm : (a : α) → α) x ≠ x
Tactic: rw [toCycle_eq_toList _ _ x]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (↑(s.formPerm.toList x) : Cycle α) = (↑s : Cycle α)
have mk : (IsRotated.setoid α : List α → List α → Prop) (s.formPerm.toList x) s
Tactic: refine Quotient.sound' ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
⊢ (s.formPerm : (a : α) → α) x ≠ x
have mk : x ∈ s.toFinset
Tactic: rw [← mem_support, support_formPerm_of_nodup _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x_1 : α
val : Cycle α
s : List α
hn_1 : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
ht : Cycle.Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
x : α
hl : 2 ≤ s.length
hn : s.Nodup
hx : x ∈ s
mk : x ∈ s.toFinset
⊢ (s.formPerm : (a : α) → α) x ≠ x
have mk₁ : ∀ (x : α), s ≠ [x]
Tactic: rw [← mem_support, support_formPerm_of_nodup _ hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
have intro : ∀ (val : Fintype α), ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
have intro : ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x) (hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y),
  ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
Tactic: obtain ⟨x, hx, hy⟩ := id hf
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
x : α
hx : (f : (a : α) → α) x ≠ x
hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
have intro : (↑(f.toList x) : Cycle α).formPerm sorry = f
Tactic: refine ⟨f.toList x, ⟨nodup_toList f x, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
f : Perm α
hf : f.IsCycle
val : Fintype α
x : α
hx : (f : (a : α) → α) x ≠ x
hy : ∀ ⦃y : α⦄, (f : (a : α) → α) y ≠ y → f.SameCycle x y
intro : (↑(f.toList x) : Cycle α).formPerm ⋯ = f
⊢ ∃! s : Cycle α, ∃ (h : s.Nodup), s.formPerm h = f
have intro₁ : ∀ (y : Cycle α), (fun (s : Cycle α) ↦ ∃ (h : s.Nodup), s.formPerm h = f) y → y = (↑(f.toList x) : Cycle α)
Tactic: refine ⟨f.toList x, ⟨nodup_toList f x, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l =
    (↑((Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).toList x) : Cycle α)
have intro : l ~r l.formPerm.toList x
Tactic: simp only [Cycle.mk_eq_coe, Cycle.coe_eq_coe, Cycle.formPerm_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ l ~r l.formPerm.toList x
have intro : 2 ≤ l.length
Tactic: refine (toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
intro : 2 ≤ l.length
⊢ l ~r l.formPerm.toList x
have intro₁ : x ∈ l
Tactic: refine (toList_formPerm_isRotated_self _ ?_ hn _ ?_).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hx : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x ≠ x
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
⊢ 2 ≤ l.length
have intro : ∀ (hx : l.length < 2),
  (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x = x
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Finite α
inst_1 : DecidableEq α
val : Fintype α
x : α
y : Cycle α
l : List α
hn : Cycle.Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l)
hf : (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).IsCycle
hy :
  ∀ ⦃y : α⦄,
    (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) y ≠ y →
      (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn).SameCycle x y
hx : l.length < 2
⊢ (Cycle.formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) l) hn : (a : α) → α) x = x
have intro : l.formPerm = 1
Tactic: suffices formPerm l = 1 by simp [this]