awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g

Tactic:
hf.support_congr hg this h

Premises used: Equiv.Perm.IsCycle.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f g : Perm α
x : α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx : Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g

Tactic:
exact hf.support_congr hg this h

Premises used: Equiv.Perm.IsCycle.support_congr
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
rw : (f ^ n).support = f.support ↔ ¬f ^ n = 1
⊢ (f ^ n).support = f.support ↔ ¬orderOf f ∣ n

Tactic:
rw [orderOf_dvd_iff_pow_eq_one]

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
mp : (f ^ n).support = f.support → ¬f ^ n = 1
mpr : ¬f ^ n = 1 → (f ^ n).support = f.support
⊢ (f ^ n).support = f.support ↔ ¬f ^ n = 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
⊢ False

Tactic:
hf.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
mp : f = 1
⊢ False

Tactic:
refine hf.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
mp : f.support = ∅
mp₁ : (f ^ n).support = ∅
mp₂ : Eq.{u_2 + 1} (α := Finset α) (support 1) ∅
mp₃ mp₄ : Eq.{u_2 + 1} (α := Finset α) ∅ ∅
⊢ f = 1

Tactic:
rw [← support_eq_empty_iff, ← h, H, support_one]

Premises used: Equiv.Perm.support_eq_empty_iff, Equiv.Perm.support_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
apply : f.support ≤ (f ^ n).support
⊢ (f ^ n).support = f.support

Tactic:
apply le_antisymm (support_pow_le _ n) _

Premises used: Equiv.Perm.support_pow_le, le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
H : ¬f ^ n = 1
x : α
hx : x ∈ f.support
contrapose : ∀ (H : x ∉ (f ^ n).support), f ^ n = 1
⊢ x ∈ (f ^ n).support

Tactic:
contrapose H
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
H₁ : ∀ (z : α), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
⊢ f ^ n = 1

Tactic:
ext z
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
pos : ∀ (hz : (f : (a : α) → α) z = z), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
neg : ∀ (hz : ¬(f : (a : α) → α) z = z), Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)

Tactic:
by_cases hz : f z = z

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : (f : (a : α) → α) z = z
pos : z = (1 : (a : α) → α) z
pos₁ pos₂ : z = z
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]

Premises used: Equiv.Perm.pow_apply_eq_self_of_apply_eq_self, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬(f : (a : α) → α) z = z
neg :
  ∀ (k : ℕ) (hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α))
    (H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support),
    Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)

Tactic:
obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)

Premises used: Equiv.Perm.IsCycle.exists_pow_eq, Equiv.Perm.mem_support, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬(f : (a : α) → α) z = z
k : ℕ
hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α)
H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support
neg :
  Eq (α := α) ((f ^ k : (a : α) → α) ((f ^ n : (a : α) → α) z : α) : α)
    ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)
⊢ Eq (α := α) ((f ^ n : (a : α) → α) z : α) ((1 : (a : α) → α) z : α)

Tactic:
apply (f ^ k).injective

Premises used: HPow.hPow, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬(f : (a : α) → α) z = z
k : ℕ
hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α)
H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support
neg :
  Eq (α := α) ((f ^ n : (a : α) → α) ((f ^ k : (a : α) → α) z : α) : α)
    ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)
⊢ Eq (α := α) ((f ^ k : (a : α) → α) ((f ^ n : (a : α) → α) z : α) : α)
    ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)

Tactic:
rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]

Premises used: Commute.pow_pow_self, Equiv.Perm.mul_apply, Commute.eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬(f : (a : α) → α) z = z
k : ℕ
hx : Membership.mem (α := α) f.support ((f ^ k : (a : α) → α) z : α)
H : ((f ^ k : (a : α) → α) z : α) ∉ (f ^ n).support
⊢ Eq (α := α) ((f ^ n : (a : α) → α) ((f ^ k : (a : α) → α) z : α) : α)
    ((f ^ k : (a : α) → α) ((1 : (a : α) → α) z : α) : α)

Tactic:
simpa using H
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
α : Type u_2
f : Perm α
inst : DecidableEq α
inst_1 : Fintype α
hf : f.IsCycle
n : ℕ
npos : 0 < n
hn : n < orderOf f
⊢ (f ^ n).support = f.support

Tactic:
hf.support_pow_eq_iff.2 <| Nat.not_dvd_of_pos_of_lt npos hn

Premises used: Iff.mpr, Equiv.Perm.IsCycle.support_pow_eq_iff, Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
intro : (f ^ n).IsCycle → n.Coprime (orderOf f)
intro₁ : n.Coprime (orderOf f) → (f ^ n).IsCycle
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
rw : ¬orderOf f ∣ n
⊢ (f ^ n).support = f.support

Tactic:
rw [hf.support_pow_eq_iff]

Premises used: Equiv.Perm.IsCycle.support_pow_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ False

