awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
inl : exponent G ∣ 0 ↔ ∀ (g : G), HPow.hPow (β := ℕ) g 0 = 1
inr : ∀ (hpos : n > 0), exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
⊢ exponent G ∣ 0 ↔ ∀ (g : G), HPow.hPow (β := ℕ) g 0 = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
inr : exponent G ∣ n → ∀ (g : G), g ^ n = 1
inr₁ : (∀ (g : G), g ^ n = 1) → exponent G ∣ n
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : exponent G ∣ n
g : G
inr : ∀ (h : n % exponent G = 0) (g : G), g ^ n = 1
⊢ g ^ n = 1

Tactic:
rw [Nat.dvd_iff_mod_eq_zero] at h

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
h : n % exponent G = 0
g : G
inr : g ^ (n % exponent G) = 1
inr₁ : HPow.hPow (β := ℕ) g 0 = 1
inr₂ inr₃ : Eq.{u + 1} (α := G) 1 1
⊢ g ^ n = 1

Tactic:
rw [pow_eq_mod_exponent, h, pow_zero]

Premises used: Monoid.pow_eq_mod_exponent, pow_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
inr : ∀ (h : ¬exponent G ∣ n), False
⊢ exponent G ∣ n

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬exponent G ∣ n
⊢ 0 < n % exponent G

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h

Premises used: Ne, Nat.dvd_iff_mod_eq_zero, pos_iff_ne_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
⊢ n % exponent G < exponent G

Tactic:
have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
apply : ∀ (g : G), g ^ (n % exponent G) = 1
⊢ exponent G ≤ n % exponent G

Tactic:
apply exponent_min' _ h

Premises used: Monoid.exponent_min'
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
simp_rw : ∀ (g : G), g ^ n = 1
⊢ ∀ (g : G), g ^ (n % exponent G) = 1

Tactic:
simp_rw [← pow_eq_mod_exponent]

Premises used: Monoid.pow_eq_mod_exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1

Tactic:
hG
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ ∀ (g : G), g ^ n = 1

Tactic:
exact hG
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
⊢ exponent G ≤ n % exponent G

Tactic:
have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False

Tactic:
h₂.not_ge h₃

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : 0 < n % exponent G
h₂ : n % exponent G < exponent G
h₃ : exponent G ≤ n % exponent G
⊢ False

Tactic:
exact h₂.not_ge h₃

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
n : ℕ
simp_rw : (∀ (g : G), g ^ n = 1) ↔ ∀ (g : G), orderOf g ∣ n
⊢ exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n

Tactic:
simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

Premises used: Monoid.exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : Fintype G
a : ∀ (b : G), Membership.mem (γ := Finset G) Finset.univ b → orderOf b ∣ exponent G
⊢ Finset.lcm.{0, u} (β := G) Finset.univ orderOf ∣ exponent G

Tactic:
apply Finset.lcm_dvd

Premises used: Finset.lcm_dvd
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : Fintype G
g : G
a : Membership.mem (γ := Finset G) Finset.univ g → orderOf g ∣ exponent G
⊢ Membership.mem (γ := Finset G) Finset.univ g → orderOf g ∣ exponent G

