G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = ⨆ (g : G), orderOf g
rw [iSup]
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)

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)
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = sSup (Set.range fun g => orderOf g)
rcases eq_or_ne (exponent G) 0 with (he | he)
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)
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)
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
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)
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)
have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
  rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
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)
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)
obtain ⟨t, ht⟩ := hne.cSup_mem hfin
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

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)
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)
apply Nat.dvd_antisymm _
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))
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)
refine' Nat.dvd_of_factors_subperm he _
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)))
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))
rw [List.subperm_ext_iff]
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
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)))
by_contra' h
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
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
obtain ⟨p, hp, hpe⟩ := h
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
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
replace hp := Nat.prime_of_mem_factors hp
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
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
simp only [Nat.factors_count_eq] at hpe
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
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
set k := (orderOf t).factorization p with hk
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
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
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
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)
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
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 _)
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)
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)
have hpk : p ^ k ∣ orderOf t := Nat.ord_proj_dvd _ _
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)
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)
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]
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)
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)
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
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)
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)
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]
  apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
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
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)
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']
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
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
exact one_lt_pow hp.one_lt a.succ_ne_zero
no goals
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
exact hpk
no goals
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)
rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
no goals
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)
rwa [← exponent_ne_zero_iff_range_orderOf_finite h]
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
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
rw [← ht]
no goals
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
apply order_dvd_exponent
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
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
rw [ht] at this
no goals
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
exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
no goals
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
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
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))
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)
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
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)
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))
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
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)
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)
nth_rw 1 [← pow_one p]
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)
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)
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
 rw [hpk', Nat.factorization_div hpk]
 simp [hp]
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)
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)
rw [this]
no goals
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)
apply Nat.pow_succ_factorization_not_dvd (h <| t ^ p ^ k).ne' hp
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
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
rw [hpk', Nat.factorization_div hpk]
no goals
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
simp [hp]