-- Mathlib/GroupTheory/Exponent.lean
theorem exists_orderOf_eq_exponent (hG : ExponentExists G) : ∃ g : G, orderOf g = exponent G

Proof state:
case h.intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
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 [k, hp]
  rw [this]
  apply Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp

Result:
case h.intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Proof state:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)

Tactic:
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
 rw [hpk', Nat.factorization_div hpk]
 simp [k, hp]

Result:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
this : 1 = (orderOf (t ^ p ^ k)).factorization p + 1
⊢ ¬p ^ 1 ∣ orderOf (t ^ p ^ k)

Proof state:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ orderOf t = exponent G

Tactic:
apply Nat.dvd_antisymm (order_dvd_exponent _)

Result:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ exponent G ∣ orderOf t

Proof state:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList

Tactic:
by_contra! h

Result:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
h :
  ∃ x ∈ (exponent G).primeFactorsList,
    List.count x (orderOf t).primeFactorsList < List.count x (exponent G).primeFactorsList
⊢ False

Proof state:
case h.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
hp : Nat.Prime p
⊢ False

Tactic:
simp only [Nat.primeFactorsList_count_eq] at hpe

Result:
case h.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
hpe : (orderOf t).factorization p < (exponent G).factorization p
⊢ False

Proof state:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
⊢ ∃ g, orderOf g = exponent G

Tactic:
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩

Result:
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
⊢ ∃ g, orderOf g = exponent G

Proof state:
case h.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : p ∈ (exponent G).primeFactorsList
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
⊢ False

Tactic:
replace hp := Nat.prime_of_mem_primeFactorsList hp

Result:
case h.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
hp : Nat.Prime p
⊢ False

Proof state:
case h.intro.intro.intro.intro
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : (exponent G).factorization p = k + a + 1
hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g)
⊢ p ^ (orderOf t).factorization p ∣ orderOf t

Tactic:
exact hpk

Result:
no goals