internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
⊢ ∀ (a : ℤ), subtypePermOfSupport c ^ a = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ a = subtypePerm k hc'
Tactic:
intro n
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePermOfSupport c ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePermOfSupport c ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Tactic:
unfold subtypePermOfSupport
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePerm g ⋯ ^ n = subtypePerm k hc'
Tactic:
rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]
Proof state after:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePermOfSupport c ^ n = subtypePerm k hc'
Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_iff
Proof state before:
case h.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ cycleFactorsFinset g
hc' : ∀ (x : α), x ∈ support c ↔ k x ∈ support c
n : ℤ
⊢ subtypePerm c ⋯ ^ n = subtypePerm k hc' ↔ subtypePermOfSupport c ^ n = subtypePerm k hc'
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_mod_card_support_cycleOf_self_apply
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
by_cases hx : f x = x
Proof state after:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x

case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : ¬f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Theorem: Equiv.Perm.zpow_mod_card_support_cycleOf_self_apply
Proof state before:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
rw [Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self hx,
  Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self hx]
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_mod_card_support_cycleOf_self_apply
Proof state before:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : ¬f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
rw [← f.cycleOf_zpow_apply_self, ← f.cycleOf_zpow_apply_self,
  ← (f.isCycle_cycleOf hx).orderOf, zpow_mod_orderOf]
Proof state after:
no goals
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n) x = x ↔ n % ↑(support g).card = 0
Tactic:
let q := n / g.support.card
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
⊢ (g ^ n) x = x ↔ n % ↑(support g).card = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
⊢ (g ^ n) x = x ↔ n % ↑(support g).card = 0
Tactic:
let r := n % g.support.card
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ (g ^ n) x = x ↔ n % ↑(support g).card = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ (g ^ n) x = x ↔ n % ↑(support g).card = 0
Tactic:
change _ ↔ r = 0
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ (g ^ n) x = x ↔ r = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ (g ^ n) x = x ↔ r = 0
Tactic:
have div_euc : r + g.support.card * q = n ∧ 0 ≤ r ∧ r < g.support.card := by
  rw [← Int.ediv_emod_unique _]
  constructor; rfl; rfl
  simp only [Int.coe_nat_pos]
  apply lt_of_lt_of_le _ (Equiv.Perm.IsCycle.two_le_card_support hg); norm_num
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(support g).card * q = n ∧ 0 ≤ r ∧ r < ↑(support g).card
⊢ (g ^ n) x = x ↔ r = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(support g).card * q = n ∧ 0 ≤ r ∧ r < ↑(support g).card
⊢ (g ^ n) x = x ↔ r = 0
Tactic:
simp only [← hg.orderOf] at div_euc
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(orderOf g) * q = n ∧ 0 ≤ r ∧ r < ↑(orderOf g)
⊢ (g ^ n) x = x ↔ r = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(orderOf g) * q = n ∧ 0 ≤ r ∧ r < ↑(orderOf g)
⊢ (g ^ n) x = x ↔ r = 0
Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le div_euc.2.1
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(orderOf g) * q = n ∧ 0 ≤ r ∧ r < ↑(orderOf g)
m : ℕ
hm : r = ↑m
⊢ (g ^ n) x = x ↔ r = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
div_euc : r + ↑(orderOf g) * q = n ∧ 0 ≤ r ∧ r < ↑(orderOf g)
m : ℕ
hm : r = ↑m
⊢ (g ^ n) x = x ↔ r = 0
Tactic:
simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and_iff] at div_euc
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ r = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ r = 0
Tactic:
simp only [hm, Nat.cast_eq_zero]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ m = 0
Tactic:
rw [← div_euc.1, zpow_add g, zpow_mul]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ ↑m * (g ^ ↑(orderOf g)) ^ q) x = x ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ ↑m * (g ^ ↑(orderOf g)) ^ q) x = x ↔ m = 0
Tactic:
simp only [zpow_natCast, coe_mul, Function.comp_apply]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) (((g ^ orderOf g) ^ q) x) = x ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) (((g ^ orderOf g) ^ q) x) = x ↔ m = 0
Tactic:
simp only [pow_orderOf_eq_one, one_zpow, coe_one, id_eq]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
⊢ (g ^ m) x = x ↔ m = 0
Tactic:
simp only [this]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
⊢ g ^ m = 1 ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
⊢ g ^ m = 1 ↔ m = 0
Tactic:
cases' dec_em (m = 0) with hm0 hm0'
Proof state after:
case intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : m = 0
⊢ g ^ m = 1 ↔ m = 0

case intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0' : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ r + ↑(support g).card * q = n ∧ 0 ≤ r ∧ r < ↑(support g).card
Tactic:
rw [← Int.ediv_emod_unique _]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n / ↑(support g).card = q ∧ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n / ↑(support g).card = q ∧ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n / ↑(support g).card = q

case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n / ↑(support g).card = q

case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Tactic:
rfl
Proof state after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ n % ↑(support g).card = r

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Tactic:
rfl
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < ↑(support g).card
Tactic:
simp only [Int.coe_nat_pos]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < (support g).card
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < (support g).card
Tactic:
apply lt_of_lt_of_le _ (Equiv.Perm.IsCycle.two_le_card_support hg)
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < 2
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x ↔ g ^ m = 1
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x → g ^ m = 1

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ m) x = x → g ^ m = 1
Tactic:
intro hgm
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : (g ^ m) x = x
⊢ g ^ m = 1
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : (g ^ m) x = x
⊢ g ^ m = 1
Tactic:
simp [Equiv.Perm.IsCycle.pow_eq_one_iff hg]
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : (g ^ m) x = x
⊢ ∃ x, ¬g x = x ∧ (g ^ m) x = x
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : (g ^ m) x = x
⊢ ∃ x, ¬g x = x ∧ (g ^ m) x = x
Tactic:
use x
Proof state after:
no goals
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x
Tactic:
intro hgm
Proof state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ (g ^ m) x = x
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ (g ^ m) x = x
Tactic:
rw [hgm]
Proof state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ 1 x = x
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ 1 x = x
Tactic:
simp only [Equiv.Perm.coe_one, id.def]
Proof state after:
no goals
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : m = 0
⊢ g ^ m = 1 ↔ m = 0
Tactic:
simp only [hm0, pow_zero, Nat.cast_zero]
Proof state after:
no goals
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0' : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0
Tactic:
simp only [Nat.cast_eq_zero, hm0', iff_false]
Proof state after:
case intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0' : ¬m = 0
⊢ ¬g ^ m = 1
Theorem: Equiv.Perm.cycle_zpow_mem_support_iff
Proof state before:
case intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hg : IsCycle g
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(support g).card
r : ℤ := n % ↑(support g).card
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0' : ¬m = 0
⊢ ¬g ^ m = 1
Tactic:
exact pow_ne_one_of_lt_orderOf' hm0' div_euc.2
Proof state after:
no goals
Theorem: Equiv.Perm.zpow_eq_zpow_on_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ m % ↑(support (cycleOf g x)).card = n % ↑(support (cycleOf g x)).card
Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0