[GOAL]
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ exponent G ≠ 0
[PROOFSTEP]
rw [exponent]
[GOAL]
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ (if h : ExponentExists G then Nat.find h else 0) ≠ 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ ExponentExists G ↔ Nat.find h ≠ 0
[PROOFSTEP]
simp [h, @not_lt_zero' ℕ]
  --if this isn't done this way, `to_additive` freaks
[GOAL]
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ ExponentExists G ↔ 0 ≠ 0
[PROOFSTEP]
tauto
[GOAL]
G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ¬ExponentExists G
[PROOFSTEP]
simp only [exponentExists_iff_ne_zero, Classical.not_not]
[GOAL]
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1
[PROOFSTEP]
by_cases ExponentExists G
[GOAL]
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1
[PROOFSTEP]
by_cases ExponentExists G
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1
[PROOFSTEP]
simp_rw [exponent, dif_pos h]
[GOAL]
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
[PROOFSTEP]
exact (Nat.find_spec h).2 g
[GOAL]
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
[PROOFSTEP]
simp_rw [exponent, dif_neg h, pow_zero]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))
[PROOFSTEP]
rw [Nat.mod_add_div]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)
[PROOFSTEP]
simp [pow_add, pow_mul, pow_exponent_eq_one]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < exponent G
[PROOFSTEP]
have h : ∃ n, 0 < n ∧ ∀ g : G, g ^ n = 1 := ⟨n, hpos, hG⟩
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ 0 < exponent G
[PROOFSTEP]
rw [exponent, dif_pos]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ 0 < Nat.find ?hc
case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
h : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
[PROOFSTEP]
exact (Nat.find_spec h).1
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ≤ n
[PROOFSTEP]
rw [exponent, dif_pos]
[GOAL]
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.find ?hc ≤ n
[PROOFSTEP]
apply Nat.find_min'
[GOAL]
case h
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ 0 < n ∧ ∀ (g : G), g ^ n = 1
[PROOFSTEP]
exact ⟨hpos, hG⟩
[GOAL]
case hc
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : 0 < n
hG : ∀ (g : G), g ^ n = 1
⊢ ExponentExists G
[PROOFSTEP]
exact ⟨n, hpos, hG⟩
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1
[PROOFSTEP]
by_contra' h
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False
[PROOFSTEP]
have hcon : exponent G ≤ m := exponent_min' m hpos h
[GOAL]
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False
[PROOFSTEP]
linarith
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G ≤ 1
[PROOFSTEP]
apply exponent_min' _ Nat.one_pos
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
[PROOFSTEP]
simp
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 1 ≤ exponent G
[PROOFSTEP]
apply Nat.succ_le_of_lt
[GOAL]
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 0 < exponent G
[PROOFSTEP]
apply exponent_pos_of_exists 1 Nat.one_pos
[GOAL]
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
[PROOFSTEP]
simp
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hpos)
[GOAL]
case inl
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
hG : ∀ (g : G), g ^ 0 = 1
⊢ exponent G ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case inr
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ exponent G ∣ n
[PROOFSTEP]
apply Nat.dvd_of_mod_eq_zero
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
⊢ n % exponent G = 0
[PROOFSTEP]
by_contra h
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
⊢ False
[PROOFSTEP]
have h₁ := Nat.pos_of_ne_zero h
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
⊢ False
[PROOFSTEP]
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ False
[PROOFSTEP]
have h₃ : exponent G ≤ n % exponent G := by
  apply exponent_min' _ h₁
  simp_rw [← pow_eq_mod_exponent]
  exact hG
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G
[PROOFSTEP]
apply exponent_min' _ h₁
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ (n % exponent G) = 1
[PROOFSTEP]
simp_rw [← pow_eq_mod_exponent]
[GOAL]
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1
[PROOFSTEP]
exact hG
[GOAL]
case inr.H
G✝ : Type u
inst✝¹ : Monoid G✝
G : Type u_1
inst✝ : Monoid G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
hpos : n > 0
h : ¬n % exponent G = 0
h₁ : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False
[PROOFSTEP]
linarith
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf ∣ exponent G
[PROOFSTEP]
apply Finset.lcm_dvd
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ (b : G), b ∈ Finset.univ → orderOf b ∣ exponent G
[PROOFSTEP]
intro g _
[GOAL]
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
[PROOFSTEP]
exact order_dvd_exponent g
[GOAL]
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
⊢ ∃ g, orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
[PROOFSTEP]
haveI := Fact.mk hp
[GOAL]
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
[PROOFSTEP]
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
[GOAL]
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
[PROOFSTEP]
refine' ⟨1, by rw [h, pow_zero, orderOf_one]⟩
[GOAL]
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
[PROOFSTEP]
rw [h, pow_zero, orderOf_one]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
rw [ht] at h 
[GOAL]
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
[PROOFSTEP]
apply h
[GOAL]
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
[PROOFSTEP]
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
[GOAL]
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
[PROOFSTEP]
rw [← Finsupp.mem_support_iff] at h 
[GOAL]
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
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 :=
  by
  suffices key : ¬exponent G ∣ exponent G / p
  · simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key
  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)
