awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s_1 : Cycle α
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)
have mk : ∀ (x : α), s ≠ [x]
Tactic: refine support_formPerm_of_nodup s h ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∉ s
⊢ (s.formPerm h : (a : α) → α) x = x
have h₁ : ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
  (hx : x ∉ Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a),
  (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x = x
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, h, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∈ s
⊢ (s.formPerm h : (a : α) → α) x = s.next h x hx
have h₁ : ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a))
  (hx : Membership.mem (γ := Cycle α) (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) x),
  (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h : (a : α) → α) x =
    next (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h x hx
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, h, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Cycle α
h : s.Nodup
⊢ s.reverse.formPerm ⋯ = (s.formPerm h)⁻¹
have h₁ : ∀ (a : List α) (h : Nodup (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)),
  (reverse (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a)).formPerm sorry =
    (formPerm (Quot.mk (⇑(IsRotated.setoid α) : List α → List α → Prop) a) h)⁻¹
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s s' : Cycle α
hs : s.Nodup
hs' : s'.Nodup
⊢ s.formPerm hs = s'.formPerm hs' ↔ s = s' ∨ s.length ≤ 1 ∧ s'.length ≤ 1
have h : ∀ (a₁ a₂ : List α) {hs : Nodup (Quotient.mk'' a₁)} {hs' : Nodup (Quotient.mk'' a₂)},
  formPerm (Quotient.mk'' a₁) hs = formPerm (Quotient.mk'' a₂) hs' ↔
    Eq (α := Cycle α) (Quotient.mk'' a₁) (Quotient.mk'' a₂) ∨
      length (Quotient.mk'' a₁) ≤ 1 ∧ length (Quotient.mk'' a₂) ≤ 1
Tactic: induction s, s' using Quotient.inductionOn₂'
Cleared hypotheses: s, s', hs, hs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
⊢ y ∈ p.toList x ↔ p.SameCycle x y ∧ x ∈ p.support
have simp : (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support
Tactic: simp only [toList, mem_iterate, iterate_eq_pow, eq_comm (a := y)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support
have mp : (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) → p.SameCycle x y ∧ x ∈ p.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x y : α
mp : (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) → p.SameCycle x y ∧ x ∈ p.support
⊢ (∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y) ↔ p.SameCycle x y ∧ x ∈ p.support
have mpr : p.SameCycle x y ∧ x ∈ p.support → ∃ m < (p.cycleOf x).support.card, (p ^ m : (a : α) → α) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ p.SameCycle x ((p ^ n : (a : α) → α) x) ∧ x ∈ p.support
have mp : x ∈ p.support
Tactic: refine ⟨⟨n, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : n < (p.cycleOf x).support.card
⊢ x ∈ p.support
have mp : ∀ (hx : x ∉ p.support), (p.cycleOf x).support.card ≤ n
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
n : ℕ
hx : x ∉ p.support
⊢ (p.cycleOf x).support.card ≤ n
have hx₁ : (p.cycleOf x).support = ∅
Tactic: rw [← support_cycleOf_eq_nil_iff] at 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 : α
⊢ (p.toList x).Nodup
have pos : ∀ (hx : (p : (a : α) → α) x = x), (p.toList x).Nodup
Tactic: by_cases hx : p x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
pos : ∀ (hx : (p : (a : α) → α) x = x), (p.toList x).Nodup
⊢ (p.toList x).Nodup
have neg : ∀ (hx : ¬(p : (a : α) → α) x = x), (p.toList x).Nodup
Tactic: by_cases hx : p x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : (p : (a : α) → α) x = x
⊢ (p.toList x).Nodup
have hx₁ : p.toList x = []
Tactic: rw [← notMem_support, ← toList_eq_nil_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
⊢ (p.toList x).Nodup
have hc : (p.cycleOf x).IsCycle
Tactic: have hc : IsCycle (cycleOf p x) := isCycle_cycleOf p hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
⊢ (p.toList x).Nodup
have neg : Function.Injective.{1, u_1 + 1} (β := α) fun (i : Fin (p.toList x).length) ↦
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry
Tactic: rw [nodup_iff_injective_getElem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
⊢ ∀ ⦃a₂ : Fin (p.toList x).length⦄,
    Eq.{u_1 + 1} (α := α)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          ⟨n, hn⟩)
        ((fun (i : Fin (p.toList x).length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
          a₂) →
      (⟨n, hn⟩ : Fin (p.toList x).length) = a₂
have neg : ∀ (m : ℕ) (hm : m < (p.toList x).length),
  Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨n, hn⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨m, hm⟩) →
    (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
Tactic: ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn : n < (p.toList x).length
m : ℕ
hm : m < (p.toList x).length
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm⟩) →
    (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
have neg : ∀ (hn_1 : n < orderOf (p.cycleOf x)) (m : ℕ) (hm : m < (p.toList x).length) (hm_1 : m < orderOf (p.cycleOf x)),
  Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨n, hn⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨m, hm⟩) →
    (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
Tactic: rw [length_toList, ← hc.orderOf] at hm hn
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : ¬(p : (a : α) → α) x = x
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn_1⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm_1⟩) →
    (⟨n, hn_1⟩ : Fin (p.toList x).length) = ⟨m, hm_1⟩
have neg : ∀ (hx : x ∈ (p.cycleOf x).support) (hc : (p.cycleOf x).IsCycle) (n : ℕ) (hn : n < (p.toList x).length)
  (hn_2 : n < orderOf (p.cycleOf x)) (m : ℕ) (hm : m < (p.toList x).length) (hm_2 : m < orderOf (p.cycleOf x)),
  Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨n, hn⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) sorry)
        ⟨m, hm⟩) →
    (⟨n, hn⟩ : Fin (p.toList x).length) = ⟨m, hm⟩
Tactic: rw [← cycleOf_apply_self, ← Ne, ← mem_support] at hx
Cleared hypotheses: hx, hc, n, hn_1, hn, m, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ Eq.{u_1 + 1} (α := α)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨n, hn_1⟩)
      ((fun (i : Fin (p.toList x).length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) (↑i : ℕ) ⋯)
        ⟨m, hm_1⟩) →
    (⟨n, hn_1⟩ : Fin (p.toList x).length) = ⟨m, hm_1⟩
have neg : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) n sorry =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) m sorry →
  n = m