Tactic:
_
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
inst_1 : Fintype G
g : G
h : Membership.mem (γ := Finset G) Finset.univ 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 : Monoid G
inst_1 : Fintype G
g : G
h : Membership.mem (γ := Finset G) Finset.univ 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 : Monoid G
p : ℕ
hp : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
haveI := Fact.mk hp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
inl :
  ∀ (h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
inr :
  ∀ (h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)

Premises used: eq_or_ne, Monoid.exponent, OfNat.ofNat, DFunLike.coe, Nat.factorization
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw : orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p 0
rw₁ : orderOf.{u} (G := G) 1 = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ orderOf.{u} (G := G) 1 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [h, pow_zero, orderOf_one]

Premises used: orderOf_one, pow_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Eq (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
refine ⟨1, by rw [h, pow_zero, orderOf_one]⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
⊢ Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [ht] at h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
h₁ : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ exponent G = ⊥

Tactic:
rw [ht] at h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
apply : Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ False

Tactic:
apply h
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
ht : exponent G = ⊥
rw : Eq (α := ℕ) ((Nat.factorization 0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw₁ : Eq (α := ℕ) ((0 : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((Nat.factorization ⊥ : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)

Tactic:
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]

Premises used: Nat.factorization_zero, Finsupp.zero_apply, bot_eq_zero
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
⊢ 0 < exponent G

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]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
he : 0 < exponent G
⊢ p ∈ (exponent G).factorization.support

Tactic:
rw [← Finsupp.mem_support_iff] at h

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : Ne (α := ℕ) (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) (0 : ℕ)
he : 0 < exponent G
h₁ : p ∈ (exponent G).factorization.support
⊢ 0 < exponent G

Tactic:
rw [← Finsupp.mem_support_iff] at h

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
key : ¬exponent G ∣ exponent G / p
rwa : ∀ (key : ¬∀ (g : G), g ^ (exponent G / p) = 1), ∃ (g : G), g ^ (exponent G / p) ≠ 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (key : ∃ (x : G), ¬x ^ (exponent G / p) = 1), ∃ (g : G), g ^ (exponent G / p) ≠ 1
⊢ ∃ (g : G), g ^ (exponent G / p) ≠ 1

Tactic:
rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key

Premises used: Monoid.exponent_dvd_iff_forall_pow_eq_one, Classical.not_forall
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
suffices : ¬exponent G ∣ exponent G / p
⊢ ∃ (g : G), g ^ (exponent G / p) ≠ 1

Tactic:
suffices key : ¬exponent G ∣ exponent G / p by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
⊢ ¬exponent G ∣ exponent G / p

Tactic:
fun hd =>
      hp.one_lt.not_ge
        ((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)

Premises used: Nat.dvd_of_mem_primeFactors, Nat.Prime.one_lt, Iff.mp, Nat.mul_dvd_of_dvd_div, LT.lt.not_ge, Nat.le_of_dvd, Not, mul_le_iff_le_one_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
⊢ ¬exponent G ∣ exponent G / p

Tactic:
exact fun hd =>
      hp.one_lt.not_ge
        ((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)

Premises used: Nat.dvd_of_mem_primeFactors, Nat.Prime.one_lt, Iff.mp, Nat.mul_dvd_of_dvd_div, LT.lt.not_ge, Nat.le_of_dvd, mul_le_iff_le_one_left
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
inr :
  ∀ (g : G) (hg : g ^ (exponent G / p) ≠ 1),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) 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_ge
        ((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)

Premises used: HDiv.hDiv, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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
inr :
  ∀ (k : ℕ) (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ordProj_dvd _ _

Premises used: Nat.ordProj_dvd, Monoid.exponent
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
inr :
  ∀ (t : ℕ) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

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

Premises used: Finsupp.mem_support_iff, Nat.exists_eq_succ_of_ne_zero, Iff.mp
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
⟨g ^ k, ?_⟩

Premises used: HPow.hPow, Exists.intro
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr : orderOf (g ^ k) = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)
⊢ ∃ (g : G), orderOf g = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
refine ⟨g ^ k, ?_⟩
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr : orderOf (g ^ k) = p ^ t.succ
⊢ orderOf (g ^ k) = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [ht]
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr : ¬(g ^ k) ^ p ^ t = 1
inr₁ : (g ^ k) ^ p ^ (t + 1) = 1
⊢ orderOf (g ^ k) = p ^ t.succ

Tactic:
apply orderOf_eq_prime_pow

Premises used: orderOf_eq_prime_pow
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr :
  ∀ (hg : g ^ (HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₁ :
  ∀ (hg : g ^ (k * HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) / p) ≠ 1)
    (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₂ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t.succ / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₃ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * (p ^ t * p) / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₄ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t * p / p) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ),
    ¬(g ^ k) ^ p ^ t = 1
inr₅ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : g ^ (k * p ^ t) ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
inr₆ inr₇ inr₈ inr₉ :
  ∀ (hk : exponent G = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k) (t : ℕ)
    (hg : (g ^ k) ^ p ^ t ≠ 1) (ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ), ¬(g ^ k) ^ p ^ t = 1
⊢ ¬(g ^ k) ^ p ^ t = 1

Tactic:
rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg

Premises used: Nat.mul_div_cancel, pow_succ, mul_assoc, Nat.Prime.pos, pow_mul, mul_comm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
inr : g ^ exponent G = 1
⊢ (g ^ k) ^ p ^ (t + 1) = 1

Tactic:
rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]

Premises used: Nat.succ_eq_add_one, pow_mul, mul_comm
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ g ^ exponent G = 1

Tactic:
pow_exponent_eq_one g

Premises used: Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
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 = HPow.hPow (β := ℕ) p (((exponent G).factorization : (a : ℕ) → ℕ) p : ℕ) * k
t : ℕ
ht : ((exponent G).factorization : (a : ℕ) → ℕ) p = t.succ
⊢ g ^ exponent G = 1

Tactic:
exact pow_exponent_eq_one g

Premises used: Monoid.pow_exponent_eq_one
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
rw₁ :
  (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
⊢ orderOf
      (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) *
        y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]

Premises used: Commute.pow_pow, Commute.orderOf_mul_eq_mul_orderOf_of_coprime
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf x ≠ 0
hn : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [orderOf_pow_orderOf_div]

Premises used: orderOf_pow_orderOf_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
rw [orderOf_pow_orderOf_div]

Premises used: orderOf_pow_orderOf_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
iterate :
  (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
hx₂ : orderOf x ≠ 0
hn₁ : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
⊢ orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

Tactic:
iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]

Premises used: Nat.Coprime, orderOf_pow_orderOf_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw :
  ((orderOf x).factorizationLCMLeft (orderOf y)).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
hx₁ : orderOf x ≠ 0
hn : (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
⊢ (orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime
    (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))

Tactic:
rw [orderOf_pow_orderOf_div]

Premises used: orderOf_pow_orderOf_div
-- Module: Mathlib.GroupTheory.Exponent
Goal:
G : Type u
inst : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
rw : ((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
hx₁ : orderOf y ≠ 0
hn : (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
⊢ ((orderOf x).factorizationLCMLeft (orderOf y)).gcd
      (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y)))) =
    1

Tactic:
rw [orderOf_pow_orderOf_div]

Premises used: orderOf_pow_orderOf_div