[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = -1
[PROOFSTEP]
refine'
  calc
    ((p - 1)! : ZMod p) = ∏ x in Ico 1 (succ (p - 1)), (x : ZMod p) := by
      rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
    _ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := _
    _ = -1 := by
      -- Porting note: `simp` is less powerful.
              -- simp_rw [← Units.coeHom_apply, ← (Units.coeHom (ZMod p)).map_prod,
              --   prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
      simp_rw [← Units.coeHom_apply]
      rw [← (Units.coeHom (ZMod p)).map_prod]
      simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = ∏ x in Ico 1 (succ (p - 1)), ↑x
[PROOFSTEP]
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, ↑x = -1
[PROOFSTEP]
simp_rw [← Units.coeHom_apply]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, ↑(Units.coeHom (ZMod p)) x = -1
[PROOFSTEP]
rw [← (Units.coeHom (ZMod p)).map_prod]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(Units.coeHom (ZMod p)) (∏ x : (ZMod p)ˣ, x) = -1
[PROOFSTEP]
simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 (succ (p - 1)), ↑x = ∏ x : (ZMod p)ˣ, ↑x
[PROOFSTEP]
have hp : 0 < p := (Fact.out (p := p.Prime)).pos
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x in Ico 1 (succ (p - 1)), ↑x = ∏ x : (ZMod p)ˣ, ↑x
[PROOFSTEP]
symm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x : (ZMod p)ˣ, ↑x = ∏ x in Ico 1 (succ (p - 1)), ↑x
[PROOFSTEP]
refine' prod_bij (fun a _ => (a : ZMod p).val) _ _ _ _
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), (fun a x => val ↑a) a ha ∈ Ico 1 (succ (p - 1))
[PROOFSTEP]
intro a ha
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ∈ Ico 1 (succ (p - 1))
[PROOFSTEP]
rw [mem_Ico, ← Nat.succ_sub hp, Nat.succ_sub_one]
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => val ↑a) a ha ∧ (fun a x => val ↑a) a ha < p
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => val ↑a) a ha
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ≠ 0
[PROOFSTEP]
rw [← @val_zero p]
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ≠ val 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (fun a x => val ↑a) a ha = val 0
⊢ False
[PROOFSTEP]
apply Units.ne_zero a (val_injective p h)
[GOAL]
case refine'_1.right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha < p
[PROOFSTEP]
exact val_lt _
[GOAL]
case refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), ↑a = ↑((fun a x => val ↑a) a ha)
[PROOFSTEP]
rintro a -
[GOAL]
case refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha✝ : a ∈ univ
⊢ ↑a = ↑((fun a x => val ↑a) a ha✝)
[PROOFSTEP]
simp only [cast_id, nat_cast_val]
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a₁ a₂ : (ZMod p)ˣ) (ha₁ : a₁ ∈ univ) (ha₂ : a₂ ∈ univ),
    (fun a x => val ↑a) a₁ ha₁ = (fun a x => val ↑a) a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
intro _ _ _ _ h
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ a₂✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => val ↑a) a₁✝ ha₁✝ = (fun a x => val ↑a) a₂✝ ha₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
rw [Units.ext_iff]
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ a₂✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => val ↑a) a₁✝ ha₁✝ = (fun a x => val ↑a) a₂✝ ha₂✝
⊢ ↑a₁✝ = ↑a₂✝
[PROOFSTEP]
exact val_injective p h
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (b : ℕ), b ∈ Ico 1 (succ (p - 1)) → ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
intro b hb
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (succ (p - 1))
⊢ ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, succ_sub_one, pos_iff_ne_zero] at hb
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
refine' ⟨Units.mk0 b _, Finset.mem_univ _, _⟩
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ False
[PROOFSTEP]
apply hb.1
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ b = 0
[PROOFSTEP]
apply_fun val at h
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : val ↑b = val 0
⊢ b = 0
[PROOFSTEP]
simpa only [val_cast_of_lt hb.right, val_zero] using h
[GOAL]
case refine'_4.refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ b = (fun a x => val ↑a) (Units.mk0 ↑b (_ : ↑b = 0 → False)) (_ : Units.mk0 ↑b (_ : ↑b = 0 → False) ∈ univ)
[PROOFSTEP]
simp only [val_cast_of_lt hb.right, Units.val_mk0]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
conv =>
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
congr
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x
case a p : ℕ inst✝ : Fact (Nat.Prime p) | -1
[PROOFSTEP]
congr
[GOAL]
case a.s
p : ℕ
inst✝ : Fact (Nat.Prime p)
| Ico 1 p
case a.f
p : ℕ
inst✝ : Fact (Nat.Prime p)
| fun x => ↑x
case a p : ℕ inst✝ : Fact (Nat.Prime p) | -1
[PROOFSTEP]
rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 (succ (p - succ 0)), ↑x = -1
[PROOFSTEP]
rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]
[GOAL]
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
⊢ Prime n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | h0)
[GOAL]
case inl
h : ↑(0 - 1)! = -1
h1 : 0 ≠ 1
⊢ Prime 0
[PROOFSTEP]
norm_num at h
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
h0 : n ≠ 0
⊢ Prime n
[PROOFSTEP]
replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n
[PROOFSTEP]
by_contra h2
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False
[PROOFSTEP]
obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False
[PROOFSTEP]
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False
[PROOFSTEP]
refine' hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans _)))
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ n ∣ (n - 1)! + 1
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd, cast_add, cast_one, h, add_left_neg]
[GOAL]
n : ℕ
h : n ≠ 1
⊢ Prime n ↔ ↑(n - 1)! = -1
[PROOFSTEP]
refine' ⟨fun h1 => _, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
[GOAL]
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ ↑(n - 1)! = -1
[PROOFSTEP]
haveI := Fact.mk h1
[GOAL]
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ ↑(n - 1)! = -1
[PROOFSTEP]
exact ZMod.wilsons_lemma n