Tactic: simp only [Fin.mk.injEq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) n ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (p.toList x) m ⋯ →
    n = m
have neg : Eq (α := α) ((p.cycleOf x ^ n : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n = m
Tactic: rw [getElem_toList, getElem_toList, ← cycleOf_pow_apply_self p x n, ←
    cycleOf_pow_apply_self p x m]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((p.cycleOf x ^ n : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n = m
have neg : ∀ (hn : 0 < (p.toList x).length) (hn : 0 < orderOf (p.cycleOf x)),
  Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → 0 = m
Tactic: rcases n with - | n
Cleared hypotheses: n, hn_1, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n < (p.toList x).length
hn : n < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
neg :
  ∀ (hn : 0 < (p.toList x).length) (hn : 0 < orderOf (p.cycleOf x)),
    Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) →
      0 = m
⊢ Eq (α := α) ((p.cycleOf x ^ n : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n = m
have neg₁ : ∀ (n : ℕ) (hn : n + 1 < (p.toList x).length) (hn : n + 1 < orderOf (p.cycleOf x)),
  Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n + 1 = m
Tactic: rcases n with - | n
Cleared hypotheses: n, hn_1, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → 0 = m
have neg : ∀ (hm : 0 < (p.toList x).length) (hm : 0 < orderOf (p.cycleOf x)),
  Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α)
      ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
    Eq (α := ℕ) 0 0
Tactic: rcases m with - | m
Cleared hypotheses: m, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
neg :
  ∀ (hm : 0 < (p.toList x).length) (hm : 0 < orderOf (p.cycleOf x)),
    Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α)
        ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
      Eq (α := ℕ) 0 0
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → 0 = m
have neg₁ : ∀ (m : ℕ) (hm : m + 1 < (p.toList x).length) (hm : m + 1 < orderOf (p.cycleOf x)),
  Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) →
    0 = m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n + 1 = m
have neg : ∀ (hm : 0 < (p.toList x).length) (hm : 0 < orderOf (p.cycleOf x)),
  Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
    n + 1 = 0
Tactic: rcases m with - | m
Cleared hypotheses: m, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
m : ℕ
hm_1 : m < (p.toList x).length
hm : m < orderOf (p.cycleOf x)
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
neg :
  ∀ (hm : 0 < (p.toList x).length) (hm : 0 < orderOf (p.cycleOf x)),
    Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α)
        ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
      n + 1 = 0
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ m : (a : α) → α) x : α) → n + 1 = m
have neg₁ : ∀ (m : ℕ) (hm : m + 1 < (p.toList x).length) (hm : m + 1 < orderOf (p.cycleOf x)),
  Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) →
    n + 1 = m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
