Theorem: Equiv.Perm.cycle_zpow_mem_support_iff (Jordan/ConjClassCount.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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]
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

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]
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

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]
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

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]
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

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]
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

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'
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

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 _]
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

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
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

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
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

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
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

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]
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

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)
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

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
State after:
no goals

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
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

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
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

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]
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

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
State after:
no goals

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
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

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]
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

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]
State after:
no goals

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]
State after:
no goals

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]
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

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
State after:
no goals