[GOAL]
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
[PROOFSTEP]
suffices key : ¬exponent G ∣ exponent G / p
[GOAL]
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
[PROOFSTEP]
simpa using mt (exponent_dvd_of_forall_pow_eq_one G (exponent G / p)) key
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ord_proj_dvd _ _
[GOAL]
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
[PROOFSTEP]
obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
[GOAL]
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
[PROOFSTEP]
refine' ⟨g ^ k, _⟩
[GOAL]
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
[PROOFSTEP]
rw [ht]
[GOAL]
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
[PROOFSTEP]
apply orderOf_eq_prime_pow
[GOAL]
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
[PROOFSTEP]
rwa [hk, mul_comm, ht, pow_succ', ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg 
[GOAL]
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
[PROOFSTEP]
rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
[GOAL]
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
[PROOFSTEP]
exact pow_exponent_eq_one g
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
[PROOFSTEP]
refine' ⟨fun he => _, fun he => _⟩
[GOAL]
case refine'_1
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ Set.Finite (Set.range orderOf)
[PROOFSTEP]
by_contra h
[GOAL]
case refine'_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
⊢ False
[PROOFSTEP]
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
[GOAL]
case refine'_1.intro.intro.intro
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬Set.Finite (Set.range orderOf)
t : G
het : exponent G < orderOf t
⊢ False
[PROOFSTEP]
exact pow_ne_one_of_lt_orderOf' he het (pow_exponent_eq_one t)
[GOAL]
case refine'_2
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
he : Set.Finite (Set.range orderOf)
⊢ exponent G ≠ 0
[PROOFSTEP]
lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ exponent G ≠ 0
[PROOFSTEP]
have htpos : 0 < t.prod id := by
  refine' Finset.prod_pos fun a ha => _
  rw [← Finset.mem_coe, ht] at ha 
  obtain ⟨k, rfl⟩ := ha
  exact h k
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
⊢ 0 < Finset.prod t id
[PROOFSTEP]
refine' Finset.prod_pos fun a ha => _
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ t
⊢ 0 < id a
[PROOFSTEP]
rw [← Finset.mem_coe, ht] at ha 
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
a : ℕ
ha : a ∈ Set.range orderOf
⊢ 0 < id a
[PROOFSTEP]
obtain ⟨k, rfl⟩ := ha
[GOAL]
case intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
k : G
⊢ 0 < id (orderOf k)
[PROOFSTEP]
exact h k
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ≠ 0
[PROOFSTEP]
suffices exponent G ∣ t.prod id by
  intro h
  rw [h, zero_dvd_iff] at this 
  exact htpos.ne' this
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
⊢ exponent G ≠ 0
[PROOFSTEP]
intro h
[GOAL]
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : exponent G ∣ Finset.prod t id
h : exponent G = 0
⊢ False
[PROOFSTEP]
rw [h, zero_dvd_iff] at this 
[GOAL]
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
this : Finset.prod t id = 0
h : exponent G = 0
⊢ False
[PROOFSTEP]
exact htpos.ne' this
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
⊢ exponent G ∣ Finset.prod t id
[PROOFSTEP]
refine' exponent_dvd_of_forall_pow_eq_one _ _ fun g => _
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ g ^ Finset.prod t id = 1
[PROOFSTEP]
rw [pow_eq_mod_orderOf, Nat.mod_eq_zero_of_dvd, pow_zero g]
[GOAL]
case refine'_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ orderOf g ∣ Finset.prod t id
[PROOFSTEP]
apply Finset.dvd_prod_of_mem
[GOAL]
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ t
[PROOFSTEP]
rw [← Finset.mem_coe, ht]
[GOAL]
case refine'_2.intro.ha
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ Set.Finite ↑t)
htpos : 0 < Finset.prod t id
g : G
⊢ Function.minimalPeriod (fun x => g * x) 1 ∈ Set.range orderOf
[PROOFSTEP]
exact Set.mem_range_self g
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
[PROOFSTEP]
have := exponent_ne_zero_iff_range_orderOf_finite h
[GOAL]
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
[PROOFSTEP]
rwa [Ne.def, not_iff_comm, Iff.comm] at this 
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf = exponent G
[PROOFSTEP]
apply Nat.dvd_antisymm (lcm_orderOf_dvd_exponent G)
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ exponent G ∣ Finset.lcm Finset.univ orderOf
[PROOFSTEP]
refine' exponent_dvd_of_forall_pow_eq_one G _ fun g => _
[GOAL]
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
[PROOFSTEP]
obtain ⟨m, hm⟩ : orderOf g ∣ Finset.univ.lcm orderOf := Finset.dvd_lcm (Finset.mem_univ g)
[GOAL]
case intro
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
m : ℕ
hm : Finset.lcm Finset.univ orderOf = orderOf g * m
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
[PROOFSTEP]
rw [hm, pow_mul, pow_orderOf_eq_one, one_pow]
[GOAL]
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ exponent G ≠ 0
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
val✝ : Fintype G
⊢ exponent G ≠ 0
[PROOFSTEP]
simpa [← lcm_order_eq_exponent, Finset.lcm_eq_zero_iff] using fun x => (orderOf_pos x).ne'
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
rw [iSup]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
rcases eq_or_ne (exponent G) 0 with (he | he)
[GOAL]
case inl
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
[GOAL]
case inr
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
[GOAL]
case inr
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
have hfin : (Set.range (orderOf : G → ℕ)).Finite := by rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
⊢ Set.Finite (Set.range orderOf)
[PROOFSTEP]
rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
[GOAL]
case inr
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
obtain ⟨t, ht⟩ := hne.cSup_mem hfin
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G = sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
apply Nat.dvd_antisymm _
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ sSup (Set.range fun g => orderOf g) ∣ exponent G
[PROOFSTEP]
rw [← ht]
[GOAL]
case inr.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ orderOf t ∣ exponent G
[PROOFSTEP]
apply order_dvd_exponent
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G ∣ sSup (Set.range fun g => orderOf g)
[PROOFSTEP]
refine' Nat.dvd_of_factors_subperm he _
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ Nat.factors (exponent G) <+~ Nat.factors (sSup (Set.range fun g => orderOf g))
[PROOFSTEP]
rw [List.subperm_ext_iff]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∀ (x : ℕ),
    x ∈ Nat.factors (exponent G) →
      List.count x (Nat.factors (exponent G)) ≤ List.count x (Nat.factors (sSup (Set.range fun g => orderOf g)))