Tactic:
h.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
refine : f ^ (orderOf f * k) = 1
⊢ False

Tactic:
refine h.ne_one ?_

Premises used: Equiv.Perm.IsCycle.ne_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
k : ℕ
h : (f ^ (orderOf f * k)).IsCycle
⊢ f ^ (orderOf f * k) = 1

Tactic:
simp [pow_mul, pow_orderOf_eq_one]

Premises used: pow_mul, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
⊢ (f ^ n).support = f.support

Tactic:
have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
rw : #(f ^ n).support = orderOf f
rw₁ : #f.support = orderOf f
rw₂ rw₃ : #f.support = #f.support
⊢ orderOf (f ^ n) = orderOf f

Tactic:
rw [h.orderOf, hr, hf.orderOf]

Premises used: Equiv.Perm.IsCycle.orderOf
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ orderOf (f ^ n) = orderOf f

Tactic:
have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ orderOf f = 0 ∨ (orderOf f).gcd n = 1

Tactic:
rw [orderOf_pow, Nat.div_eq_self] at this

Premises used: orderOf_pow, Nat.div_eq_self
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f = 0 ∨ (orderOf f).gcd n = 1
intro : ∀ (h : orderOf f = 0), n.Coprime (orderOf f)
intro₁ : (orderOf f).gcd n = 1 → n.Coprime (orderOf f)
⊢ n.Coprime (orderOf f)

Tactic:
rcases this with h | _
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h_1 : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h : orderOf f = 0
⊢ n.Coprime (orderOf f)

Tactic:
absurd h (orderOf_pos _).ne'

Premises used: LT.lt.ne', absurd, orderOf_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h_1 : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h : orderOf f = 0
⊢ n.Coprime (orderOf f)

Tactic:
exact absurd h (orderOf_pos _).ne'

Premises used: LT.lt.ne', absurd, orderOf_pos
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
h_1 : (orderOf f).gcd n = 1
intro : n.gcd (orderOf f) = 1
intro₁ intro₂ intro₃ intro₄ : (orderOf f).gcd n = 1
⊢ n.Coprime (orderOf f)

Tactic:
rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]

Premises used: Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
intro : ∀ (m : ℕ) (hm : (f ^ n) ^ m = f), (f ^ n).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h

Premises used: exists_pow_eq_self_of_coprime
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
rwa rwa₁ rwa₂ rwa₃ : f.IsCycle
⊢ ((f ^ n) ^ m).IsCycle

Tactic:
rwa [hm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
⊢ ((f ^ n) ^ m).IsCycle

Tactic:
have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
⊢ (f ^ n).IsCycle

Tactic:
hf'.of_pow fun x hx => ?_

Premises used: Equiv.Perm.IsCycle.of_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
intro : ∀ (x : β) (hx : x ∈ (f ^ n).support), x ∈ ((f ^ n) ^ m).support
⊢ (f ^ n).IsCycle

Tactic:
refine hf'.of_pow fun x hx => ?_

Premises used: Equiv.Perm.IsCycle.of_pow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
intro : x ∈ f.support
⊢ x ∈ ((f ^ n) ^ m).support

Tactic:
rw [hm]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support

Tactic:
support_pow_le _ n hx

Premises used: Equiv.Perm.support_pow_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : n.Coprime (orderOf f)
m : ℕ
hm : (f ^ n) ^ m = f
hf' : ((f ^ n) ^ m).IsCycle
x : β
hx : x ∈ (f ^ n).support
⊢ x ∈ f.support

Tactic:
exact support_pow_le _ n hx

Premises used: Equiv.Perm.support_pow_le
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
intro₁ : ∀ (val : Fintype β), (f ^ n).IsCycle → n.Coprime (orderOf f)
intro₂ intro₃ : ∀ (val : Fintype β), n.Coprime (orderOf f) → (f ^ n).IsCycle
⊢ (f ^ n).IsCycle ↔ n.Coprime (orderOf f)

Tactic:
classical
    cases nonempty_fintype β
    constructor
    · intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]
    · intro h
      obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
      have hf' : IsCycle ((f ^ n) ^ m) := by rwa [hm]
      refine hf'.of_pow fun x hx => ?_
      rw [hm]
      exact support_pow_le _ n hx

Premises used: orderOf_pow, nonempty_fintype, Nat.coprime_iff_gcd_eq_one, Nat.div_eq_self, Nat.gcd_comm
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
intro : f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
intro₁ : (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x) → f ^ n = 1
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : f ^ n = 1
intro : ∀ (x : β) (hx : (f : (a : β) → β) x ≠ x), ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : f ^ n = 1
x : β
hx : (f : (a : β) → β) x ≠ x
⊢ (f ^ n : (a : β) → β) x = x

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
h : f ^ n = 1
x : β
hx : (f : (a : β) → β) x ≠ x
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x

