-- Mathlib/GroupTheory/Exponent.lean
theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ} (hp : p.Prime) :
    ∃ g : G, orderOf g = p ^ (exponent G).factorization p

Proof state:
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ orderOf (g ^ k) = p ^ t.succ

Tactic:
apply orderOf_eq_prime_pow

Result:
case inr.intro.intro.intro.hnot
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ¬(g ^ k) ^ p ^ t = 1

case inr.intro.intro.intro.hfin
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Proof state:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
ht : exponent G = ⊥
⊢ False

Tactic:
rw [ht] at h

Result:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : ⊥.factorization p ≠ 0
ht : exponent G = ⊥
⊢ False

Proof state:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
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]

Result:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p ≠ 0
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Proof state:
case inr
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 := by
  suffices key : ¬exponent G ∣ exponent G / p by
    rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at 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_primeFactors h) hd)

Result:
case inr.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Proof state:
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ orderOf 1 = p ^ (exponent G).factorization p

Tactic:
rw [h, pow_zero, orderOf_one]

Result:
no goals

Proof state:
case inr.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p

Tactic:
obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)

Result:
case inr.intro.intro.intro
G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : p ∈ (exponent G).factorization.support
he : 0 < exponent G
g : G
hg : g ^ (exponent G / p) ≠ 1
k : ℕ
hk : exponent G = p ^ (exponent G).factorization p * k
t : ℕ
ht : (exponent G).factorization p = t.succ
⊢ ∃ g, orderOf g = p ^ (exponent G).factorization p