[PROOFSTEP]
by_contra' h
[GOAL]
G : Type u
inst✝ : CommMonoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
h :
  ∃ x,
    x ∈ Nat.factors (exponent G) ∧
      List.count x (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count x (Nat.factors (exponent G))
⊢ False
[PROOFSTEP]
obtain ⟨p, hp, hpe⟩ := h
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : p ∈ Nat.factors (exponent G)
hpe : List.count p (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count p (Nat.factors (exponent G))
⊢ False
[PROOFSTEP]
replace hp := Nat.prime_of_mem_factors hp
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hpe : List.count p (Nat.factors (sSup (Set.range fun g => orderOf g))) < List.count p (Nat.factors (exponent G))
hp : Nat.Prime p
⊢ False
[PROOFSTEP]
simp only [Nat.factors_count_eq] at hpe 
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
⊢ False
[PROOFSTEP]
set k := (orderOf t).factorization p with hk
[GOAL]
case intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
⊢ False
[PROOFSTEP]
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
⊢ False
[PROOFSTEP]
suffices orderOf t < orderOf (t ^ p ^ k * g) by
  rw [ht] at this 
  exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
this : orderOf t < orderOf (t ^ p ^ k * g)
⊢ False
[PROOFSTEP]
rw [ht] at this 
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
this : sSup (Set.range orderOf) < orderOf (t ^ p ^ k * g)
⊢ False
[PROOFSTEP]
exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hpk : p ^ k ∣ orderOf t := Nat.ord_proj_dvd _ _
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
  rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k
[PROOFSTEP]
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
[GOAL]
case intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
have hcoprime : (orderOf (t ^ p ^ k)).coprime (orderOf g) :=
  by
  rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
  apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
  nth_rw 1 [← pow_one p]
  have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 :=
    by
    rw [hpk', Nat.factorization_div hpk]
    simp [hp]
  rw [this]
    -- Porting note: convert made to_additive complain
  apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
[PROOFSTEP]
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ Nat.coprime p (orderOf (t ^ p ^ k))
[PROOFSTEP]
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ ¬p ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
nth_rw 1 [← pow_one p]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 :=
  by
  rw [hpk', Nat.factorization_div hpk]
  simp [hp]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
[PROOFSTEP]
rw [hpk', Nat.factorization_div hpk]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
⊢ 1 = ↑(Nat.factorization (orderOf t) - Nat.factorization (p ^ k)) p + 1
[PROOFSTEP]
simp [hp]
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
this : 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
rw [this]
  -- Porting note: convert made to_additive complain
[GOAL]
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
this : 1 = ↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1
⊢ ¬p ^ (↑(Nat.factorization (orderOf (t ^ p ^ k))) p + 1) ∣ orderOf (t ^ p ^ k)
[PROOFSTEP]
apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)
[PROOFSTEP]
rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk', hg, ha, ← ht, ← hk, pow_add, pow_add,
  pow_one, ← mul_assoc, ← mul_assoc, Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| h t, ← pow_succ']
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ 1 < p ^ (a + 1)
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ p ^ k ∣ orderOf t
[PROOFSTEP]
exact one_lt_pow hp.one_lt a.succ_ne_zero
[GOAL]
case intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
hne : Set.Nonempty (Set.range orderOf)
hfin : Set.Finite (Set.range orderOf)
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p < ↑(Nat.factorization (exponent G)) p
k : ℕ := ↑(Nat.factorization (orderOf t)) p
hk : k = ↑(Nat.factorization (orderOf t)) p
g : G
hg : orderOf g = p ^ ↑(Nat.factorization (exponent G)) p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ↑(Nat.factorization (exponent G)) p = ↑(Nat.factorization (sSup (Set.range fun g => orderOf g))) p + a + 1
hcoprime : Nat.coprime (orderOf (t ^ p ^ k)) (orderOf g)
⊢ p ^ k ∣ orderOf t
[PROOFSTEP]
exact hpk
[GOAL]
G : Type u
inst✝ : CommMonoid G
⊢ exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ (g : G), orderOf g
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G : Type u
inst✝ : CommMonoid G
h : ∃ g, orderOf g = 0
⊢ exponent G = 0
[PROOFSTEP]
obtain ⟨g, hg⟩ := h
[GOAL]
case pos.intro
G : Type u
inst✝ : CommMonoid G
g : G
hg : orderOf g = 0
⊢ exponent G = 0
[PROOFSTEP]
exact exponent_eq_zero_of_order_zero hg
[GOAL]
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
have := not_exists.mp h
[GOAL]
case neg
G : Type u
inst✝ : CommMonoid G
h : ¬∃ g, orderOf g = 0
this : ∀ (x : G), ¬orderOf x = 0
⊢ exponent G = ⨆ (g : G), orderOf g
[PROOFSTEP]
exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ 1 ∈ Finset.image orderOf Finset.univ
[PROOFSTEP]
simp
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = Finset.max' (Finset.image orderOf Finset.univ) (_ : ∃ x, x ∈ Finset.image orderOf Finset.univ)
[PROOFSTEP]
rw [← Finset.Nonempty.cSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]
[GOAL]
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf
[PROOFSTEP]
exact exponent_eq_iSup_orderOf orderOf_pos
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
[PROOFSTEP]
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
[PROOFSTEP]
rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
have hf : Function.Surjective f :=
  by
  rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
  exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Function.Surjective ↑f
[PROOFSTEP]
rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
[GOAL]
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ ↑S ⊆ ↑(MonoidHom.range f)
[PROOFSTEP]
exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Function.Surjective ↑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
replace hf := nat_card_dvd_of_surjective f hf
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
rw [Nat.card_pi] at hf 
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
[PROOFSTEP]
refine' hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => _)
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card { x // x ∈ zpowers ↑g } ∣ Monoid.exponent G
[PROOFSTEP]
rw [← order_eq_card_zpowers']
[GOAL]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G
[PROOFSTEP]
exact Monoid.order_dvd_exponent (g : G)
