case intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
case intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
case intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
rw [← Fintype.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
  orderOf_dvd_iff_pow_eq_one]
case intro.mp
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1

case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
case intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
constructor
case intro.mp
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : ∀ (x : Kˣ), x ^ i = 1
⊢ x ^ i = 1
case intro.mp
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
intro h
no goals
case intro.mp
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : ∀ (x : Kˣ), x ^ i = 1
⊢ x ^ i = 1
apply h
case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : x ^ i = 1
y : Kˣ
⊢ y ^ i = 1
case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
intro h y
case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
y : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
⊢ y ^ i = 1
case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
h : x ^ i = 1
y : Kˣ
⊢ y ^ i = 1
simp_rw [← mem_powers_iff_mem_zpowers] at hx
case intro.mpr.intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (fun x x_1 => x ^ x_1) x j ^ i = 1
case intro.mpr
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
y : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
⊢ y ^ i = 1
rcases hx y with ⟨j, rfl⟩
no goals
case intro.mpr.intro
K : Type u_1
R : Type ?u.404549
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), x_1 ∈ Submonoid.powers x
j : ℕ
⊢ (fun x x_1 => x ^ x_1) x j ^ i = 1
rw [← pow_mul, mul_comm, pow_mul, h, one_pow]