awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
H : Type u_1
inst_1 : Monoid H
e : G ≃* H
⊢ exponent G = exponent H

Tactic:
Nat.dvd_antisymm
    (exponent_dvd_of_monoidHom e e.injective)
    (exponent_dvd_of_monoidHom e.symm e.symm.injective)

Premises used: MonoidHomClass.toMonoidHom, Monoid.exponent_dvd_of_monoidHom, MulEquiv.symm, MulEquiv.injective, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ exponent.{u} ↥⊤ = exponent G

Tactic:
exponent_eq_of_mulEquiv Submonoid.topEquiv

Premises used: Submonoid.topEquiv, Monoid.exponent_eq_of_mulEquiv
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ S) g g_in_s ^ exponent.{u} ↥S = 1

Tactic:
have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) g g_in_s ^ exponent.{u} ↥S = 1
rwa : ∀ (this : Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g ^ exponent.{u} ↥S) ⋯ = 1), g ^ exponent.{u} ↥S = 1
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) (g ^ exponent.{u} ↥S) ⋯) : G) = 1), g ^ exponent.{u} ↥S = 1
⊢ g ^ exponent.{u} ↥S = 1

Tactic:
rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

Premises used: OneMemClass.coe_eq_one, SubmonoidClass.mk_pow
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩

Premises used: Finset.univ, orderOf, And.intro, Exists.intro, Finset.lcm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
refine_1 : 0 < Finset.lcm.{0, u} (β := G) Finset.univ orderOf
refine_2 : ∀ (g : G), g ^ Finset.lcm.{0, u} (β := G) Finset.univ orderOf = 1
⊢ ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.lcm.{0, u} (β := G) Finset.univ orderOf

Tactic:
simpa [pos_iff_ne_zero, Finset.lcm_eq_zero_iff] using fun x => (_root_.orderOf_pos x).ne'

Premises used: LT.lt.ne', Finset.lcm_eq_zero_iff, orderOf_pos, pos_iff_ne_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
refine_2 : orderOf g ∣ exponent G
⊢ g ^ Finset.lcm.{0, u} (β := G) Finset.univ orderOf = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, lcm_orderOf_eq_exponent]

Premises used: Monoid.lcm_orderOf_eq_exponent, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G

Tactic:
order_dvd_exponent g

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G

Tactic:
exact order_dvd_exponent g

Premises used: Monoid.order_dvd_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
⊢ exponent G ≠ 0

Tactic:
ExponentExists.of_finite.exponent_ne_zero

Premises used: Monoid.ExponentExists.exponent_ne_zero, Monoid.ExponentExists.of_finite
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
inst_2 : Nontrivial G
rw : exponent G ≠ 0 ∧ exponent G ≠ 1
⊢ 1 < exponent G

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one]

Premises used: Nat.one_lt_iff_ne_zero_and_ne_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
inst_2 : Nontrivial G
⊢ exponent G ≠ 0 ∧ exponent G ≠ 1

Tactic:
⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

Premises used: mt, And.intro, Monoid.exp_eq_one_iff, not_subsingleton, Iff.mp, Monoid.exponent_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
inst_2 : Nontrivial G
⊢ exponent G ≠ 0 ∧ exponent G ≠ 1

Tactic:
exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : LeftCancelMonoid G
inst_1 : Finite G
⊢ NeZero (exponent G)

Tactic:
⟨Monoid.exponent_ne_zero_of_finite⟩

Premises used: NeZero.mk, Monoid.exponent_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
⊢ exponent G ≠ 0

Tactic:
have he := hG.exponent_ne_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty

Tactic:
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
rwa rwa₁ rwa₂ rwa₃ : exponent G ≠ 0
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]

Premises used: Monoid.exponent_ne_zero_iff_range_orderOf_finite, Monoid.ExponentExists.orderOf_pos
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
⊢ (Set.range.{0, u + 1} (ι := G) orderOf).Finite

Tactic:
have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
    rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
obtain : ∀ (t : G) (ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)), ∃ (g : G), orderOf g = exponent G
⊢ ∃ (g : G), orderOf g = exponent G

Tactic:
obtain ⟨t, ht⟩ := hne.csSup_mem hfin

Premises used: Set.Nonempty.csSup_mem
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
h : orderOf t = exponent G
⊢ ∃ (g : G), orderOf g = exponent G

Tactic:
use t
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
h : exponent G ∣ orderOf t
⊢ orderOf t = exponent G

Tactic:
apply Nat.dvd_antisymm (order_dvd_exponent _)

Premises used: Monoid.order_dvd_exponent, Nat.dvd_antisymm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
⊢ exponent G ∣ orderOf t

Tactic:
Nat.dvd_of_primeFactorsList_subperm he ?_

