[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1 ↔ x ^ n = 1
[PROOFSTEP]
rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ (fun x_1 => x ^ n * x_1) 1 = 1 ↔ x ^ n = 1
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ x ^ n * 1 = 1 ↔ x ^ n = 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
h : Injective fun n => x ^ n
⊢ ¬IsOfFinOrder x
[PROOFSTEP]
simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
h : Injective fun n => x ^ n
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬x ^ x_1 = 1
[PROOFSTEP]
intro n hn_pos hnx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = 1
⊢ False
[PROOFSTEP]
rw [← pow_zero x] at hnx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
[PROOFSTEP]
rw [h hnx] at hn_pos
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
x : G
h : Injective fun n => x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False
[PROOFSTEP]
exact irrefl 0 hn_pos
[GOAL]
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Submonoid G
x : { x // x ∈ H }
⊢ IsOfFinOrder x ↔ IsOfFinOrder ↑x
[PROOFSTEP]
rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]
[GOAL]
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Submonoid G
x : { x // x ∈ H }
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, 0 < n ∧ ↑x ^ n = 1
[PROOFSTEP]
norm_cast
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ ↑f x ^ n = 1
[PROOFSTEP]
rcases(isOfFinOrder_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ ↑f x ^ n = 1
[PROOFSTEP]
exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ↑f x ^ n = 1
[PROOFSTEP]
rw [← f.map_pow, hn, f.map_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)
[PROOFSTEP]
rcases(isOfFinOrder_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n✝ m : ℕ
η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)
[PROOFSTEP]
exact fun _ => (isOfFinOrder_iff_pow_eq_one _).mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ x ^ orderOf x = 1
[PROOFSTEP]
refine
  Eq.trans ?_
    (isPeriodicPt_minimalPeriod (x * ·) 1)
      -- porting note: we need a `dsimp` in the middle of the rewrite to do beta reduction
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ x ^ orderOf x = (fun x_1 => x * x_1)^[minimalPeriod (fun x_1 => x * x_1) 1] 1
[PROOFSTEP]
rw [orderOf, mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = (fun x_1 => x ^ minimalPeriod (fun x_2 => x * x_2) 1 * x_1) 1
[PROOFSTEP]
dsimp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
⊢ x ^ minimalPeriod (fun x_1 => x * x_1) 1 = x ^ minimalPeriod (fun x_1 => x * x_1) 1 * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : ¬IsOfFinOrder x
⊢ orderOf x = 0
[PROOFSTEP]
rwa [orderOf, minimalPeriod, dif_neg]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
[PROOFSTEP]
simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ (m : ℕ), m < n → 0 < m → x ^ m ≠ 1
[PROOFSTEP]
simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
⊢ (if h : 1 ∈ periodicPts fun x_1 => x * x_1 then Nat.find h else 0) = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
split_ifs with h1
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ Nat.find h1 = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
classical
rw [find_eq_iff]
simp only [h, true_and]
push_neg
rfl
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ Nat.find h1 = n ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
rw [find_eq_iff]
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ ((n > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n 1) ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
simp only [h, true_and]
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧
      ∀ (n_1 : ℕ), n_1 < n → ¬(n_1 > 0 ∧ IsPeriodicPt (fun x_1 => x * x_1) n_1 1)) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
push_neg
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : 1 ∈ periodicPts fun x_1 => x * x_1
⊢ (IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (n_1 : ℕ), n_1 < n → n_1 > 0 → ¬IsPeriodicPt (fun x_1 => x * x_1) n_1 1) ↔
    IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
rfl
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ 0 = n ↔ IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1
[PROOFSTEP]
rw [iff_false_left h.ne]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
⊢ ¬(IsPeriodicPt (fun x_1 => x * x_1) n 1 ∧ ∀ (m : ℕ), m < n → 0 < m → ¬IsPeriodicPt (fun x_1 => x * x_1) m 1)
[PROOFSTEP]
rintro ⟨h', -⟩
[GOAL]
case neg.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : 0 < n
h1 : ¬1 ∈ periodicPts fun x_1 => x * x_1
h' : IsPeriodicPt (fun x_1 => x * x_1) n 1
⊢ False
[PROOFSTEP]
exact h1 ⟨n, h, h'⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
⊢ 0 < orderOf x ↔ IsOfFinOrder x
[PROOFSTEP]
rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x y✝ : G
a b : A
n m : ℕ
inst✝ : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y
[PROOFSTEP]
rw [← orderOf_pos_iff] at hx ⊢
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x y✝ : G
a b : A
n m : ℕ
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y
[PROOFSTEP]
exact Nat.pos_of_dvd_of_pos h hx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ IsPeriodicPt (fun x_1 => x * x_1) n 1
[PROOFSTEP]
rwa [isPeriodicPt_mul_iff_pow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
⊢ orderOf 1 = 1
[PROOFSTEP]
rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
⊢ orderOf x = 1 ↔ x = 1
[PROOFSTEP]
rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
⊢ x ^ n = x ^ (n % orderOf x + orderOf x * (n / orderOf x))
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ (n % orderOf x)
[PROOFSTEP]
simp [pow_add, pow_mul, pow_orderOf_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1
[PROOFSTEP]
rw [pow_eq_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n✝ m n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x
[PROOFSTEP]
rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
x : G
hn : n < orderOf x
hm : m < orderOf x
eq : x ^ n = x ^ m
⊢ (fun x_1 => x * x_1)^[n] 1 = (fun x_1 => x * x_1)^[m] 1
[PROOFSTEP]
simpa only [mul_left_iterate, mul_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
[PROOFSTEP]
rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]
[GOAL]
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (↑ψ x) ∣ orderOf x
[PROOFSTEP]
apply orderOf_dvd_of_pow_eq_one
[GOAL]
case h
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ x ^ orderOf x = 1
[PROOFSTEP]
rw [← map_pow, pow_orderOf_eq_one]
[GOAL]
case h
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ↑ψ 1 = 1
[PROOFSTEP]
apply map_one
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
by_cases h0 : orderOf x = 0
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
rw [h0, coprime_zero_right] at h
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
exact ⟨1, by rw [h, pow_one, pow_one]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x
[PROOFSTEP]
rw [h, pow_one, pow_one]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
by_cases h1 : orderOf x = 1
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ (x ^ n) ^ 0 = x
[PROOFSTEP]
rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)
[GOAL]
case neg.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m✝ : ℕ
h✝ : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
[PROOFSTEP]
exact ⟨m, by rw [← pow_mul, pow_eq_mod_orderOf, h, pow_one]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m✝ : ℕ
h✝ : coprime n (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x
[PROOFSTEP]
rw [← pow_mul, pow_eq_mod_orderOf, h, pow_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
⊢ orderOf x = n
[PROOFSTEP]
cases' exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx) with a ha
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ orderOf x = n
[PROOFSTEP]
suffices a = 1 by
  simp [this, ha]
    -- Assume `a` is not one...
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
this : a = 1
⊢ orderOf x = n
[PROOFSTEP]
simp [this, ha]
  -- Assume `a` is not one...
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
⊢ a = 1
[PROOFSTEP]
by_contra h
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ False
[PROOFSTEP]
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n :=
  by
  obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
  rw [hb, ← mul_assoc] at ha
  exact Dvd.intro_left (orderOf x * b) ha.symm
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ minFac a ∣ n
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b✝ : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * minFac a
⊢ minFac a ∣ n
[PROOFSTEP]
rw [hb, ← mul_assoc] at ha
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b✝ : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * minFac a
hb : a = b * minFac a
⊢ minFac a ∣ n
[PROOFSTEP]
exact Dvd.intro_left (orderOf x * b) ha.symm
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ False
[PROOFSTEP]
refine' hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one _
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ x ^ (n / minFac a) = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff a_min_fac_dvd_p_sub_one, ha, mul_comm,
  Nat.mul_dvd_mul_iff_left (orderOf_pos' _)]
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ minFac a ∣ a
[PROOFSTEP]
exact Nat.minFac_dvd a
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ IsOfFinOrder x
[PROOFSTEP]
rw [isOfFinOrder_iff_pow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a✝ b : A
n m : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : minFac a ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
exact Exists.intro n (id ⟨hn, hx⟩)
[GOAL]
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x y✝ : G
a b : A
n m : ℕ
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
[PROOFSTEP]
simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]
[GOAL]
G : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
inst✝¹ : AddMonoid A
x✝ y : G
a b : A
n m : ℕ
H : Type u_6
inst✝ : Monoid H
f : G →* H
hf : Injective ↑f
x : G
⊢ orderOf (↑f x) = orderOf x
[PROOFSTEP]
simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : n ≠ 0
⊢ orderOf (x ^ n) = orderOf x / gcd (orderOf x) n
[PROOFSTEP]
unfold orderOf
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : n ≠ 0
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / gcd (minimalPeriod (fun x_1 => x * x_1) 1) n
[PROOFSTEP]
rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : IsOfFinOrder x
⊢ orderOf (x ^ n) = orderOf x / gcd (orderOf x) n
[PROOFSTEP]
unfold orderOf
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / gcd (minimalPeriod (fun x_1 => x * x_1) 1) n
[PROOFSTEP]
rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime (orderOf y) m
⊢ orderOf (y ^ m) = orderOf y
[PROOFSTEP]
by_cases hg : orderOf y = 0
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime (orderOf y) m
hg : orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y
[PROOFSTEP]
rw [m.coprime_zero_left.mp (hg ▸ h), pow_one]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : coprime (orderOf y) m
hg : ¬orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y
[PROOFSTEP]
rw [orderOf_pow'' y m (hg.imp_symm orderOf_eq_zero), h.gcd_eq_one, Nat.div_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
⊢ orderOf (x * y) ∣ lcm (orderOf x) (orderOf y)
[PROOFSTEP]
rw [orderOf, ← comp_mul_left]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 ∣ lcm (orderOf x) (orderOf y)
[PROOFSTEP]
exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
[PROOFSTEP]
by_cases h0 : orderOf x = 0
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
[PROOFSTEP]
rw [h0, lcm_zero_left]
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0
[PROOFSTEP]
apply dvd_zero
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
[PROOFSTEP]
conv_lhs =>
  rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0), _root_.pow_succ', mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf y
[PROOFSTEP]
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0), _root_.pow_succ', mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf y
[PROOFSTEP]
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0), _root_.pow_succ', mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : ¬orderOf x = 0
| orderOf y
[PROOFSTEP]
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0), _root_.pow_succ', mul_assoc]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ pred (orderOf x) * (x * y)) ∣ lcm (orderOf x) (orderOf (x * y))
[PROOFSTEP]
exact
  (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
    (lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (dvd_lcm_left _ _), dvd_lcm_right _ _⟩)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hco : coprime (orderOf x) (orderOf y)
⊢ orderOf (x * y) = orderOf x * orderOf y
[PROOFSTEP]
rw [orderOf, ← comp_mul_left]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hco : coprime (orderOf x) (orderOf y)
⊢ minimalPeriod ((fun x_1 => x * x_1) ∘ fun x => y * x) 1 = orderOf x * orderOf y
[PROOFSTEP]
exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y
[PROOFSTEP]
have hoy := orderOf_pos' hy
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
⊢ orderOf (x * y) = orderOf y
[PROOFSTEP]
have hxy := dvd_of_forall_prime_mul_dvd hdvd
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) = orderOf y
[PROOFSTEP]
apply orderOf_eq_of_pow_and_pow_div_prime hoy
[GOAL]
case hx
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ (x * y) ^ orderOf y = 1
[PROOFSTEP]
simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
[GOAL]
case hd
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → (x * y) ^ (orderOf y / p) ≠ 1
[PROOFSTEP]
simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
[GOAL]
case hx
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y
[PROOFSTEP]
exact h.orderOf_mul_dvd_lcm.trans (lcm_dvd hxy dvd_rfl)
[GOAL]
case hd
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
[PROOFSTEP]
refine' fun p hp hpy hd => hp.ne_one _
[GOAL]
case hd
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p = 1
[PROOFSTEP]
rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff hpy]
[GOAL]
case hd
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p
[PROOFSTEP]
refine' (orderOf_dvd_lcm_mul h).trans (lcm_dvd ((dvd_div_iff hpy).2 _) hd)
[GOAL]
case hd
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ p * orderOf x ∣ orderOf y
[PROOFSTEP]
by_cases h : p ∣ orderOf x
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h✝ : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m : ℕ
h✝ : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : ¬p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y
[PROOFSTEP]
exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
hg : x ^ p = 1
hg1 : x ≠ 1
⊢ ¬IsFixedPt (fun x_1 => x * x_1) 1
[PROOFSTEP]
rwa [IsFixedPt, mul_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ orderOf x = p ^ (n + 1)
[PROOFSTEP]
apply minimalPeriod_eq_prime_pow
[GOAL]
case hk
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ ¬IsPeriodicPt (fun x_1 => x * x_1) (p ^ n) 1
[PROOFSTEP]
rwa [isPeriodicPt_mul_iff_pow_eq_one]
[GOAL]
case hk1
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun x_1 => x * x_1) (p ^ (n + 1)) 1
[PROOFSTEP]
rwa [isPeriodicPt_mul_iff_pow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ p ^ k = 1
[PROOFSTEP]
rw [← hk, pow_orderOf_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
⊢ ∃ k, orderOf x = p ^ k
[PROOFSTEP]
obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
inst✝ : AddMonoid A
x y : G
a b : A
n m p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
k : ℕ
left✝ : k ≤ w✝
hk : orderOf x = p ^ k
⊢ ∃ k, orderOf x = p ^ k
[PROOFSTEP]
exact ⟨k, hk⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m n : ℕ
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
[PROOFSTEP]
wlog hmn : m ≤ n generalizing m n
[GOAL]
case inr
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
[PROOFSTEP]
rw [eq_comm, ModEq.comm, this (le_of_not_le hmn)]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
[PROOFSTEP]
rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
[PROOFSTEP]
exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
⊢ (Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
[PROOFSTEP]
refine' ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => _⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m✝ n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m
[PROOFSTEP]
rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x y : G
m✝ n✝ : ℕ
h : orderOf x = 0
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m
[PROOFSTEP]
rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
[PROOFSTEP]
let s := {n | 0 < n}.image fun n : ℕ => x ^ n
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
[PROOFSTEP]
have hs : s ⊆ {y : G | ¬IsOfFinOrder y} :=
  by
  rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
  apply h
  rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
  obtain ⟨m, hm, hm'⟩ := contra
  exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
⊢ s ⊆ {y | ¬IsOfFinOrder y}
[PROOFSTEP]
rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
⊢ IsOfFinOrder x
[PROOFSTEP]
rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ n_1, 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
obtain ⟨m, hm, hm'⟩ := contra
[GOAL]
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m✝ n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m✝ n✝ : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ x ^ (n * m) = 1
[PROOFSTEP]
rwa [pow_mul]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
[PROOFSTEP]
suffices s.Infinite by exact this.mono hs
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
this : Set.Infinite s
⊢ Set.Infinite {y | ¬IsOfFinOrder y}
[PROOFSTEP]
exact this.mono hs
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
⊢ Set.Infinite s
[PROOFSTEP]
contrapose! h
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
⊢ IsOfFinOrder x
[PROOFSTEP]
have : ¬Injective fun n : ℕ => x ^ n :=
  by
  have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
  contrapose! this
  exact Set.injOn_of_injective this _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
⊢ ¬Injective fun n => x ^ n
[PROOFSTEP]
have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
this : ¬Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
⊢ ¬Injective fun n => x ^ n
[PROOFSTEP]
contrapose! this
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
this : Injective fun n => x ^ n
⊢ Set.InjOn (fun n => x ^ n) (Set.Ioi 0)
[PROOFSTEP]
exact Set.injOn_of_injective this _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LeftCancelMonoid G
x✝ y : G
m n : ℕ
x : G
s : Set G := (fun n => x ^ n) '' {n | 0 < n}
hs : s ⊆ {y | ¬IsOfFinOrder y}
h : ¬Set.Infinite ((fun n => x ^ n) '' {n | 0 < n})
this : ¬Injective fun n => x ^ n
⊢ IsOfFinOrder x
[PROOFSTEP]
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x✝ y : G
i : ℤ
x : G
hx : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ x⁻¹ ^ n = 1
[PROOFSTEP]
rcases(isOfFinOrder_iff_pow_eq_one x).mp hx with ⟨n, npos, hn⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x✝ y : G
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x⁻¹ ^ n = 1
[PROOFSTEP]
refine' ⟨n, npos, by simp_rw [inv_pow, hn, inv_one]⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x✝ y : G
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ x⁻¹ ^ n = 1
[PROOFSTEP]
simp_rw [inv_pow, hn, inv_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
⊢ ↑(orderOf x) ∣ i ↔ x ^ i = 1
[PROOFSTEP]
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
[GOAL]
case intro.inl
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1
[PROOFSTEP]
rw [Int.coe_nat_dvd, orderOf_dvd_iff_pow_eq_one, zpow_ofNat]
[GOAL]
case intro.inr
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
[PROOFSTEP]
rw [dvd_neg, Int.coe_nat_dvd, zpow_neg, inv_eq_one, zpow_ofNat, orderOf_dvd_iff_pow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x✝ y : G
i : ℤ
x : G
⊢ orderOf x⁻¹ = orderOf x
[PROOFSTEP]
simp [orderOf_eq_orderOf_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
⊢ x ^ i = ?m.965169
[PROOFSTEP]
rw [← Int.emod_add_ediv i (orderOf x)]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
⊢ x ^ (i % ↑(orderOf x) + ↑(orderOf x) * (i / ↑(orderOf x))) = x ^ (i % ↑(orderOf x))
[PROOFSTEP]
simp [zpow_add, zpow_mul, pow_orderOf_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
⊢ (x ^ i) ^ orderOf x = 1
[PROOFSTEP]
by_cases h : IsOfFinOrder x
[GOAL]
case pos
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
[PROOFSTEP]
rw [← zpow_ofNat, ← zpow_mul, mul_comm, zpow_mul, zpow_ofNat, pow_orderOf_eq_one, one_zpow]
[GOAL]
case neg
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
[PROOFSTEP]
rw [orderOf_eq_zero h, _root_.pow_zero]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
h : IsOfFinOrder x
h' : y ∈ Subgroup.zpowers x
⊢ IsOfFinOrder y
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
k : ℤ
h' : x ^ k ∈ Subgroup.zpowers x
⊢ IsOfFinOrder (x ^ k)
[PROOFSTEP]
exact h.zpow
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
i : ℤ
h : y ∈ Subgroup.zpowers x
⊢ orderOf y ∣ orderOf x
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x : G
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x
[PROOFSTEP]
rw [orderOf_dvd_iff_pow_eq_one]
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x : G
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ (x ^ k) ^ orderOf x = 1
[PROOFSTEP]
exact zpow_pow_orderOf
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α✝ : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
i : ℤ
α : Type u_6
inst✝ : MulAction G α
hx : x ∈ Subgroup.zpowers y
a : α
hs : y • a = a
⊢ x • a = a
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α✝ : Type u_4
β : Type u_5
inst✝¹ : Group G
y : G
i : ℤ
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ y ^ k • a = a
[PROOFSTEP]
rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, MonoidHom.map_zpow _ y k, MulAction.toPermHom_apply]
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α✝ : Type u_4
β : Type u_5
inst✝¹ : Group G
y : G
i : ℤ
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ ↑(MulAction.toPerm y ^ k) a = a
[PROOFSTEP]
exact Function.IsFixedPt.perm_zpow (by exact hs) k
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α✝ : Type u_4
β : Type u_5
inst✝¹ : Group G
y : G
i : ℤ
α : Type u_6
inst✝ : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : y ^ k ∈ Subgroup.zpowers y
⊢ IsFixedPt (↑(MulAction.toPerm y)) a
[PROOFSTEP]
exact hs
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∀ (x : ℕ),
    x ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n)) →
      ∀ (y : ℕ),
        y ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n)) →
          x ≠ y →
            Disjoint (Finset.filter (fun x_1 => orderOf x_1 = x) Finset.univ)
              (Finset.filter (fun x => orderOf x = y) Finset.univ)
[PROOFSTEP]
intros
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x✝ : ℕ
a✝² : x✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
y✝ : ℕ
a✝¹ : y✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
a✝ : x✝ ≠ y✝
⊢ Disjoint (Finset.filter (fun x => orderOf x = x✝) Finset.univ) (Finset.filter (fun x => orderOf x = y✝) Finset.univ)
[PROOFSTEP]
apply Finset.disjoint_filter.2
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x✝ : ℕ
a✝² : x✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
y✝ : ℕ
a✝¹ : y✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
a✝ : x✝ ≠ y✝
⊢ ∀ (x : G), x ∈ Finset.univ → orderOf x = x✝ → ¬orderOf x = y✝
[PROOFSTEP]
rintro _ _ rfl
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
y✝ : ℕ
a✝³ : y✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
x✝ : G
a✝² : x✝ ∈ Finset.univ
a✝¹ : orderOf x✝ ∈ Finset.filter (fun x => x ∣ n) (Finset.range (succ n))
a✝ : orderOf x✝ ≠ y✝
⊢ ¬orderOf x✝ = y✝
[PROOFSTEP]
assumption
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ ∀ (a : G),
    (a ∈
        Finset.biUnion (Finset.filter (fun x => x ∣ n) (Finset.range (succ n))) fun m =>
          Finset.filter (fun x => orderOf x = m) Finset.univ) ↔
      a ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ
[PROOFSTEP]
intro x
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x✝ : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x : G
⊢ (x ∈
      Finset.biUnion (Finset.filter (fun x => x ∣ n) (Finset.range (succ n))) fun m =>
        Finset.filter (fun x => orderOf x = m) Finset.univ) ↔
    x ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ
[PROOFSTEP]
suffices orderOf x ≤ n ∧ orderOf x ∣ n ↔ x ^ n = 1 by simpa [Nat.lt_succ_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x✝ : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x : G
this : orderOf x ≤ n ∧ orderOf x ∣ n ↔ x ^ n = 1
⊢ (x ∈
      Finset.biUnion (Finset.filter (fun x => x ∣ n) (Finset.range (succ n))) fun m =>
        Finset.filter (fun x => orderOf x = m) Finset.univ) ↔
    x ∈ Finset.filter (fun x => x ^ n = 1) Finset.univ
[PROOFSTEP]
simpa [Nat.lt_succ_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x✝ : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x : G
⊢ orderOf x ≤ n ∧ orderOf x ∣ n ↔ x ^ n = 1
[PROOFSTEP]
exact
  ⟨fun h => by
    let ⟨m, hm⟩ := h.2
    rw [hm, pow_mul, pow_orderOf_eq_one, one_pow], fun h =>
    ⟨orderOf_le_of_pow_eq_one hn.bot_lt h, orderOf_dvd_of_pow_eq_one h⟩⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x✝ : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x : G
h : orderOf x ≤ n ∧ orderOf x ∣ n
⊢ x ^ n = 1
[PROOFSTEP]
let ⟨m, hm⟩ := h.2
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Monoid G
x✝ : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
x : G
h : orderOf x ≤ n ∧ orderOf x ∣ n
m : ℕ
hm : n = orderOf x * m
⊢ x ^ n = 1
[PROOFSTEP]
rw [hm, pow_mul, pow_orderOf_eq_one, one_pow]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
⊢ IsOfFinOrder x
[PROOFSTEP]
have : (Set.univ : Set G).Finite := Set.univ.toFinite
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
this : Set.Finite Set.univ
⊢ IsOfFinOrder x
[PROOFSTEP]
contrapose! this
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
this : ¬IsOfFinOrder x
⊢ ¬Set.Finite Set.univ
[PROOFSTEP]
exact Set.Infinite.mono (Set.subset_univ _) (infinite_not_isOfFinOrder this)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x✝ y : G
n✝ : ℕ
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivPowers x).symm { val := x ^ n, property := hn } =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
[PROOFSTEP]
rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, pow_eq_mod_orderOf, Fin.val_mk]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x y : G
n✝ : ℕ
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(powersEquivPowers h) { val := x ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ n) } =
    { val := y ^ n, property := (_ : ∃ y_1, (fun x x_1 => x ^ x_1) y y_1 = y ^ n) }
[PROOFSTEP]
rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ← Equiv.eq_symm_apply,
  finEquivPowers_symm_apply]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : LeftCancelMonoid G
x y : G
n✝ : ℕ
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(Fin.castIso h).toEquiv { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) } =
    { val := n % orderOf y, isLt := (_ : n % orderOf y < orderOf y) }
[PROOFSTEP]
simp [h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
⊢ ∃ i x_1, x ^ i = 1
[PROOFSTEP]
rcases exists_pow_eq_one x with ⟨w, hw1, hw2⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ ∃ i x_1, x ^ i = 1
[PROOFSTEP]
refine' ⟨w, Int.coe_nat_ne_zero.mpr (_root_.ne_of_gt hw1), _⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ ↑w = 1
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n : ℕ
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ w = 1
[PROOFSTEP]
exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n✝ : ℕ
inst✝ : Finite G
x✝ : y ∈ Submonoid.powers x
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = y
⊢ (fun x x_1 => x ^ x_1) x ↑n = y
[PROOFSTEP]
simp_all
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Finite G
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x x_1 => x ^ x_1) x i = y
⊢ (fun x x_1 => x ^ x_1) x (Int.natAbs (i % ↑(orderOf x))) = y
[PROOFSTEP]
dsimp only
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Finite G
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x x_1 => x ^ x_1) x i = y
⊢ x ^ Int.natAbs (i % ↑(orderOf x)) = y
[PROOFSTEP]
rwa [← zpow_ofNat, Int.natAbs_of_nonneg (Int.emod_nonneg _ (Int.coe_nat_ne_zero_iff_pos.2 (orderOf_pos x))), ←
  zpow_eq_mod_orderOf]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G
x y : G
n : ℕ
inst✝¹ : Finite G
inst✝ : DecidableEq G
⊢ y ∈ zpowers x ↔ y ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (orderOf x))
[PROOFSTEP]
rw [← mem_powers_iff_mem_zpowers, mem_powers_iff_mem_range_orderOf]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n✝ : ℕ
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]
[PROOFSTEP]
rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n✝ : ℕ
m n : ℤ
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]
[PROOFSTEP]
rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd, zero_sub, neg_sub]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n : ℕ
⊢ (Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x
[PROOFSTEP]
refine' ⟨_, fun h n m hnm => _⟩
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n : ℕ
⊢ (Injective fun n => x ^ n) → ¬IsOfFinOrder x
[PROOFSTEP]
simp_rw [isOfFinOrder_iff_pow_eq_one]
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n : ℕ
⊢ (Injective fun n => x ^ n) → ¬∃ n, 0 < n ∧ x ^ n = 1
[PROOFSTEP]
rintro h ⟨n, hn, hx⟩
[GOAL]
case refine'_1.intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n✝ : ℕ
h : Injective fun n => x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
[PROOFSTEP]
exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n✝ : ℕ
h : Injective fun n => x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ (fun n => x ^ n) ↑n = (fun n => x ^ n) 0
[PROOFSTEP]
simpa using hx
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Group G
x y : G
n✝ : ℕ
h : ¬IsOfFinOrder x
n m : ℤ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m
[PROOFSTEP]
rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n✝ : ℕ
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivZpowers x).symm { val := x ^ n, property := hn } =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
[PROOFSTEP]
rw [finEquivZpowers, Equiv.symm_trans_apply]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x✝ y : G
n✝ : ℕ
inst✝ : Finite G
x : G
n : ℕ
hn : ∃ m, x ^ m = x ^ n
⊢ ↑(finEquivPowers x).symm
      (↑(Equiv.Set.ofEq (_ : ↑(Submonoid.powers x) = ↑(zpowers x))).symm { val := x ^ n, property := hn }) =
    { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }
[PROOFSTEP]
exact finEquivPowers_symm_apply x n
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n✝ : ℕ
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(zpowersEquivZpowers h) { val := x ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ n) } =
    { val := y ^ n, property := (_ : ∃ y_1, (fun x x_1 => x ^ x_1) y y_1 = y ^ n) }
[PROOFSTEP]
rw [zpowersEquivZpowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZpowers_symm_apply, ← Equiv.eq_symm_apply,
  finEquivZpowers_symm_apply]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n✝ : ℕ
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ ↑(Fin.castIso h).toEquiv { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) } =
    { val := n % orderOf y, isLt := (_ : n % orderOf y < orderOf y) }
[PROOFSTEP]
simp [h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
classical
have ft_prod : Fintype ((G ⧸ zpowers x) × zpowers x) := Fintype.ofEquiv G groupEquivQuotientProdSubgroup
have ft_s : Fintype (zpowers x) := @Fintype.prodRight _ _ _ ft_prod _
have ft_cosets : Fintype (G ⧸ zpowers x) := @Fintype.prodLeft _ _ _ ft_prod ⟨⟨1, (zpowers x).one_mem⟩⟩
have eq₁ : Fintype.card G = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
  calc
    Fintype.card G = @Fintype.card _ ft_prod := @Fintype.card_congr _ _ _ ft_prod groupEquivQuotientProdSubgroup
    _ = @Fintype.card _ (@instFintypeProd _ _ ft_cosets ft_s) := (congr_arg (@Fintype.card _) <| Subsingleton.elim _ _)
    _ = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s := @Fintype.card_prod _ _ ft_cosets ft_s
have eq₂ : orderOf x = @Fintype.card _ ft_s :=
  calc
    orderOf x = _ := orderOf_eq_card_zpowers
    _ = _ := congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
exact Dvd.intro (@Fintype.card (G ⧸ Subgroup.zpowers x) ft_cosets) (by rw [eq₁, eq₂, mul_comm])
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
have ft_prod : Fintype ((G ⧸ zpowers x) × zpowers x) := Fintype.ofEquiv G groupEquivQuotientProdSubgroup
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
have ft_s : Fintype (zpowers x) := @Fintype.prodRight _ _ _ ft_prod _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
ft_s : Fintype { x_1 // x_1 ∈ zpowers x }
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
have ft_cosets : Fintype (G ⧸ zpowers x) := @Fintype.prodLeft _ _ _ ft_prod ⟨⟨1, (zpowers x).one_mem⟩⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
ft_s : Fintype { x_1 // x_1 ∈ zpowers x }
ft_cosets : Fintype (G ⧸ zpowers x)
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
have eq₁ : Fintype.card G = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
  calc
    Fintype.card G = @Fintype.card _ ft_prod := @Fintype.card_congr _ _ _ ft_prod groupEquivQuotientProdSubgroup
    _ = @Fintype.card _ (@instFintypeProd _ _ ft_cosets ft_s) := (congr_arg (@Fintype.card _) <| Subsingleton.elim _ _)
    _ = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s := @Fintype.card_prod _ _ ft_cosets ft_s
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
ft_s : Fintype { x_1 // x_1 ∈ zpowers x }
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : Fintype.card G = Fintype.card (G ⧸ zpowers x) * Fintype.card { x_1 // x_1 ∈ zpowers x }
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
have eq₂ : orderOf x = @Fintype.card _ ft_s :=
  calc
    orderOf x = _ := orderOf_eq_card_zpowers
    _ = _ := congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
ft_s : Fintype { x_1 // x_1 ∈ zpowers x }
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : Fintype.card G = Fintype.card (G ⧸ zpowers x) * Fintype.card { x_1 // x_1 ∈ zpowers x }
eq₂ : orderOf x = Fintype.card { x_1 // x_1 ∈ zpowers x }
⊢ orderOf x ∣ Fintype.card G
[PROOFSTEP]
exact Dvd.intro (@Fintype.card (G ⧸ Subgroup.zpowers x) ft_cosets) (by rw [eq₁, eq₂, mul_comm])
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
ft_prod : Fintype ((G ⧸ zpowers x) × { x_1 // x_1 ∈ zpowers x })
ft_s : Fintype { x_1 // x_1 ∈ zpowers x }
ft_cosets : Fintype (G ⧸ zpowers x)
eq₁ : Fintype.card G = Fintype.card (G ⧸ zpowers x) * Fintype.card { x_1 // x_1 ∈ zpowers x }
eq₂ : orderOf x = Fintype.card { x_1 // x_1 ∈ zpowers x }
⊢ orderOf x * Fintype.card (G ⧸ zpowers x) = Fintype.card G
[PROOFSTEP]
rw [eq₁, eq₂, mul_comm]
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
x : G
⊢ orderOf x ∣ Nat.card G
[PROOFSTEP]
cases' fintypeOrInfinite G with h h
[GOAL]
case inl
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, orderOf_dvd_card_univ]
[GOAL]
case inr
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x✝ y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G
[PROOFSTEP]
simp only [card_eq_zero_of_infinite, dvd_zero]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
⊢ x ^ Fintype.card G = 1
[PROOFSTEP]
rw [← Nat.card_eq_fintype_card, pow_card_eq_one']
[GOAL]
G✝ : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : Group G✝
x y : G✝
n : ℕ
inst✝² : Fintype G✝
G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
⊢ g ^ index H ∈ H
[PROOFSTEP]
rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n✝ : ℕ
inst✝ : Fintype G
n : ℕ
⊢ x ^ n = x ^ (n % Fintype.card G)
[PROOFSTEP]
rw [pow_eq_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card_univ, ← pow_eq_mod_orderOf]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n✝ : ℕ
inst✝ : Fintype G
n : ℤ
⊢ x ^ n = x ^ (n % ↑(Fintype.card G))
[PROOFSTEP]
rw [zpow_eq_mod_orderOf, ← Int.emod_emod_of_dvd n (Int.coe_nat_dvd.2 orderOf_dvd_card_univ), ← zpow_eq_mod_orderOf]
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
⊢ (fun g => g ^ gcdB (Nat.card G) n) ((fun g => g ^ n) g) = g
[PROOFSTEP]
have key := congr_arg ((· ^ ·) g) ((Nat.card G).gcd_eq_gcd_ab n)
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
key :
  (fun x x_1 => x ^ x_1) g ↑(gcd (Nat.card G) n) =
    (fun x x_1 => x ^ x_1) g (↑(Nat.card G) * gcdA (Nat.card G) n + ↑n * gcdB (Nat.card G) n)
⊢ (fun g => g ^ gcdB (Nat.card G) n) ((fun g => g ^ n) g) = g
[PROOFSTEP]
dsimp only at key
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
key : g ^ ↑(gcd (Nat.card G) n) = g ^ (↑(Nat.card G) * gcdA (Nat.card G) n + ↑n * gcdB (Nat.card G) n)
⊢ (fun g => g ^ gcdB (Nat.card G) n) ((fun g => g ^ n) g) = g
[PROOFSTEP]
rwa [zpow_add, zpow_mul, zpow_mul, zpow_ofNat, zpow_ofNat, zpow_ofNat, h.gcd_eq_one, pow_one, pow_card_eq_one',
  one_zpow, one_mul, eq_comm] at key
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
⊢ (fun g => g ^ n) ((fun g => g ^ gcdB (Nat.card G) n) g) = g
[PROOFSTEP]
have key := congr_arg ((· ^ ·) g) ((Nat.card G).gcd_eq_gcd_ab n)
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
key :
  (fun x x_1 => x ^ x_1) g ↑(gcd (Nat.card G) n) =
    (fun x x_1 => x ^ x_1) g (↑(Nat.card G) * gcdA (Nat.card G) n + ↑n * gcdB (Nat.card G) n)
⊢ (fun g => g ^ n) ((fun g => g ^ gcdB (Nat.card G) n) g) = g
[PROOFSTEP]
dsimp only at key
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G✝
x y : G✝
n : ℕ
inst✝¹ : Fintype G✝
G : Type u_6
inst✝ : Group G
h : coprime (Nat.card G) n
g : G
key : g ^ ↑(gcd (Nat.card G) n) = g ^ (↑(Nat.card G) * gcdA (Nat.card G) n + ↑n * gcdB (Nat.card G) n)
⊢ (fun g => g ^ n) ((fun g => g ^ gcdB (Nat.card G) n) g) = g
[PROOFSTEP]
rwa [zpow_add, zpow_mul, zpow_mul', zpow_ofNat, zpow_ofNat, zpow_ofNat, h.gcd_eq_one, pow_one, pow_card_eq_one',
  one_zpow, one_mul, eq_comm] at key
[GOAL]
G✝ : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝⁴ : Group G✝
x y : G✝
n : ℕ
inst✝³ : Fintype G✝
G : Type u_6
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
⊢ H ⊓ K = ⊥
[PROOFSTEP]
refine' (H ⊓ K).eq_bot_iff_forall.mpr fun x hx => _
[GOAL]
G✝ : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝⁴ : Group G✝
x✝ y : G✝
n : ℕ
inst✝³ : Fintype G✝
G : Type u_6
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
x : G
hx : x ∈ H ⊓ K
⊢ x = 1
[PROOFSTEP]
rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← h.gcd_eq_one, Nat.dvd_gcd_iff]
[GOAL]
G✝ : Type u_1
H✝ : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝⁴ : Group G✝
x✝ y : G✝
n : ℕ
inst✝³ : Fintype G✝
G : Type u_6
inst✝² : Group G
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype { x // x ∈ K }
h : coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })
x : G
hx : x ∈ H ⊓ K
⊢ orderOf x ∣ Fintype.card { x // x ∈ H } ∧ orderOf x ∣ Fintype.card { x // x ∈ K }
[PROOFSTEP]
exact
  ⟨(congr_arg (· ∣ Fintype.card H) (orderOf_subgroup ⟨x, hx.1⟩)).mpr orderOf_dvd_card_univ,
    (congr_arg (· ∣ Fintype.card K) (orderOf_subgroup ⟨x, hx.2⟩)).mpr orderOf_dvd_card_univ⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G
x y : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
⊢ Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = Set.toFinset ↑(zpowers x)
[PROOFSTEP]
ext x
[GOAL]
case a
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝² : Group G
x✝ y : G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x : G
⊢ x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ Set.toFinset ↑(zpowers x✝)
[PROOFSTEP]
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
h : x ^ gcd n (Fintype.card G) = 1
⊢ x ^ n = 1
[PROOFSTEP]
let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Group G
x y : G
n : ℕ
inst✝ : Fintype G
h : x ^ gcd n (Fintype.card G) = 1
m : ℕ
hm : n = gcd n (Fintype.card G) * m
⊢ x ^ n = 1
[PROOFSTEP]
rw [hm, pow_mul, h, one_pow]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Fintype M
S : Set M
hS1 : Set.Nonempty S
hS2 : S * S = S
a : M
ha : a ∈ S
⊢ a ^ (zero + 1) ∈ S
[PROOFSTEP]
rwa [Nat.zero_eq, zero_add, pow_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Fintype M
S : Set M
hS1 : Set.Nonempty S
hS2 : S * S = S
pow_mem : ∀ (a : M), a ∈ S → ∀ (n : ℕ), a ^ (n + 1) ∈ S
⊢ 1 ∈ { carrier := S, mul_mem' := (_ : ∀ {a b : M}, a ∈ S → b ∈ S → a * b ∈ S) }.carrier
[PROOFSTEP]
obtain ⟨a, ha⟩ := hS1
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Fintype M
S : Set M
hS2 : S * S = S
pow_mem : ∀ (a : M), a ∈ S → ∀ (n : ℕ), a ^ (n + 1) ∈ S
a : M
ha : a ∈ S
⊢ 1 ∈ { carrier := S, mul_mem' := (_ : ∀ {a b : M}, a ∈ S → b ∈ S → a * b ∈ S) }.carrier
[PROOFSTEP]
rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Fintype M
S : Set M
hS2 : S * S = S
pow_mem : ∀ (a : M), a ∈ S → ∀ (n : ℕ), a ^ (n + 1) ∈ S
a : M
ha : a ∈ S
⊢ a ^ (orderOf a - succ 0 + succ 0) ∈ { carrier := S, mul_mem' := (_ : ∀ {a b : M}, a ∈ S → b ∈ S → a * b ∈ S) }.carrier
[PROOFSTEP]
exact pow_mem a ha (orderOf a - 1)
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS1 : Set.Nonempty S
hS2 : S * S = S
src✝ : Submonoid G := submonoidOfIdempotent S hS1 hS2
a : G
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := S, mul_mem' := (_ : ∀ {a b : G}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
⊢ a⁻¹ ∈ submonoidOfIdempotent S hS1 hS2
[PROOFSTEP]
rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS1 : Set.Nonempty S
hS2 : S * S = S
src✝ : Submonoid G := submonoidOfIdempotent S hS1 hS2
a : G
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := S, mul_mem' := (_ : ∀ {a b : G}, a ∈ src✝.carrier → b ∈ src✝.carrier → a * b ∈ src✝.carrier) },
          one_mem' := (_ : 1 ∈ src✝.carrier) }.toSubsemigroup.carrier
⊢ a ^ (orderOf a - succ 0) ∈ submonoidOfIdempotent S hS1 hS2
[PROOFSTEP]
exact pow_mem ha (orderOf a - 1)
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : Set.Nonempty S
⊢ 1 ∈ S ^ Fintype.card G
[PROOFSTEP]
obtain ⟨a, ha⟩ := hS
[GOAL]
case intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ 1 ∈ S ^ Fintype.card G
[PROOFSTEP]
rw [← pow_card_eq_one]
[GOAL]
case intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ ?m.1815695 ^ Fintype.card G ∈ S ^ Fintype.card G
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ G
[PROOFSTEP]
exact Set.pow_mem_pow ha (Fintype.card G)
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : Set.Nonempty S
one_mem : 1 ∈ S ^ Fintype.card G
⊢ S ^ Fintype.card G * S ^ Fintype.card G = S ^ Fintype.card G
[PROOFSTEP]
classical!
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : Set.Nonempty S
one_mem : 1 ∈ S ^ Fintype.card G
em✝ : (a : Prop) → Decidable a
⊢ S ^ Fintype.card G * S ^ Fintype.card G = S ^ Fintype.card G
[PROOFSTEP]
apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : Set.Nonempty S
one_mem : 1 ∈ S ^ Fintype.card G
em✝ : (a : Prop) → Decidable a
⊢ Fintype.card ↑(S ^ Fintype.card G) = Fintype.card ↑(S ^ Fintype.card G * S ^ Fintype.card G)
[PROOFSTEP]
simp_rw [← pow_add, Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x = 0
[PROOFSTEP]
rw [orderOf_eq_zero_iff']
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1
[PROOFSTEP]
intro n hn hx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
[PROOFSTEP]
replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ |x| ^ n = 1
[PROOFSTEP]
simpa only [abs_one, abs_pow] using congr_arg abs hx
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
⊢ False
[PROOFSTEP]
cases' h.lt_or_lt with h h
[GOAL]
case inl
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : |x| < 1
⊢ False
[PROOFSTEP]
exact ((pow_lt_one (abs_nonneg x) h hn.ne').ne hx).elim
[GOAL]
case inr
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h✝ : |x| ≠ 1
n : ℕ
hn : 0 < n
hx : |x| ^ n = 1
h : 1 < |x|
⊢ False
[PROOFSTEP]
exact ((one_lt_pow h hn.ne').ne' hx).elim
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
⊢ orderOf x ≤ 2
[PROOFSTEP]
cases' ne_or_eq |x| 1 with h h
[GOAL]
case inl
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| ≠ 1
⊢ orderOf x ≤ 2
[PROOFSTEP]
simp [orderOf_abs_ne_one h]
[GOAL]
case inr
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
x : G
h : |x| = 1
⊢ orderOf x ≤ 2
[PROOFSTEP]
rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
[GOAL]
case inr.inl
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
h : |1| = 1
⊢ orderOf 1 ≤ 2
[PROOFSTEP]
simp
[GOAL]
case inr.inr
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ orderOf (-1) ≤ 2
[PROOFSTEP]
apply orderOf_le_of_pow_eq_one
[GOAL]
case inr.inr.hn
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
case inr.inr.h
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : LinearOrderedRing G
h : |(-1)| = 1
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
x : α × β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)
[PROOFSTEP]
simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
c : α
x : β
⊢ c⁻¹ • c • x = x
[PROOFSTEP]
rw [smul_smul, mul_left_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
c : α
x : β
⊢ c • c⁻¹ • x = x
[PROOFSTEP]
rw [smul_smul, mul_right_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one, smul_mul_smul, mul_right_inv, mul_right_inv, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
p : ℤ
⊢ (c • x) ^ p = c ^ p • x ^ p
[PROOFSTEP]
cases p
[GOAL]
case ofNat
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
a✝ : ℕ
⊢ (c • x) ^ Int.ofNat a✝ = c ^ Int.ofNat a✝ • x ^ Int.ofNat a✝
[PROOFSTEP]
simp [smul_pow, smul_inv]
[GOAL]
case negSucc
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Group β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
a✝ : ℕ
⊢ (c • x) ^ Int.negSucc a✝ = c ^ Int.negSucc a✝ • x ^ Int.negSucc a✝
[PROOFSTEP]
simp [smul_pow, smul_inv]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Mul β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
a b : β
r : α
⊢ Commute (r • a) b ↔ Commute a b
[PROOFSTEP]
rw [Commute.symm_iff, Commute.smul_right_iff, Commute.symm_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
a✝ a : α
ha : a ≠ 0
x y : β
h : a⁻¹ • x = y
⊢ x = a • y
[PROOFSTEP]
rw [← h, smul_inv_smul₀ ha]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
a✝ a : α
ha : a ≠ 0
x y : β
h : x = a • y
⊢ a⁻¹ • x = y
[PROOFSTEP]
rw [h, inv_smul_smul₀ ha]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : AddMonoid β
inst✝ : DistribMulAction α β
a : α
x : β
h : a • x = 0
⊢ x = 0
[PROOFSTEP]
rw [← inv_smul_smul a x, h, smul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
⊢ ∀ (b : A → B), 1 • b = b
[PROOFSTEP]
intro f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ 1 • f = f
[PROOFSTEP]
show (fun x => f ((1 : G)⁻¹ • x)) = f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ (fun x => f (1⁻¹ • x)) = f
[PROOFSTEP]
simp only [inv_one, one_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
⊢ ∀ (x y : G) (b : A → B), (x * y) • b = x • y • b
[PROOFSTEP]
intros x y f
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (x * y) • f = x • y • f
[PROOFSTEP]
show (fun a => f ((x * y)⁻¹ • a)) = (fun a => f (y⁻¹ • x⁻¹ • a))
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
A : Type u_2
B : Type u_3
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
x y : G
f : A → B
⊢ (fun a => f ((x * y)⁻¹ • a)) = fun a => f (y⁻¹ • x⁻¹ • a)
[PROOFSTEP]
simp only [mul_smul, mul_inv_rev]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ : Group α
inst✝⁴ : Monoid β
inst✝³ : AddGroup β
inst✝² : DistribMulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
r : α
a : β
⊢ IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
[PROOFSTEP]
rw [← isUnit_smul_iff r (1 - r⁻¹ • a), smul_sub, smul_inv_smul]


[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
x✝³ x✝² x✝¹ : α
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
b : { x // x ∈ ↑opposite (normalizer H) }
c x✝¹ : α
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc, mem_normalizer_iff'.mp b.prop,
  mul_assoc, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
hH : Normal H
x✝³ : αᵐᵒᵖ
x✝² x✝¹ : α
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H
[PROOFSTEP]
rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc, mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ : Group α
inst✝² : Monoid β
inst✝¹ : MulAction β α
H : Subgroup α
inst✝ : QuotientAction β H
b : β
q : α ⧸ H
⊢ ↑(b • Quotient.out' q) = b • q
[PROOFSTEP]
rw [← Quotient.smul_mk, QuotientGroup.out_eq']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Group α
inst✝¹ : Monoid β
inst✝ : MulAction β α
H : Subgroup α
a : α
q : α ⧸ H
⊢ (Quotient.out' q)⁻¹ * a ^ minimalPeriod ((fun x x_1 => x • x_1) a) q * Quotient.out' q ∈ H
[PROOFSTEP]
rw [mul_assoc, ← QuotientGroup.eq', QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out', eq_comm,
  pow_smul_eq_iff_minimalPeriod_dvd]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
g : α ⧸ stabilizer α x
g1 g2 : α
H : Setoid.r g1 g2
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x
[PROOFSTEP]
rw [smul_smul, mul_inv_cancel_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ Setoid.r g₁ g₂
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer α x
[PROOFSTEP]
show (g₁⁻¹ * g₂) • x = x
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x : β
y₁ y₂ : α ⧸ stabilizer α x
g₁ g₂ : α
H : g₁ • x = g₂ • x
⊢ (g₁⁻¹ * g₂) • x = x
[PROOFSTEP]
rw [mul_smul, ← H, inv_smul_smul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² inst✝¹ : Group α
inst✝ : MulAction α β
x✝ b : β
x y : α ⧸ stabilizer α b
hxy :
  (fun g => { val := ofQuotientStabilizer α b g, property := (_ : ofQuotientStabilizer α b g ∈ orbit α b) }) x =
    (fun g => { val := ofQuotientStabilizer α b g, property := (_ : ofQuotientStabilizer α b g ∈ orbit α b) }) y
⊢ ofQuotientStabilizer α b x = ofQuotientStabilizer α b y
[PROOFSTEP]
convert congr_arg Subtype.val hxy
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x b : β
inst✝² : Fintype α
inst✝¹ : Fintype ↑(orbit α b)
inst✝ : Fintype { x // x ∈ stabilizer α b }
⊢ Fintype.card ↑(orbit α b) * Fintype.card { x // x ∈ stabilizer α b } = Fintype.card α
[PROOFSTEP]
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H
[PROOFSTEP]
simp [QuotientGroup.eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
classical
have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω)) :=
  by
  intro ω
  rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
    Nat.mul_div_cancel]
  exact Fintype.card_pos_iff.mpr (by infer_instance)
simp_rw [this, ← Fintype.card_sigma, Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
have : ∀ ω : Ω, Fintype.card α / Fintype.card (stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω)) :=
  by
  intro ω
  rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
    Nat.mul_div_cancel]
  exact Fintype.card_pos_iff.mpr (by infer_instance)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
⊢ ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
[PROOFSTEP]
intro ω
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
[PROOFSTEP]
rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)), Fintype.card_prod,
  Nat.mul_div_cancel]
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ 0 < Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr (by infer_instance)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁶ inst✝⁵ : Group α
inst✝⁴ : MulAction α β
x : β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype { x // x ∈ stabilizer α b }
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) } = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω : Quotient (orbitRel α β), Fintype.card α / Fintype.card { x // x ∈ stabilizer α (φ ω) }
[PROOFSTEP]
simp_rw [this, ← Fintype.card_sigma, Fintype.card_congr (selfEquivSigmaOrbitsQuotientStabilizer' α β hφ)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁵ inst✝⁴ : Group α
inst✝³ : MulAction α β
x : β
inst✝² : Fintype α
inst✝¹ : (a : α) → Fintype ↑(fixedBy α β a)
inst✝ : Fintype (Quotient (orbitRel α β))
⊢ ∑ a : α, Fintype.card ↑(fixedBy α β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α
[PROOFSTEP]
rw [← Fintype.card_prod, ← Fintype.card_sigma, Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y
[PROOFSTEP]
{ rintro ⟨x⟩ ⟨y⟩
  refine' ⟨y * x⁻¹, QuotientGroup.eq.mpr _⟩
  simp only [smul_eq_mul, H.one_mem, mul_left_inv, inv_mul_cancel_right]
}
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x✝¹ : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ∃ g, g • Quot.mk Setoid.r x = Quot.mk Setoid.r y
[PROOFSTEP]
refine' ⟨y * x⁻¹, QuotientGroup.eq.mpr _⟩
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
inst✝³ inst✝² : Group α
inst✝¹ : MulAction α β
x✝¹ : β
G : Type ?u.117012
inst✝ : Group G
H : Subgroup G
x✝ : G ⧸ H
x : G
y✝ : G ⧸ H
y : G
⊢ ((fun x x_1 => x • x_1) (y * x⁻¹) x)⁻¹ * y ∈ H
[PROOFSTEP]
simp only [smul_eq_mul, H.one_mem, mul_left_inv, inv_mul_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card G / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
classical
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
exact Fintype.card_pos_iff.mpr inferInstance
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card G / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) =
    Fintype.card (ConjAct G) / Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ Fintype.card ↑(carrier (ConjClasses.mk g)) = Fintype.card ↑(MulAction.orbit (ConjAct G) g)
case H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ 0 < Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(carrier (ConjClasses.mk g))
inst✝ : Fintype { x // x ∈ MulAction.stabilizer (ConjAct G) g }
⊢ 0 < Fintype.card { x // x ∈ MulAction.stabilizer (ConjAct G) g }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr inferInstance
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H = MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ normalCore H ≤ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
intro g hg
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
[PROOFSTEP]
apply Equiv.Perm.ext
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
⊢ ∀ (x : G ⧸ H), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) x = ↑1 x
[PROOFSTEP]
refine' fun q ↦ QuotientGroup.induction_on q _
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
⊢ ∀ (z : G), ↑(↑(MulAction.toPermHom G (G ⧸ H)) g) ↑z = ↑1 ↑z
[PROOFSTEP]
refine' fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr _)
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ (g • g')⁻¹ * g' ∈ H
[PROOFSTEP]
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]
[GOAL]
case a.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ normalCore H
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
[PROOFSTEP]
exact H.normalCore.inv_mem hg g'⁻¹
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H)) ≤ normalCore H
[PROOFSTEP]
refine' (Subgroup.normal_le_normalCore.mpr fun g hg => _)
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ g ∈ H
[PROOFSTEP]
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ MonoidHom.ker (MulAction.toPermHom G (G ⧸ H))
⊢ ↑(g * 1) = ↑1
[PROOFSTEP]
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
classical
rcases fintypeOrInfinite G; swap
· rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
simp only [Nat.card_eq_fintype_card]
  -- Porting note: Changed `calc` proof into a `rw` proof.
rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
  sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
    (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g)) fun g ↦
    card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
  MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
congr 1; apply card_congr'; congr; ext; exact (Setoid.comm' _).trans isConj_iff.symm
[GOAL]
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
rcases fintypeOrInfinite G
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
case inr
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
swap
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.fst p.snd } = Nat.card (ConjClasses G) * Nat.card G
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card]
  -- Porting note: Changed `calc` proof into a `rw` proof.
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card { p // Commute p.fst p.snd } = card (ConjClasses G) * card G
[PROOFSTEP]
rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
  sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
    (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g)) fun g ↦
    card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
  MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) = card (ConjClasses G) * card G
[PROOFSTEP]
congr 1
[GOAL]
case inl.e_a
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)
[PROOFSTEP]
apply card_congr'
[GOAL]
case inl.e_a.h
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ Quotient (MulAction.orbitRel (ConjAct G) G) = ConjClasses G
[PROOFSTEP]
congr
[GOAL]
case inl.e_a.h.e_s
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ MulAction.orbitRel (ConjAct G) G = IsConj.setoid G
[PROOFSTEP]
ext
[GOAL]
case inl.e_a.h.e_s.H
α : Type u
β : Type v
γ : Type w
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
a✝ b✝ : G
⊢ Setoid.Rel (MulAction.orbitRel (ConjAct G) G) a✝ b✝ ↔ Setoid.Rel (IsConj.setoid G) a✝ b✝
[PROOFSTEP]
exact (Setoid.comm' _).trans isConj_iff.symm