awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
⊢ (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
have mp : (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
mp :
  (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) → ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
⊢ (∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x) ↔ ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
have mpr : (∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False) → ∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ (x : α), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
x : α
hx : x ∈ l
hx' : x ∈ l'
⊢ False
have h₁ : (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: specialize h x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
x : α
hx : x ∈ l
hx' : x ∈ l'
h : (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ False
have h₁ : l.length ≤ 1 ∨ l'.length ≤ 1
Tactic: rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have pos : ∀ (hx : x ∈ l), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: by_cases hx : x ∈ l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
pos : ∀ (hx : x ∈ l), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have neg : ∀ (hx : x ∉ l), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: by_cases hx : x ∈ l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: by_cases hx' : x ∈ l'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have neg : ∀ (hx' : x ∉ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: by_cases hx' : x ∈ l'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: on_goal 1 => by_cases hx' : x ∈ l'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
pos : ∀ (hx' : x ∈ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have neg : ∀ (hx' : x ∉ l'), (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
Tactic: on_goal 1 => by_cases hx' : x ∈ l'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have this : (l'.formPerm : (a : α) → α) x = x
Tactic: have := List.formPerm_apply_of_notMem ‹_›
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∈ l
hx' : x ∉ l'
this : (l'.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have neg : ¬(l.formPerm : (a : α) → α) x = x → (l'.formPerm : (a : α) → α) x = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have this : (l.formPerm : (a : α) → α) x = x
Tactic: have := List.formPerm_apply_of_notMem ‹_›
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
hn : 2 ≤ l.length
hn' : 2 ≤ l'.length
h : ∀ ⦃a : α⦄, a ∈ l → a ∈ l' → False
x : α
hx : x ∉ l
this : (l.formPerm : (a : α) → α) x = x
⊢ (l.formPerm : (a : α) → α) x = x ∨ (l'.formPerm : (a : α) → α) x = x
have neg : ¬(l.formPerm : (a : α) → α) x = x → (l'.formPerm : (a : α) → α) x = x
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ l.formPerm.IsCycle
have nil : ∀ (hl : Nodup.{u_1} (α := α) []) (hn : 2 ≤ length.{u_1} (α := α) []), IsCycle.{u_1} (α := α) (formPerm [])
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
nil : ∀ (hl : Nodup.{u_1} (α := α) []) (hn : 2 ≤ length.{u_1} (α := α) []), IsCycle.{u_1} (α := α) (formPerm [])
⊢ l.formPerm.IsCycle
have cons : ∀ (x : α) (l : List α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ (x :: y :: l).formPerm.IsCycle
have h : ((x :: y :: l).formPerm : (a : α) → α) x ≠ x ∧
  ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
Tactic: use x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
⊢ ((x :: y :: l).formPerm : (a : α) → α) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
have h : ((x :: y :: l).formPerm : (a : α) → α) x ≠ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
h : ((x :: y :: l).formPerm : (a : α) → α) x ≠ x
⊢ ((x :: y :: l).formPerm : (a : α) → α) x ≠ x ∧
    ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
have h₁ : ∀ ⦃y_1 : α⦄, ((x :: y :: l).formPerm : (a : α) → α) y_1 ≠ y_1 → (x :: y :: l).formPerm.SameCycle x y_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : ((x :: y :: l).formPerm : (a : α) → α) w ≠ w
⊢ (x :: y :: l).formPerm.SameCycle x w
have this : w ∈ x :: y :: l
Tactic: have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
w : α
hw : ((x :: y :: l).formPerm : (a : α) → α) w ≠ w
this : w ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x w
have h : ∀ (k : ℕ) (hk : k < (x :: y :: l).length)
  (hw :
    ((x :: y :: l).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk) ≠
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)
  (this : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk ∈ x :: y :: l),
  (x :: y :: l).formPerm.SameCycle x (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)
Tactic: obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
Cleared hypotheses: w, hw, this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
y : α
l : List α
tail_ih : ∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle
x : α
hl : (x :: y :: l).Nodup
hn : 2 ≤ (x :: y :: l).length
k : ℕ
hk : k < (x :: y :: l).length
hw :
  ((x :: y :: l).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk) ≠
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk
this : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk ∈ x :: y :: l
⊢ (x :: y :: l).formPerm.SameCycle x (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk)
have h : (HPow.hPow (β := ℤ) (x :: y :: l).formPerm (↑k : ℤ) : (a : α) → α) x =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) k hk
Tactic: use k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
⊢ (x :: l).formPerm.IsCycle
have cons : ∀ (x : α) (hl : [x].Nodup) (hn : 2 ≤ [x].length), [x].formPerm.IsCycle
Tactic: induction l generalizing x with
  | nil => norm_num at hn
  | cons y l =>
    use x
    constructor
    · rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]
    · intro w hw
      have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
      obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
      use k
      simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]
Cleared hypotheses: x, l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : α
l : List α
hl : (x :: l).Nodup
hn : 2 ≤ (x :: l).length
cons : ∀ (x : α) (hl : [x].Nodup) (hn : 2 ≤ [x].length), [x].formPerm.IsCycle
⊢ (x :: l).formPerm.IsCycle
have cons₁ : ∀ (y : α) (l : List α),
  (∀ (x : α) (hl : (x :: l).Nodup) (hn : 2 ≤ (x :: l).length), (x :: l).formPerm.IsCycle) →
    ∀ (x : α) (hl : (x :: y :: l).Nodup) (hn : 2 ≤ (x :: y :: l).length), (x :: y :: l).formPerm.IsCycle
Tactic: induction l generalizing x with
  | nil => norm_num at hn
  | cons y l =>
    use x
    constructor
    · rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]
    · intro w hw
      have : w ∈ x::y::l := mem_of_formPerm_apply_ne hw
      obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
      use k
      simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]
Cleared hypotheses: x, l, hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
x : { x : α // x ∈ l }
⊢ 2 ≤ l.attach.length
have rwa : ∀ (hn : 2 ≤ l.attach.length) (x : { x : α // x ∈ l }), 2 ≤ l.attach.length
Tactic: rwa [← length_attach] at hn
Cleared hypotheses: hn, x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn_1 : 2 ≤ l.length
x : { x : α // x ∈ l }
hn : 2 ≤ l.attach.length
⊢ l.attach.Nodup
have rwa : ∀ (hl : l.attach.Nodup) (hn : 2 ≤ l.length) (x : { x : α // x ∈ l }) (hn : 2 ≤ l.attach.length), l.attach.Nodup
Tactic: rwa [← nodup_attach] at hl
Cleared hypotheses: hl, hn_1, x, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.length
⊢ l.attach.formPerm.cycleType = {l.length}
have hn₁ : 2 ≤ l.attach.length
Tactic: rw [← length_attach] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}
have hl₁ : l.attach.Nodup
Tactic: rw [← nodup_attach] at hl
Cleared hypotheses: hl, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ l.attach.formPerm.cycleType = {l.length}
have rw : (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
Tactic: rw [cycleType_eq [l.attach.formPerm]]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
⊢ l.attach.formPerm.cycleType = {l.length}
have h0 : [l.attach.formPerm].prod = l.attach.formPerm
Tactic: rw [cycleType_eq [l.attach.formPerm]]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
h0 : [l.attach.formPerm].prod = l.attach.formPerm
⊢ l.attach.formPerm.cycleType = {l.length}
have h1 : ∀ σ ∈ [l.attach.formPerm], σ.IsCycle
Tactic: rw [cycleType_eq [l.attach.formPerm]]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
h0 : [l.attach.formPerm].prod = l.attach.formPerm
h1 : ∀ σ ∈ [l.attach.formPerm], σ.IsCycle
⊢ l.attach.formPerm.cycleType = {l.length}
have h2 : Pairwise Perm.Disjoint [l.attach.formPerm]
Tactic: rw [cycleType_eq [l.attach.formPerm]]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ (↑(map (Finset.card ∘ support) [l.attach.formPerm]) : Multiset ℕ) = {l.length}
have simp : (↑[l.attach.formPerm.support.card] : Multiset ℕ) = {l.length}
Tactic: simp only [map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
⊢ (↑[l.attach.formPerm.support.card] : Multiset ℕ) = {l.length}
have rw : (↑[l.attach.length] : Multiset ℕ) = {l.length}
Tactic: rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.attach.Nodup
hn : 2 ≤ l.attach.length
rw : (↑[l.attach.length] : Multiset ℕ) = {l.length}
⊢ (↑[l.attach.formPerm.support.card] : Multiset ℕ) = {l.length}
have rw₁ : ∀ (x : { x : α // x ∈ l }), l.attach ≠ [x]
Tactic: rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm : (a : α) → α) x = l.next x hx
have obtain : ∀ (k : ℕ) (hk : k < l.length) (hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l),
  (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
Tactic: obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
have rw : (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) sorry
Tactic: rw [next_getElem _ hl, formPerm_apply_getElem _ hl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk ∈ l
rw :
  (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) ⋯
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) =
    l.next (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l k hk) hx
have rw₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) sorry =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l ((k + 1) % l.length) sorry
Tactic: rw [next_getElem _ hl, formPerm_apply_getElem _ hl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ HEq.{u_1 + 1} (α := Nodup ⟦l₁⟧ → Equiv.Perm α) fun (x : Nodup ⟦l₁⟧) ↦ l₁.formPerm (β := Nodup ⟦l₂⟧ → Equiv.Perm α)
    fun (x : Nodup ⟦l₂⟧) ↦ l₂.formPerm
have hα : Nodup ⟦l₁⟧ = Nodup ⟦l₂⟧
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
hα : Nodup ⟦l₁⟧ = Nodup ⟦l₂⟧
⊢ HEq.{u_1 + 1} (α := Nodup ⟦l₁⟧ → Equiv.Perm α) fun (x : Nodup ⟦l₁⟧) ↦ l₁.formPerm (β := Nodup ⟦l₂⟧ → Equiv.Perm α)
    fun (x : Nodup ⟦l₂⟧) ↦ l₂.formPerm
have h₁ : ∀ (a : Nodup ⟦l₁⟧) (a' : Nodup ⟦l₂⟧), a ≍ a' → l₁.formPerm ≍ l₂.formPerm
Tactic: apply Function.hfunext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 s : Cycle α
l₁ l₂ : List α
h : l₁ ~r l₂
⊢ Nodup ⟦l₁⟧ = Nodup ⟦l₂⟧
have hα : Nodup ⟦l₁⟧ ↔ Nodup ⟦l₂⟧
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Subsingleton
⊢ s.formPerm ⋯ = 1
have mk : ∀ (s : List α) (h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
  formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) sorry = 1
Tactic: obtain ⟨s⟩ := s
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) ⋯ = 1
have mk : s.formPerm = 1
Tactic: simp only [formPerm_coe, mk_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
⊢ s.formPerm = 1
have h₁ : s.length ≤ 1
Tactic: simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : s.length ≤ 1
⊢ s.formPerm = 1
have mk : ∀ (h : List.length.{u_1} (α := α) [] ≤ 1), Eq.{u_1 + 1} (α := Equiv.Perm α) (List.formPerm []) 1
Tactic: obtain - | ⟨hd, tl⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s_1 : Cycle α
s : List α
h : s.length ≤ 1
mk : ∀ (h : List.length.{u_1} (α := α) [] ≤ 1), Eq.{u_1 + 1} (α := Equiv.Perm α) (List.formPerm []) 1
⊢ s.formPerm = 1
have mk₁ : ∀ (hd : α) (tl : List α) (h : (hd :: tl).length ≤ 1), (hd :: tl).formPerm = 1
Tactic: obtain - | ⟨hd, tl⟩ := s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ (hd :: tl).formPerm = 1
have h₁ : tl = []
Tactic: simp only [length_eq_zero_iff, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).IsCycle
have h₁ : ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
  (hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)),
  (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h).IsCycle
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, h, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).support = s.toFinset
have mk : ∀ (s : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s))
  (hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)),
  (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s) h).support =
    toFinset (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) s)
Tactic: obtain ⟨s⟩ := s
Cleared hypotheses: h, hn