Tactic:
exact ⟨x, hx, by simp [h]⟩
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
pos : ∀ (h : (f ^ n).support = f.support), f ^ n = 1
neg : ∀ (h : ¬(f ^ n).support = f.support), f ^ n = 1
⊢ f ^ n = 1

Tactic:
by_cases h : support (f ^ n) = support f

Premises used: Equiv.Perm.support, HPow.hPow
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : (f ^ n).support = f.support
⊢ (f ^ n : (a : β) → β) x ≠ x

Tactic:
rw [← mem_support, ← h, mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : (f ^ n).support = f.support
hx₁ : (f ^ n : (a : β) → β) x ≠ x
⊢ (f ^ n : (a : β) → β) x = x

Tactic:
rw [← mem_support, ← h, mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : (f ^ n).support = f.support
hx₁ : (f ^ n : (a : β) → β) x ≠ x
hx'₁ : (f ^ n : (a : β) → β) x = x
⊢ (f ^ n).support = f.support

Tactic:
rw [← mem_support, ← h, mem_support] at hx

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f ^ n : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : ¬(f ^ n).support = f.support
⊢ orderOf f ∣ n

Tactic:
rw [hf.support_pow_eq_iff, Classical.not_not] at h

Premises used: Classical.not_not, Equiv.Perm.IsCycle.support_pow_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
hx' : (f ^ n : (a : β) → β) x = x
h : orderOf f ∣ n
neg : ∀ (k : ℕ) (hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x), f ^ (orderOf f * k) = 1
⊢ f ^ n = 1

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
val : Fintype β
x : β
hx : (f : (a : β) → β) x ≠ x
k : ℕ
hx' : (f ^ (orderOf f * k) : (a : β) → β) x = x
neg : (f ^ orderOf f) ^ k = 1
neg₁ : HPow.hPow (α := Perm β) 1 k = 1
neg₂ neg₃ : Eq.{u_3 + 1} (α := Perm β) 1 1
⊢ f ^ (orderOf f * k) = 1

Tactic:
rw [pow_mul, pow_orderOf_eq_one, one_pow]

Premises used: one_pow, pow_mul, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
intro : ∀ (val : Fintype β), f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
intro₁ : ∀ (val : Fintype β), f ^ n = 1 → ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x
intro₂ intro₃ : ∀ (val : Fintype β), (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x) → f ^ n = 1
⊢ f ^ n = 1 ↔ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ (f ^ n : (a : β) → β) x = x

Tactic:
classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]

Premises used: one_pow, Classical.not_not, Equiv.Perm.mem_support, id, pow_mul, pow_orderOf_eq_one, nonempty_fintype, rfl
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
x : β
hx : (f : (a : β) → β) x ≠ x
⊢ f ^ n = 1 ↔ (f ^ n : (a : β) → β) x = x

Tactic:
⟨fun h => DFunLike.congr_fun h x, fun h => hf.pow_eq_one_iff.2 ⟨x, hx, h⟩⟩

Premises used: Iff.mpr, DFunLike.congr_fun, Equiv.Perm.IsCycle.pow_eq_one_iff, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ f ^ n = 1 ↔ ∀ (x : β), (f : (a : β) → β) x ≠ x → (f ^ n : (a : β) → β) x = x

Tactic:
⟨fun h _ hx => (hf.pow_eq_one_iff' hx).1 h, fun h =>
    let ⟨_, hx, _⟩ := id hf
    (hf.pow_eq_one_iff' hx).2 (h _ hx)⟩

Premises used: Iff.mpr, Equiv.Perm.IsCycle.pow_eq_one_iff', id, HPow.hPow, _private.0.Equiv.Perm.IsCycle.pow_eq_one_iff''.match_1, Iff.intro, Iff.mp, OfNat.ofNat, Eq
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
intro :
  ∀ (val : Fintype β),
    f ^ a = f ^ b ↔
      ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
intro :
  f ^ a = f ^ b →
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
intro₁ :
  (∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)) →
    f ^ a = f ^ b
⊢ f ^ a = f ^ b ↔
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
h : f ^ a = f ^ b
intro :
  ∀ (x : β) (hx : (f : (a : β) → β) x ≠ x),
    ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Premises used: id
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
h : f ^ a = f ^ b
x : β
hx : (f : (a : β) → β) x ≠ x
⊢ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Cycle.Basic
Goal:
β : Type u_3
inst : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val : Fintype β
h : f ^ a = f ^ b
x : β
hx : (f : (a : β) → β) x ≠ x
⊢ ∃ (x : β), (f : (a : β) → β) x ≠ x ∧ Eq (α := β) ((f ^ a : (a : β) → β) x : β) ((f ^ b : (a : β) → β) x : β)

Tactic:
exact ⟨x, hx, by simp [h]⟩