[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Subsingleton α
x : α
⊢ x ∈ zpowers 1
[PROOFSTEP]
rw [Subsingleton.elim x 1]
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Subsingleton α
x : α
⊢ 1 ∈ zpowers 1
[PROOFSTEP]
exact mem_zpowers 1
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
[PROOFSTEP]
obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
[GOAL]
case intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
[PROOFSTEP]
obtain ⟨m, hm⟩ := hG (σ h)
[GOAL]
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
⊢ ∃ m, ∀ (g : G), ↑σ g = g ^ m
[PROOFSTEP]
refine' ⟨m, fun g => _⟩
[GOAL]
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
g : G
⊢ ↑σ g = g ^ m
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hG g
[GOAL]
case intro.intro.intro
α : Type u
a : α
inst✝¹ : Group α
G : Type u_1
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x x_1 => x ^ x_1) h m = ↑σ h
n : ℤ
⊢ ↑σ ((fun x x_1 => x ^ x_1) h n) = (fun x x_1 => x ^ x_1) h n ^ m
[PROOFSTEP]
rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ IsCyclic α
[PROOFSTEP]
classical
use x
simp_rw [← SetLike.mem_coe, ← Set.eq_univ_iff_forall]
rw [← Fintype.card_congr (Equiv.Set.univ α), orderOf_eq_card_zpowers] at hx
exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ IsCyclic α
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ∀ (x_1 : α), x_1 ∈ zpowers x
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, ← Set.eq_univ_iff_forall]
[GOAL]
case h
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx : orderOf x = Fintype.card α
⊢ ↑(zpowers x) = Set.univ
[PROOFSTEP]
rw [← Fintype.card_congr (Equiv.Set.univ α), orderOf_eq_card_zpowers] at hx
[GOAL]
case h
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
x : α
hx✝ : orderOf x = Fintype.card ↑Set.univ
hx : Fintype.card { x_1 // x_1 ∈ zpowers x } = Fintype.card ↑Set.univ
⊢ ↑(zpowers x) = Set.univ
[PROOFSTEP]
exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := Fintype.exists_ne_of_one_lt_card (h.symm ▸ hp.1.one_lt) 1
[GOAL]
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
classical
  -- for Fintype (Subgroup.zpowers g)
have : Fintype.card (Subgroup.zpowers g) ∣ p := by
  rw [← h]
  apply card_subgroup_dvd_card
rw [Nat.dvd_prime hp.1] at this
cases' this with that that
· rw [Fintype.card_eq_one_iff] at that
  cases' that with t ht
  suffices g = 1 by contradiction
  have hgt :=
    ht
      ⟨g, by
        change g ∈ Subgroup.zpowers g
        exact Subgroup.mem_zpowers g⟩
  rw [← ht 1] at hgt
  change (⟨_, _⟩ : Subgroup.zpowers g) = ⟨_, _⟩ at hgt
  simpa using hgt
· use g
  intro x
  rw [← h] at that
  rw [Subgroup.eq_top_of_card_eq _ that]
  exact Subgroup.mem_top _
[GOAL]
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
have : Fintype.card (Subgroup.zpowers g) ∣ p := by
  rw [← h]
  apply card_subgroup_dvd_card
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ Fintype.card { x // x ∈ zpowers g } ∣ p
[PROOFSTEP]
rw [← h]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
⊢ Fintype.card { x // x ∈ zpowers g } ∣ Fintype.card α
[PROOFSTEP]
apply card_subgroup_dvd_card
[GOAL]
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } ∣ p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
rw [Nat.dvd_prime hp.1] at this
[GOAL]
case intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
this : Fintype.card { x // x ∈ zpowers g } = 1 ∨ Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
cases' this with that that
[GOAL]
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
rw [Fintype.card_eq_one_iff] at that
[GOAL]
case intro.inl
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : ∃ x, ∀ (y : { x // x ∈ zpowers g }), y = x
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
cases' that with t ht
[GOAL]
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
suffices g = 1 by contradiction
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
this : g = 1
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
contradiction
[GOAL]
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g = 1
[PROOFSTEP]
have hgt :=
  ht
    ⟨g, by
      change g ∈ Subgroup.zpowers g
      exact Subgroup.mem_zpowers g⟩
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g ∈ zpowers g
[PROOFSTEP]
change g ∈ Subgroup.zpowers g
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
⊢ g ∈ zpowers g
[PROOFSTEP]
exact Subgroup.mem_zpowers g
[GOAL]
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = t
⊢ g = 1
[PROOFSTEP]
rw [← ht 1] at hgt
[GOAL]
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = 1
⊢ g = 1
[PROOFSTEP]
change (⟨_, _⟩ : Subgroup.zpowers g) = ⟨_, _⟩ at hgt
[GOAL]
case intro.inl.intro
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
t : { x // x ∈ zpowers g }
ht : ∀ (y : { x // x ∈ zpowers g }), y = t
hgt : { val := g, property := (_ : g ∈ zpowers g) } = { val := 1, property := (_ : 1 ∈ (zpowers g).toSubmonoid) }
⊢ g = 1
[PROOFSTEP]
simpa using hgt
[GOAL]
case intro.inr
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∃ g, ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
use g
[GOAL]
case h
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
⊢ ∀ (x : α), x ∈ zpowers g
[PROOFSTEP]
intro x
[GOAL]
case h
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = p
x : α
⊢ x ∈ zpowers g
[PROOFSTEP]
rw [← h] at that
[GOAL]
case h
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ zpowers g
[PROOFSTEP]
rw [Subgroup.eq_top_of_card_eq _ that]
[GOAL]
case h
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
g : α
hg : g ≠ 1
that : Fintype.card { x // x ∈ zpowers g } = Fintype.card α
x : α
⊢ x ∈ ⊤
[PROOFSTEP]
exact Subgroup.mem_top _
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Fintype.card α
[PROOFSTEP]
classical
rw [orderOf_eq_card_zpowers]
apply Fintype.card_of_finset'
simpa using hx
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Fintype.card α
[PROOFSTEP]
rw [orderOf_eq_card_zpowers]
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ Fintype.card { x // x ∈ zpowers g } = Fintype.card α
[PROOFSTEP]
apply Fintype.card_of_finset'
[GOAL]
case H
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Fintype α
g : α
hx : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (x : α), x ∈ Finset.univ ↔ x ∈ ↑(zpowers g)
[PROOFSTEP]
simpa using hx
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0
[PROOFSTEP]
classical
rw [orderOf_eq_zero_iff']
refine' fun n hn hgn => _
have ho := orderOf_pos' ((isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, hn, hgn⟩)
obtain ⟨x, hx⟩ := Infinite.exists_not_mem_finset (Finset.image (fun x => g ^ x) <| Finset.range <| orderOf g)
apply hx
rw [← mem_powers_iff_mem_range_order_of' (x := g) (y := x) ho, Submonoid.mem_powers_iff]
obtain ⟨k, hk⟩ := h x
dsimp at hk
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
· exact ⟨k, by exact_mod_cast hk⟩
rw [zpow_eq_mod_orderOf] at hk
have : 0 ≤ (-k % orderOf g : ℤ) := Int.emod_nonneg (-k) (by exact_mod_cast ho.ne')
refine' ⟨(-k % orderOf g : ℤ).toNat, _⟩
rwa [← zpow_ofNat, Int.toNat_of_nonneg this]
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = 0
[PROOFSTEP]
rw [orderOf_eq_zero_iff']
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
⊢ ∀ (n : ℕ), 0 < n → g ^ n ≠ 1
[PROOFSTEP]
refine' fun n hn hgn => _
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
⊢ False
[PROOFSTEP]
have ho := orderOf_pos' ((isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, hn, hgn⟩)
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
⊢ False
[PROOFSTEP]
obtain ⟨x, hx⟩ := Infinite.exists_not_mem_finset (Finset.image (fun x => g ^ x) <| Finset.range <| orderOf g)
[GOAL]
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
[PROOFSTEP]
rw [← mem_powers_iff_mem_range_order_of' (x := g) (y := x) ho, Submonoid.mem_powers_iff]
[GOAL]
case intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
obtain ⟨k, hk⟩ := h x
[GOAL]
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : (fun x x_1 => x ^ x_1) g k = x
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
dsimp at hk
[GOAL]
case intro.intro
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℤ
hk : g ^ k = x
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
obtain ⟨k, rfl | rfl⟩ := k.eq_nat_or_neg
[GOAL]
case intro.intro.intro.inl
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ ↑k = x
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
exact ⟨k, by exact_mod_cast hk⟩
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ ↑k = x
⊢ g ^ k = x
[PROOFSTEP]
exact_mod_cast hk
[GOAL]
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k) = x
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
rw [zpow_eq_mod_orderOf] at hk
[GOAL]
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
have : 0 ≤ (-k % orderOf g : ℤ) := Int.emod_nonneg (-k) (by exact_mod_cast ho.ne')
[GOAL]
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
⊢ ↑(orderOf g) ≠ 0
[PROOFSTEP]
exact_mod_cast ho.ne'
[GOAL]
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ ∃ n, g ^ n = x
[PROOFSTEP]
refine' ⟨(-k % orderOf g : ℤ).toNat, _⟩
[GOAL]
case intro.intro.intro.inr
α : Type u
a : α
inst✝¹ : Group α
inst✝ : Infinite α
g : α
h : ∀ (x : α), x ∈ zpowers g
n : ℕ
hn : 0 < n
hgn : g ^ n = 1
ho : 0 < orderOf g
x : α
hx : ¬x ∈ Finset.image (fun x => g ^ x) (Finset.range (orderOf g))
k : ℕ
hk : g ^ (-↑k % ↑(orderOf g)) = x
this : 0 ≤ -↑k % ↑(orderOf g)
⊢ g ^ Int.toNat (-↑k % ↑(orderOf g)) = x
[PROOFSTEP]
rwa [← zpow_ofNat, Int.toNat_of_nonneg this]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
h : Int.natAbs k = 0
⊢ x = 1
[PROOFSTEP]
rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
⊢ g ^ Int.natAbs k ∈ H
[PROOFSTEP]
cases' k with k k
[GOAL]
case ofNat
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x x_1 => x ^ x_1) g (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ g ^ Int.natAbs (Int.ofNat k) ∈ H
[PROOFSTEP]
rw [Int.ofNat_eq_coe, Int.natAbs_cast k, ← zpow_ofNat, ← Int.ofNat_eq_coe, hk]
[GOAL]
case ofNat
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x x_1 => x ^ x_1) g (Int.ofNat k) = x
hk : g ^ Int.ofNat k = x
⊢ x ∈ H
[PROOFSTEP]
exact hx₁
[GOAL]
case negSucc
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x x_1 => x ^ x_1) g (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ g ^ Int.natAbs (Int.negSucc k) ∈ H
[PROOFSTEP]
rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]
[GOAL]
case negSucc
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x, x ∈ H ∧ x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x x_1 => x ^ x_1) g (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ (g ^ Nat.succ k)⁻¹ ∈ H
[PROOFSTEP]
simp_all
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
[PROOFSTEP]
rw [zpow_mul]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
⊢ (g ^ ↑(Nat.find hex)) ^ (k / ↑(Nat.find hex)) ∈ H
[PROOFSTEP]
apply H.zpow_mem
[GOAL]
case hx
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
⊢ g ^ ↑(Nat.find hex) ∈ H
[PROOFSTEP]
exact_mod_cast (Nat.find_spec hex).2
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ g ^ (k % ↑(Nat.find hex)) * g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
[PROOFSTEP]
rw [← zpow_add, Int.emod_add_ediv, hk]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ x ∈ H
[PROOFSTEP]
exact hx
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
⊢ k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
[PROOFSTEP]
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ (Int.coe_nat_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
⊢ g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
[PROOFSTEP]
rwa [← zpow_ofNat, ← hk₄]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
hk₅ : g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
h : ¬Int.natAbs (k % ↑(Nat.find hex)) = 0
⊢ ↑(Int.natAbs (k % ↑(Nat.find hex))) < ↑(Nat.find hex)
[PROOFSTEP]
rw [← hk₄]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
hk₅ : g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
h : ¬Int.natAbs (k % ↑(Nat.find hex)) = 0
⊢ k % ↑(Nat.find hex) < ↑(Nat.find hex)
[PROOFSTEP]
exact Int.emod_lt_of_pos _ (Int.coe_nat_pos.2 (Nat.find_spec hex).1)
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
hk₅ : g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
hk₆ : Int.natAbs (k % ↑(Nat.find hex)) = 0
⊢ ↑((fun x x_1 => x ^ x_1) { val := g ^ Nat.find hex, property := (_ : g ^ Nat.find hex ∈ H) } (k / ↑(Nat.find hex))) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this✝ : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
hk₅ : g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
hk₆ : Int.natAbs (k % ↑(Nat.find hex)) = 0
this : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x
⊢ ↑((fun x x_1 => x ^ x_1) { val := g ^ Nat.find hex, property := (_ : g ^ Nat.find hex ∈ H) } (k / ↑(Nat.find hex))) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
simpa [zpow_mul]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x, x ∈ H ∧ x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x x_1 => x ^ x_1) g k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : { x // x ∈ H }
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x x_1 => x ^ x_1) g k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(Int.natAbs (k % ↑(Nat.find hex)))
hk₅ : g ^ Int.natAbs (k % ↑(Nat.find hex)) ∈ H
hk₆ : Int.natAbs (k % ↑(Nat.find hex)) = 0
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x
[PROOFSTEP]
rw [Int.mul_ediv_cancel' (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)), hk]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ H ∧ x ≠ 1
⊢ IsCyclic { x // x ∈ H }
[PROOFSTEP]
have : H = (⊥ : Subgroup α) :=
  Subgroup.ext fun x => ⟨fun h => by simp at *; tauto, fun h => by rw [Subgroup.mem_bot.1 h]; exact H.one_mem⟩
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ H ∧ x ≠ 1
x : α
h : x ∈ H
⊢ x ∈ ⊥
[PROOFSTEP]
simp at *
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
h : x ∈ H
hx : ∀ (x : α), x ∈ H → x = 1
⊢ x = 1
[PROOFSTEP]
tauto
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ H ∧ x ≠ 1
x : α
h : x ∈ ⊥
⊢ x ∈ H
[PROOFSTEP]
rw [Subgroup.mem_bot.1 h]
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ H ∧ x ≠ 1
x : α
h : x ∈ ⊥
⊢ 1 ∈ H
[PROOFSTEP]
exact H.one_mem
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
H : Subgroup α
this✝ : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ H ∧ x ≠ 1
this : H = ⊥
⊢ IsCyclic { x // x ∈ H }
[PROOFSTEP]
subst this
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : IsCyclic α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ¬∃ x, x ∈ ⊥ ∧ x ≠ 1
⊢ IsCyclic { x // x ∈ ⊥ }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : (fun x x_1 => x ^ x_1) g m = x
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
[PROOFSTEP]
dsimp at hm
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
[PROOFSTEP]
have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1 := by rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff];
  exact (mem_filter.1 hx).2
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ g ^ (m * Nat.gcd n (Fintype.card α)) = 1
[PROOFSTEP]
rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
⊢ x ^ n = 1
[PROOFSTEP]
exact (mem_filter.1 hx).2
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (fun x x_1 => x ^ x_1) (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α)))
      ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) =
    x
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) ^ ↑(m / (Fintype.card α / Nat.gcd n (Fintype.card α))) = x
[PROOFSTEP]
rw [zpow_ofNat, ← pow_mul, Nat.mul_div_cancel_left', hm]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) ∣ m
[PROOFSTEP]
refine' Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) _
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α) ∣ m * Nat.gcd n (Fintype.card α)
[PROOFSTEP]
conv_lhs => rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
| Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α)
[PROOFSTEP]
rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
| Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α)
[PROOFSTEP]
rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
| Fintype.card α / Nat.gcd n (Fintype.card α) * Nat.gcd n (Fintype.card α)
[PROOFSTEP]
rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ filter (fun a => a ^ n = 1) univ
m : ℕ
hm : g ^ m = x
hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1
⊢ orderOf g ∣ m * Nat.gcd n (Fintype.card α)
[PROOFSTEP]
exact orderOf_dvd_of_pow_eq_one hgmn
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
[PROOFSTEP]
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
[PROOFSTEP]
have hm0 : 0 < m :=
  Nat.pos_of_ne_zero fun hm0 => by
    rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
    exact hm.elim' 1
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : m = 0
⊢ False
[PROOFSTEP]
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : IsEmpty α
hm0 : m = 0
⊢ False
[PROOFSTEP]
exact hm.elim' 1
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ card (Set.toFinset ↑(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))))) ≤ n
[PROOFSTEP]
simp only [Set.toFinset_card, SetLike.coe_sort_coe]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card { x // x ∈ zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) } ≤ n
[PROOFSTEP]
rw [← orderOf_eq_card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Fintype.card α) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
[PROOFSTEP]
nth_rw 2 [hm]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Fintype.card α / Nat.gcd n (Fintype.card α)) ≤ n
[PROOFSTEP]
nth_rw 3 [hm]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α /
      Nat.gcd (Nat.gcd n (Fintype.card α) * m) (Nat.gcd n (Fintype.card α) * m / Nat.gcd n (Fintype.card α)) ≤
    n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm, Nat.mul_div_cancel _ hm0]
[GOAL]
α : Type u
a : α
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m
hm0 : 0 < m
⊢ Nat.gcd n (Fintype.card α) ≤ n
[PROOFSTEP]
exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ Submonoid.powers x
[PROOFSTEP]
simp_rw [mem_powers_iff_mem_zpowers]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x
[PROOFSTEP]
exact IsCyclic.exists_generator
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i => a ^ i) (range (orderOf a)) = univ
[PROOFSTEP]
simp_rw [← SetLike.mem_coe] at ha
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ ↑(zpowers a)
⊢ image (fun i => a ^ i) (range (orderOf a)) = univ
[PROOFSTEP]
simp only [_root_.image_range_orderOf, Set.eq_univ_iff_forall.mpr ha, Set.toFinset_univ]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i => a ^ i) (range (Fintype.card α)) = univ
[PROOFSTEP]
rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : { x // x ∈ zpowers a }
⊢ ↑b ^ orderOf a = 1
[PROOFSTEP]
let ⟨i, hi⟩ := b.2
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : { x // x ∈ zpowers a }
i : ℤ
hi : (fun x x_1 => x ^ x_1) a i = ↑b
⊢ ↑b ^ orderOf a = 1
[PROOFSTEP]
rw [← hi, ← zpow_ofNat, ← zpow_mul, mul_comm, zpow_mul, zpow_ofNat, pow_orderOf_eq_one, one_zpow]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ ∀ {d : ℕ},
    d ∣ Fintype.card α →
      0 < card (filter (fun a => orderOf a = d) univ) → card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
intro d hd hpos
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
induction' d using Nat.strongRec' with d IH
[GOAL]
case H
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
rcases Decidable.eq_or_ne d 0 with (rfl | hd0)
[GOAL]
case H.inl
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd✝ : d ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d) univ)
IH :
  ∀ (m : ℕ),
    m < 0 →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = 0) univ)
⊢ card (filter (fun a => orderOf a = 0) univ) = φ 0
[PROOFSTEP]
cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)
[GOAL]
case H.inr
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
rcases card_pos.1 hpos with ⟨a, ha'⟩
[GOAL]
case H.inr.intro
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
have ha : orderOf a = d := (mem_filter.1 ha').2
[GOAL]
case H.inr.intro
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
have h1 : (∑ m in d.properDivisors, (univ.filter fun a : α => orderOf a = m).card) = ∑ m in d.properDivisors, φ m :=
  by
  refine' Finset.sum_congr rfl fun m hm => _
  simp only [mem_filter, mem_range, mem_properDivisors] at hm
  refine' IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), _⟩)
  simp only [mem_filter, mem_univ, orderOf_pow a, ha, true_and_iff, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
    Nat.div_div_self hm.1 hd0]
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
⊢ ∑ m in properDivisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in properDivisors d, φ m
[PROOFSTEP]
refine' Finset.sum_congr rfl fun m hm => _
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
m : ℕ
hm : m ∈ properDivisors d
⊢ card (filter (fun a => orderOf a = m) univ) = φ m
[PROOFSTEP]
simp only [mem_filter, mem_range, mem_properDivisors] at hm
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ card (filter (fun a => orderOf a = m) univ) = φ m
[PROOFSTEP]
refine' IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), _⟩)
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ a ^ (d / m) ∈ filter (fun a => orderOf a = m) univ
[PROOFSTEP]
simp only [mem_filter, mem_univ, orderOf_pow a, ha, true_and_iff, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
  Nat.div_div_self hm.1 hd0]
[GOAL]
case H.inr.intro
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m in properDivisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in properDivisors d, φ m
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
have h2 : (∑ m in d.divisors, (univ.filter fun a : α => orderOf a = m).card) = ∑ m in d.divisors, φ m := by
  rw [← filter_dvd_eq_divisors hd0, sum_card_orderOf_eq_card_pow_eq_one hd0, filter_dvd_eq_divisors hd0, sum_totient, ←
    ha, card_pow_eq_one_eq_orderOf_aux hn a]
[GOAL]
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m in properDivisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in properDivisors d, φ m
⊢ ∑ m in divisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in divisors d, φ m
[PROOFSTEP]
rw [← filter_dvd_eq_divisors hd0, sum_card_orderOf_eq_card_pow_eq_one hd0, filter_dvd_eq_divisors hd0, sum_totient, ←
  ha, card_pow_eq_one_eq_orderOf_aux hn a]
[GOAL]
case H.inr.intro
α : Type u
a✝ : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d✝ : ℕ
hd✝ : d✝ ∣ Fintype.card α
hpos✝ : 0 < card (filter (fun a => orderOf a = d✝) univ)
d : ℕ
IH :
  ∀ (m : ℕ),
    m < d →
      m ∣ Fintype.card α →
        0 < card (filter (fun a => orderOf a = m) univ) → card (filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card (filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m in properDivisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in properDivisors d, φ m
h2 : ∑ m in divisors d, card (filter (fun a => orderOf a = m) univ) = ∑ m in divisors d, φ m
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
simpa [← cons_self_properDivisors hd0, ← h1] using h2
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
let c := Fintype.card α
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
apply card_orderOf_eq_totient_aux₁ hn hd
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ 0 < card (filter (fun a => orderOf a = d) univ)
[PROOFSTEP]
by_contra h0
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < card (filter (fun a => orderOf a = d) univ)
⊢ False
[PROOFSTEP]
simp only [not_lt, _root_.le_zero_iff, card_eq_zero] at h0
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ False
[PROOFSTEP]
apply lt_irrefl c
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c < c
[PROOFSTEP]
calc
  c = ∑ m in c.divisors, (univ.filter fun a : α => orderOf a = m).card :=
    by
    simp only [← filter_dvd_eq_divisors hc0.ne', sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
    apply congr_arg card
    simp
  _ = ∑ m in c.divisors.erase d, (univ.filter fun a : α => orderOf a = m).card :=
    by
    rw [eq_comm]
    refine' sum_subset (erase_subset _ _) fun m hm₁ hm₂ => _
    have : m = d := by
      contrapose! hm₂
      exact mem_erase_of_ne_of_mem hm₂ hm₁
    simp [this, h0]
  _ ≤ ∑ m in c.divisors.erase d, φ m := by
    refine' sum_le_sum fun m hm => _
    have hmc : m ∣ c := by
      simp only [mem_erase, mem_divisors] at hm
      tauto
    rcases(filter (fun a : α => orderOf a = m) univ).card.eq_zero_or_pos with (h1 | h1)
    · simp [h1]
    · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
  _ < ∑ m in c.divisors, φ m :=
    (sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos (pos_of_dvd_of_pos hd hc0)))
  _ = c := sum_totient _
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c = ∑ m in divisors c, card (filter (fun a => orderOf a = m) univ)
[PROOFSTEP]
simp only [← filter_dvd_eq_divisors hc0.ne', sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ Fintype.card α = card (filter (fun x => x ^ Fintype.card α = 1) univ)
[PROOFSTEP]
apply congr_arg card
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ univ = filter (fun x => x ^ Fintype.card α = 1) univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m in divisors c, card (filter (fun a => orderOf a = m) univ) =
    ∑ m in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ)
[PROOFSTEP]
rw [eq_comm]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ) =
    ∑ m in divisors c, card (filter (fun a => orderOf a = m) univ)
[PROOFSTEP]
refine' sum_subset (erase_subset _ _) fun m hm₁ hm₂ => _
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm₁ : m ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
[PROOFSTEP]
have : m = d := by
  contrapose! hm₂
  exact mem_erase_of_ne_of_mem hm₂ hm₁
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm₁ : m ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
⊢ m = d
[PROOFSTEP]
contrapose! hm₂
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm₁ : m ∈ divisors c
hm₂ : m ≠ d
⊢ m ∈ erase (divisors (Fintype.card α)) d
[PROOFSTEP]
exact mem_erase_of_ne_of_mem hm₂ hm₁
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm₁ : m ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
this : m = d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
[PROOFSTEP]
simp [this, h0]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ) ≤ ∑ m in erase (divisors c) d, φ m
[PROOFSTEP]
refine' sum_le_sum fun m hm => _
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
[PROOFSTEP]
have hmc : m ∣ c := by
  simp only [mem_erase, mem_divisors] at hm
  tauto
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ erase (divisors c) d
⊢ m ∣ c
[PROOFSTEP]
simp only [mem_erase, mem_divisors] at hm
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ≠ d ∧ m ∣ Fintype.card α ∧ Fintype.card α ≠ 0
⊢ m ∣ c
[PROOFSTEP]
tauto
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ erase (divisors c) d
hmc : m ∣ c
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
[PROOFSTEP]
rcases(filter (fun a : α => orderOf a = m) univ).card.eq_zero_or_pos with (h1 | h1)
[GOAL]
case inl
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) = 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
[PROOFSTEP]
simp [h1]
[GOAL]
case inr
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) > 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
[PROOFSTEP]
simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < card (filter (fun a => orderOf a = Fintype.card α) univ)
[PROOFSTEP]
rw [card_orderOf_eq_totient_aux₂ hn dvd_rfl]
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < φ (Fintype.card α)
[PROOFSTEP]
exact totient_pos (Fintype.card_pos_iff.2 ⟨1⟩)
[GOAL]
α✝ : Type u
a : α✝
inst✝⁵ : Group α✝
inst✝⁴ : DecidableEq α✝
inst✝³ : Fintype α✝
hn✝ : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => n • a = 0) univ) ≤ n
⊢ IsAddCyclic α
[PROOFSTEP]
obtain ⟨g, hg⟩ := (@isCyclic_of_card_pow_eq_one_le (Multiplicative α) _ _ (_) hn)
[GOAL]
case mk.intro
α✝ : Type u
a : α✝
inst✝⁵ : Group α✝
inst✝⁴ : DecidableEq α✝
inst✝³ : Fintype α✝
hn✝ : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => n • a = 0) univ) ≤ n
g : Multiplicative α
hg : ∀ (x : Multiplicative α), x ∈ zpowers g
⊢ IsAddCyclic α
[PROOFSTEP]
exact ⟨⟨g, hg⟩⟩
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
[PROOFSTEP]
apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd
[GOAL]
α✝ : Type u
a : α✝
inst✝³ : Group α✝
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : IsAddCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => addOrderOf a = d) univ) = φ d
[PROOFSTEP]
obtain ⟨g, hg⟩ := id ‹IsAddCyclic α›
[GOAL]
case mk.intro
α✝ : Type u
a : α✝
inst✝³ : Group α✝
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : IsAddCyclic α
inst✝ : Fintype α
d : ℕ
hd : d ∣ Fintype.card α
g : α
hg : ∀ (x : α), x ∈ AddSubgroup.zmultiples g
⊢ card (filter (fun a => addOrderOf a = d) univ) = φ d
[PROOFSTEP]
apply @IsCyclic.card_orderOf_eq_totient (Multiplicative α) _ ⟨⟨g, hg⟩⟩ (_) _ hd
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
⊢ Nontrivial α
[PROOFSTEP]
have h' := Nat.Prime.one_lt (Fact.out (p := p.Prime))
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < p
⊢ Nontrivial α
[PROOFSTEP]
rw [← h] at h'
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
h' : 1 < Fintype.card α
⊢ Nontrivial α
[PROOFSTEP]
exact Fintype.one_lt_card_iff_nontrivial.1 h'
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
classical
have hcard := card_subgroup_dvd_card H
rw [h, dvd_prime (Fact.out (p := p.Prime))] at hcard
refine' hcard.imp (fun h1 => _) fun hp => _
· haveI := Fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1)
  apply eq_bot_of_subsingleton
