G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
haveI := Fact.mk hp
case inl
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p = 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p

case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
have he : 0 < exponent G :=
  Ne.bot_lt fun ht => by
    rw [ht] at h
    apply h
    rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
rw [← Finsupp.mem_support_iff] at h
case inr.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
case inr.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ord_proj_dvd _ _
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
case inr.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ ↑(Nat.factorization (exponent G)) p
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
refine' ⟨g ^ k, _⟩
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ Nat.succ t
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ ↑(Nat.factorization (exponent G)) p
rw [ht]
case inr.intro.intro.intro.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ¬(g ^ k) ^ p ^ t = 1

case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ (g ^ k) ^ p ^ (t + 1) = 1
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ orderOf (g ^ k) = p ^ Nat.succ t
apply orderOf_eq_prime_pow
no goals
case inl
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p = 0
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
refine' ⟨1, by rw [h, pow_zero, orderOf_one]⟩
no goals
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p = 0
⊢ orderOf 1 = p ^ ↑(Nat.factorization (exponent G)) p
rw [h, pow_zero, orderOf_one]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ False
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization (exponent G)) p ≠ 0
ht : exponent G = ⊥
⊢ False
rw [ht] at h
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ ↑(Nat.factorization ⊥) p = 0
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ False
apply h
no goals
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ↑(Nat.factorization ⊥) p ≠ 0
ht : exponent G = ⊥
⊢ ↑(Nat.factorization ⊥) p = 0
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
⊢ ∃ g, g ^ (exponent G / p) ≠ 1

case key
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ¬exponent G ∣ exponent G / p
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ∃ g, g ^ (exponent G / p) ≠ 1
suffices key : ¬exponent G ∣ exponent G / p
no goals
case key
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
⊢ ¬exponent G ∣ exponent G / p
exact fun hd =>
  hp.one_lt.not_le
    ((mul_le_iff_le_one_left he).mp <|
      Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_factorization h) hd)
no goals
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
key : ¬exponent G ∣ exponent G / p
⊢ ∃ g, g ^ (exponent G / p) ≠ 1
simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key
no goals
case inr.intro.intro.intro.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ ¬(g ^ k) ^ p ^ t = 1
rwa [hk, mul_comm, ht, pow_succ', ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ g ^ exponent G = 1
case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ (g ^ k) ^ p ^ (t + 1) = 1
rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
no goals
case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (Nat.factorization (exponent G)).support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ ↑(Nat.factorization (exponent G)) p * k
t : ℕ
ht : ↑(Nat.factorization (exponent G)) p = Nat.succ t
⊢ g ^ exponent G = 1
exact pow_exponent_eq_one g