hn_1 : 0 < (p.toList x).length
hn : 0 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α) →
    0 = m + 1
have hx₁ : (p ^ m.succ : (a : α) → α) x ≠ x
Tactic: rw [← hc.support_pow_of_pos_of_lt_orderOf m.zero_lt_succ hm, mem_support,
      cycleOf_pow_apply_self] at hx
Cleared hypotheses: hx, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
hm_1 : 0 < (p.toList x).length
hm : 0 < orderOf (p.cycleOf x)
⊢ Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) (p.cycleOf x) 0 : (a : α) → α) x : α) →
    n + 1 = 0
have hx₁ : (p ^ n.succ : (a : α) → α) x ≠ x
Tactic: rw [← hc.support_pow_of_pos_of_lt_orderOf n.zero_lt_succ hn, mem_support,
      cycleOf_pow_apply_self] at hx
Cleared hypotheses: hx, hn_1, hn, hm_1, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
⊢ n + 1 = m + 1
have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
Tactic: have hn' : ¬orderOf (p.cycleOf x) ∣ n.succ := Nat.not_dvd_of_pos_of_lt n.zero_lt_succ hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
⊢ n + 1 = m + 1
have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
Tactic: have hm' : ¬orderOf (p.cycleOf x) ∣ m.succ := Nat.not_dvd_of_pos_of_lt m.zero_lt_succ hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
⊢ n + 1 = m + 1
have hn'₁ : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
Tactic: rw [← hc.support_pow_eq_iff] at hn' hm'
Cleared hypotheses: hn', hm'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
hn'₁ : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
⊢ n + 1 = m + 1
have hm'₁ : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
Tactic: rw [← hc.support_pow_eq_iff] at hn' hm'
Cleared hypotheses: hn', hm'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ n + 1 = m + 1
have neg : p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)
Tactic: rw [← Nat.mod_eq_of_lt hn, ← Nat.mod_eq_of_lt hm, ← pow_inj_mod]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)
have neg : (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x ^ (m + 1)).support
Tactic: refine support_congr ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Cycle.Concrete (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn_1 : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm_1 : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x : α)
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
neg : (p.cycleOf x ^ (n + 1)).support ⊆ (p.cycleOf x ^ (m + 1)).support
⊢ p.cycleOf x ^ (n + 1) = p.cycleOf x ^ (m + 1)
have neg₁ : ∀ x_1 ∈ (p.cycleOf x ^ (m + 1)).support,
  Eq (α := α) ((p.cycleOf x ^ (n + 1) : (a : α) → α) x_1 : α) ((p.cycleOf x ^ (m + 1) : (a : α) → α) x_1 : α)
Tactic: refine support_congr ?_ ?_