Premises used: Nat.dvd_of_primeFactorsList_subperm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
h : (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList
⊢ exponent G ∣ orderOf t

Tactic:
refine Nat.dvd_of_primeFactorsList_subperm he ?_

Premises used: Nat.dvd_of_primeFactorsList_subperm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
h :
  ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
⊢ (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList

Tactic:
rw [List.subperm_ext_iff]

Premises used: List.subperm_ext_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
h :
  ∀ (p : ℕ) (hp : p ∈ (exponent G).primeFactorsList)
    (hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList), False
⊢ ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList

Tactic:
by_contra! ⟨p, hp, hpe⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : p ∈ (exponent G).primeFactorsList
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
⊢ Nat.Prime p

Tactic:
replace hp := Nat.prime_of_mem_primeFactorsList hp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hpe : List.count p (orderOf t).primeFactorsList < List.count p (exponent G).primeFactorsList
hp : Nat.Prime p
⊢ LT.lt (α := ℕ) (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
simp only [Nat.primeFactorsList_count_eq] at hpe

Premises used: Nat.primeFactorsList_count_eq
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
hpe :
  LT.lt (α := ℕ) (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ let k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p;
  k < ((exponent G).factorization : (a : ℕ) → ℕ) p

Tactic:
set k := (orderOf t).factorization p with hk

Premises used: orderOf, DFunLike.coe, Nat.factorization
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
hpe :
  LT.lt (α := ℕ) (((orderOf t).factorization : (a : ℕ) → ℕ) p : ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpe₁ :
  let k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p;
  k < ((exponent G).factorization : (a : ℕ) → ℕ) p
⊢ let k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p;
  k = ((orderOf t).factorization : (a : ℕ) → ℕ) p

Tactic:
set k := (orderOf t).factorization p with hk

Premises used: orderOf, DFunLike.coe, Nat.factorization
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
h : ∀ (g : G) (hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)), False
⊢ False

Tactic:
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G

Premises used: Nat.Prime.exists_orderOf_eq_pow_factorization_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
this : orderOf t < orderOf (t ^ p ^ k * g)
⊢ sSup (Set.range.{0, u + 1} (ι := G) orderOf) < orderOf (t ^ p ^ k * g)

Tactic:
rw [ht] at this
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
this : sSup (Set.range.{0, u + 1} (ι := G) orderOf) < orderOf (t ^ p ^ k * g)
⊢ False

Tactic:
this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)

Premises used: Set.mem_range_self, le_csSup, LT.lt.not_ge, Set.Finite.bddAbove
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
this : sSup (Set.range.{0, u + 1} (ι := G) orderOf) < orderOf (t ^ p ^ k * g)
⊢ False

Tactic:
exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)

Premises used: Set.mem_range_self, le_csSup, LT.lt.not_ge, Set.Finite.bddAbove
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
h : orderOf t < orderOf (t ^ p ^ k * g)
⊢ False

Tactic:
suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ p ^ k ∣ orderOf t

Tactic:
have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
rw : orderOf t / (orderOf t).gcd (p ^ k) = orderOf t / p ^ k
rw₁ rw₂ : orderOf t / p ^ k = orderOf t / p ^ k
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k

Tactic:
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]

Premises used: orderOf_pow', pow_ne_zero, Nat.Prime.ne_zero, Nat.gcd_eq_right
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
⊢ orderOf (t ^ p ^ k) = orderOf t / p ^ k

Tactic:
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]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
h : ∀ (a : ℕ) (ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1), orderOf t < orderOf (t ^ p ^ k * g)
⊢ orderOf t < orderOf (t ^ p ^ k * g)

Tactic:
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe

Premises used: Nat.exists_eq_add_of_lt
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
rw : p.Coprime (orderOf (t ^ p ^ k))
⊢ (orderOf (t ^ p ^ k)).Coprime (orderOf g)

Tactic:
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]

Premises used: Nat.coprime_pow_right_iff, pos_of_gt, Nat.coprime_comm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
apply : ¬p ∣ orderOf (t ^ p ^ k)
⊢ p.Coprime (orderOf (t ^ p ^ k))

Tactic:
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)

Premises used: Or.resolve_right, Nat.coprime_or_dvd_of_prime
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
nth_rw : ¬HPow.hPow (β := ℕ) p 1 ∣ orderOf (t ^ p ^ k)
⊢ ¬p ∣ orderOf (t ^ p ^ k)

Tactic:
nth_rw 1 [← pow_one p]

Premises used: pow_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
rw : 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf t).factorization - (p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
⊢ 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf (t ^ p ^ k)).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
rw [hpk', Nat.factorization_div hpk]

Premises used: Nat.factorization_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range.{0, u + 1} (ι := G) orderOf).Nonempty
hfin : (Set.range.{0, u + 1} (ι := G) orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range.{0, u + 1} (ι := G) orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := ((orderOf t).factorization : (a : ℕ) → ℕ) p
hpe : k < ((exponent G).factorization : (a : ℕ) → ℕ) p
hk : k = ((orderOf t).factorization : (a : ℕ) → ℕ) p
g : G
hg : orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
hpk : p ^ k ∣ orderOf t
hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k
a : ℕ
ha : ((exponent G).factorization : (a : ℕ) → ℕ) p = k + a + 1
⊢ 1 = HAdd.hAdd (α := ℕ) (β := ℕ) (((orderOf t).factorization - (p ^ k).factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)

Tactic:
simp [k, hp]