· exact eq_top_of_card_eq _ (hp.trans h.symm)
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
have hcard := card_subgroup_dvd_card H
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } ∣ Fintype.card α
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
rw [h, dvd_prime (Fact.out (p := p.Prime))] at hcard
[GOAL]
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
refine' hcard.imp (fun h1 => _) fun hp => _
[GOAL]
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
⊢ H = ⊥
[PROOFSTEP]
haveI := Fintype.card_le_one_iff_subsingleton.1 (le_of_eq h1)
[GOAL]
case refine'_1
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card α = p
this✝ : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
h1 : Fintype.card { x // x ∈ H } = 1
this : Subsingleton { x // x ∈ H }
⊢ H = ⊥
[PROOFSTEP]
apply eq_bot_of_subsingleton
[GOAL]
case refine'_2
α✝ : Type u
a : α✝
inst✝² : Group α✝
α : Type u
inst✝¹ : Group α
inst✝ : Fintype α
p : ℕ
hp✝ : Fact (Nat.Prime p)
h : Fintype.card α = p
this : Nontrivial α
H : Subgroup α
x✝ : Normal H
hcard : Fintype.card { x // x ∈ H } = 1 ∨ Fintype.card { x // x ∈ H } = p
hp : Fintype.card { x // x ∈ H } = p
⊢ H = ⊤
[PROOFSTEP]
exact eq_top_of_card_eq _ (hp.trans h.symm)
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
⊢ x ^ m = ↑f a
[PROOFSTEP]
simpa [Subtype.ext_iff] using hm
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
⊢ x ^ n = ↑f b
[PROOFSTEP]
simpa [Subtype.ext_iff] using hn
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
⊢ y ^ (-m) * a ∈ MonoidHom.ker f
[PROOFSTEP]
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_self]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
⊢ y ^ (-n) * b ∈ MonoidHom.ker f
[PROOFSTEP]
rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_self]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b)
[PROOFSTEP]
rw [mem_center_iff.1 ha]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b))
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a)
[PROOFSTEP]
rw [mem_center_iff.1 hb]
[GOAL]
α : Type u
a✝ : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
a b : G
x : H
y : G
hxy : ↑f y = x
hx : ∀ (a : { x // x ∈ MonoidHom.range f }), a ∈ zpowers { val := x, property := (_ : ∃ y, ↑f y = x) }
m : ℤ
hm✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } m =
    { val := ↑f a, property := (_ : ∃ y, ↑f y = ↑f a) }
n : ℤ
hn✝ :
  (fun x x_1 => x ^ x_1) { val := x, property := (_ : ∃ y, ↑f y = x) } n =
    { val := ↑f b, property := (_ : ∃ y, ↑f y = ↑f b) }
hm : x ^ m = ↑f a
hn : x ^ n = ↑f b
ha : y ^ (-m) * a ∈ center G
hb : y ^ (-n) * b ∈ center G
⊢ y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) = b * a
[PROOFSTEP]
group
[GOAL]
α : Type u
a : α
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
inst✝ : IsCyclic H
f : G →* H
hf : MonoidHom.ker f ≤ center G
⊢ Group G
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ IsCyclic α
[PROOFSTEP]
cases' subsingleton_or_nontrivial α with hi hi
[GOAL]
case inl
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi : Subsingleton α
⊢ IsCyclic α
[PROOFSTEP]
haveI := hi
[GOAL]
case inr
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi : Nontrivial α
⊢ IsCyclic α
[PROOFSTEP]
haveI := hi
[GOAL]
case inl
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Subsingleton α
⊢ IsCyclic α
[PROOFSTEP]
apply isCyclic_of_subsingleton
[GOAL]
case inr
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
⊢ IsCyclic α
[PROOFSTEP]
obtain ⟨g, hg⟩ := exists_ne (1 : α)
[GOAL]
case inr.intro
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
⊢ IsCyclic α
[PROOFSTEP]
refine' ⟨⟨g, fun x => _⟩⟩
[GOAL]
case inr.intro
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
⊢ x ∈ Subgroup.zpowers g
[PROOFSTEP]
cases' IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers g) with hb ht
[GOAL]
case inr.intro.inl
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
hb : Subgroup.zpowers g = ⊥
⊢ x ∈ Subgroup.zpowers g
[PROOFSTEP]
exfalso
[GOAL]
case inr.intro.inl.h
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
hb : Subgroup.zpowers g = ⊥
⊢ False
[PROOFSTEP]
apply hg
[GOAL]
case inr.intro.inl.h
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
hb : Subgroup.zpowers g = ⊥
⊢ g = 1
[PROOFSTEP]
rw [← Subgroup.mem_bot, ← hb]
[GOAL]
case inr.intro.inl.h
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
hb : Subgroup.zpowers g = ⊥
⊢ g ∈ Subgroup.zpowers g
[PROOFSTEP]
apply Subgroup.mem_zpowers
[GOAL]
case inr.intro.inr
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
ht : Subgroup.zpowers g = ⊤
⊢ x ∈ Subgroup.zpowers g
[PROOFSTEP]
rw [ht]
[GOAL]
case inr.intro.inr
α : Type u
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
hi this : Nontrivial α
g : α
hg : g ≠ 1
x : α
ht : Subgroup.zpowers g = ⊤
⊢ x ∈ ⊤
[PROOFSTEP]
apply Subgroup.mem_top
[GOAL]
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
⊢ Nat.Prime (Fintype.card α)
[PROOFSTEP]
have h0 : 0 < Fintype.card α := Fintype.card_pos_iff.2 (by infer_instance)
[GOAL]
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
⊢ Nonempty α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
⊢ Nat.Prime (Fintype.card α)
[PROOFSTEP]
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
[GOAL]
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Nat.Prime (Fintype.card α)
[PROOFSTEP]
rw [Nat.prime_def_lt'']
[GOAL]
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ 2 ≤ Fintype.card α ∧ ∀ (m : ℕ), m ∣ Fintype.card α → m = 1 ∨ m = Fintype.card α
[PROOFSTEP]
refine' ⟨Fintype.one_lt_card_iff_nontrivial.2 inferInstance, fun n hn => _⟩
[GOAL]
case intro
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ n = 1 ∨ n = Fintype.card α
[PROOFSTEP]
refine' (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).symm.imp _ _
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊤ → n = 1
[PROOFSTEP]
intro h
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n = 1
[PROOFSTEP]
have hgo := orderOf_pow (n := n) g
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = orderOf g / Nat.gcd (orderOf g) n
⊢ n = 1
[PROOFSTEP]
rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.gcd_eq_right_iff_dvd.1 hn, orderOf_eq_card_of_forall_mem_zpowers,
  eq_comm, Nat.div_eq_iff_eq_mul_left (Nat.pos_of_dvd_of_pos hn h0) hn] at hgo
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo✝ : orderOf (g ^ n) = Fintype.card α / n
hgo : Fintype.card α = Fintype.card α * n
⊢ n = 1
[PROOFSTEP]
exact (mul_left_cancel₀ (ne_of_gt h0) ((mul_one (Fintype.card α)).trans hgo)).symm
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
⊢ ∀ (x : α), x ∈ Subgroup.zpowers (g ^ n)
[PROOFSTEP]
intro x
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ Subgroup.zpowers (g ^ n)
[PROOFSTEP]
rw [h]
[GOAL]
case intro.refine'_1
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊤
hgo : orderOf (g ^ n) = Fintype.card α / n
x : α
⊢ x ∈ ⊤
[PROOFSTEP]
exact Subgroup.mem_top _
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
⊢ Subgroup.zpowers (g ^ n) = ⊥ → n = Fintype.card α
[PROOFSTEP]
intro h
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ n = Fintype.card α
[PROOFSTEP]
apply le_antisymm (Nat.le_of_dvd h0 hn)
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ Fintype.card α ≤ n
[PROOFSTEP]
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ orderOf g ≤ n
[PROOFSTEP]
apply orderOf_le_of_pow_eq_one (Nat.pos_of_dvd_of_pos hn h0)
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n = 1
[PROOFSTEP]
rw [← Subgroup.mem_bot, ← h]
[GOAL]
case intro.refine'_2
α : Type u
a : α
inst✝² : CommGroup α
inst✝¹ : IsSimpleGroup α
inst✝ : Fintype α
h0 : 0 < Fintype.card α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
n : ℕ
hn : n ∣ Fintype.card α
h : Subgroup.zpowers (g ^ n) = ⊥
⊢ g ^ n ∈ Subgroup.zpowers (g ^ n)
[PROOFSTEP]
exact Subgroup.mem_zpowers _
[GOAL]
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsSimpleGroup α → IsCyclic α ∧ Nat.Prime (Fintype.card α)
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
h : IsSimpleGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α)
[PROOFSTEP]
exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩
[GOAL]
case mpr
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
⊢ IsCyclic α ∧ Nat.Prime (Fintype.card α) → IsSimpleGroup α
[PROOFSTEP]
rintro ⟨_, hp⟩
[GOAL]
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
⊢ IsSimpleGroup α
[PROOFSTEP]
haveI : Fact (Fintype.card α).Prime := ⟨hp⟩
[GOAL]
case mpr.intro
α : Type u
a : α
inst✝¹ : Fintype α
inst✝ : CommGroup α
left✝ : IsCyclic α
hp : Nat.Prime (Fintype.card α)
this : Fact (Nat.Prime (Fintype.card α))
⊢ IsSimpleGroup α
[PROOFSTEP]
exact isSimpleGroup_of_prime_card rfl
[GOAL]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
⊢ exponent α = Fintype.card α
[PROOFSTEP]
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
[GOAL]
case intro
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α = Fintype.card α
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ exponent α ∣ Fintype.card α
[PROOFSTEP]
rw [← lcm_order_eq_exponent, Finset.lcm_dvd_iff]
[GOAL]
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ ∀ (b : α), b ∈ Finset.univ → orderOf b ∣ Fintype.card α
[PROOFSTEP]
exact fun b _ => orderOf_dvd_card_univ
[GOAL]
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ Fintype.card α ∣ exponent α
[PROOFSTEP]
rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
[GOAL]
case intro.a
α : Type u
a : α
inst✝² : Group α
inst✝¹ : IsCyclic α
inst✝ : Fintype α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
⊢ orderOf g ∣ exponent α
[PROOFSTEP]
exact order_dvd_exponent _