awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : 0 < n
h1 : 1 ∉ periodicPts fun (x_1 : G) ↦ x * x_1
h' : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1
⊢ False

Tactic:
exact h1 ⟨n, h, h'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : 0 < orderOf x ↔ ¬orderOf x = 0
rw₁ rw₂ : orderOf x ≠ 0 ↔ ¬orderOf x = 0
⊢ 0 < orderOf x ↔ IsOfFinOrder x

Tactic:
rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

Premises used: iff_not_comm, orderOf_eq_zero_iff, Iff.mp, pos_iff_ne_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
β : Type u_5
inst : Monoid G
x : G
inst_1 : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
rw : ∀ (hx : 0 < orderOf x) (h : orderOf y ∣ orderOf x), 0 < orderOf y
⊢ IsOfFinOrder y

Tactic:
rw [← orderOf_pos_iff] at hx ⊢

Premises used: orderOf_pos_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
β : Type u_5
inst : Monoid G
x : G
inst_1 : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Tactic:
Nat.pos_of_dvd_of_pos h hx

Premises used: Nat.pos_of_dvd_of_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
β : Type u_5
inst : Monoid G
x : G
inst_1 : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Tactic:
exact Nat.pos_of_dvd_of_pos h hx

Premises used: Nat.pos_of_dvd_of_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
n0 : n ≠ 0
h : n < orderOf x
⊢ x ^ n ≠ 1

Tactic:
fun j =>
  not_isPeriodicPt_of_pos_of_lt_minimalPeriod n0 h ((isPeriodicPt_mul_iff_pow_eq_one x).mpr j)

Premises used: Iff.mpr, isPeriodicPt_mul_iff_pow_eq_one, Not, Function.not_isPeriodicPt_of_pos_of_lt_minimalPeriod
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
h rwa rwa₁ rwa₂ rwa₃ : x ^ n = 1
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1

Tactic:
rwa [isPeriodicPt_mul_iff_pow_eq_one]

Premises used: isPeriodicPt_mul_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
rw : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = 1
rw₁ : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = minimalPeriod.{u_1} (α := G) id 1
rw₂ rw₃ : minimalPeriod (fun (x : G) ↦ 1 * x) 1 = minimalPeriod (fun (x : G) ↦ 1 * x) 1
⊢ orderOf.{u_1} (G := G) 1 = 1

Tactic:
rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

Premises used: one_mul_eq_id, orderOf, Function.minimalPeriod_id
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = 1 ↔ x = 1
rw₁ : IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x = 1
rw₂ : x * 1 = 1 ↔ x = 1
rw₃ rw₄ : x = 1 ↔ x = 1
⊢ orderOf x = 1 ↔ x = 1

Tactic:
rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]

Premises used: Function.minimalPeriod_eq_one_iff_isFixedPt, orderOf, Function.IsFixedPt, mul_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Tactic:
simp [pow_add, pow_mul, pow_orderOf_eq_one]

Premises used: pow_add, pow_mul, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw rw₁ : x ^ n = x ^ n
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
rw [Nat.mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : x ^ n = 1
⊢ orderOf x ∣ n

Tactic:
IsPeriodicPt.minimalPeriod_dvd ((isPeriodicPt_mul_iff_pow_eq_one _).mpr h)

Premises used: Iff.mpr, Function.IsPeriodicPt.minimalPeriod_dvd, orderOf, isPeriodicPt_mul_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
rw : x ^ (n % orderOf x) = 1
rw₁ : HPow.hPow (β := ℕ) x 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ x ^ n = 1

Tactic:
rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero]

Premises used: pow_mod_orderOf, pow_zero, Nat.mod_eq_zero_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : (x ^ n) ^ orderOf x = 1
rw₁ : (x ^ orderOf x) ^ n = 1
rw₂ : HPow.hPow (α := G) 1 n = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := G) 1 1
⊢ orderOf (x ^ n) ∣ orderOf x

Tactic:
rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]

Premises used: one_pow, pow_right_comm, pow_orderOf_eq_one, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
⊢ Set.InjOn.{0, u_1} (β := G) (fun (x_1 : ℕ) ↦ x ^ x_1) (Set.Iio (orderOf x))

Tactic:
simpa only [mul_left_iterate_apply_one]
    using iterate_injOn_Iio_minimalPeriod (f := (x * ·)) (x := 1)

Premises used: Function.iterate_injOn_Iio_minimalPeriod, mul_left_iterate_apply_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
inst_1 : DecidableEq G
hx : IsOfFinOrder x
⊢ Membership.mem (γ := Submonoid G) (powers x) y ↔
    Membership.mem (γ := Finset G) (Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (orderOf x))) y

Tactic:
Finset.mem_range_iff_mem_finset_range_of_mod_eq' hx.orderOf_pos <| pow_mod_orderOf _

Premises used: IsOfFinOrder.orderOf_pos, Set.Mem, pow_mod_orderOf, setOf, Finset.mem_range_iff_mem_finset_range_of_mod_eq', Set.range
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
inst_1 : DecidableEq G
hx : IsOfFinOrder x
⊢ (↑(powers x) : Set G) = (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (orderOf x))) : Set G)

Tactic:
Set.ext fun _ ↦ hx.mem_powers_iff_mem_range_orderOf

Premises used: Set.ext, IsOfFinOrder.mem_powers_iff_mem_range_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
inl : ∀ (hle : a ≤ b), x ^ a = x ^ b
inr : ∀ (hle : b ≤ a), x ^ a = x ^ b
⊢ x ^ a = x ^ b

Tactic:
obtain hle | hle := le_total a b

Premises used: le_total
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : a ≤ b
inl : ∀ (c : ℕ) (h : a ≡ a + c [MOD n]) (hle : a ≤ a + c), x ^ a = x ^ (a + c)
⊢ x ^ a = x ^ b

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle

Premises used: le_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ n ∣ c

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
inl : ∀ (c : ℕ) (h : a ≡ a + n * c [MOD n]) (hle : a ≤ a + n * c), x ^ a = x ^ (a + n * c)
⊢ x ^ a = x ^ (a + c)

Tactic:
obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + n * c [MOD n]
hle : a ≤ a + n * c
⊢ x ^ a = x ^ (a + n * c)

Tactic:
simp [pow_add, pow_mul, hx]

Premises used: pow_add, pow_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
hle : b ≤ a
inr : ∀ (c : ℕ) (h : b + c ≡ b [MOD n]) (hle : b ≤ b + c), x ^ (b + c) = x ^ b
⊢ x ^ a = x ^ b

Tactic:
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hle

Premises used: le_iff_exists_add, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ n ∣ c

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
inr : ∀ (c : ℕ) (h : b + n * c ≡ b [MOD n]) (hle : b ≤ b + n * c), x ^ (b + n * c) = x ^ b
⊢ x ^ (b + c) = x ^ b

Tactic:
obtain ⟨c, rfl⟩ : n ∣ c := by simpa using h

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + n * c ≡ b [MOD n]
hle : b ≤ b + n * c
⊢ x ^ (b + n * c) = x ^ b

Tactic:
simp [pow_add, pow_mul, hx]

Premises used: pow_add, pow_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
rw : x ^ n = 1 ↔ orderOf x ∣ n
rw₁ rw₂ : x ^ n = 1 ↔ x ^ n = 1
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Tactic:
rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]

Premises used: Nat.modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
ψ : G →* H
x : G
h : HPow.hPow (α := H) ((ψ : (a : G) → H) x : H) (orderOf x) = 1
⊢ orderOf.{u_6} (G := H) ((ψ : (a : G) → H) x : H) ∣ orderOf x

Tactic:
apply orderOf_dvd_of_pow_eq_one

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
ψ : G →* H
x : G
h : Eq.{u_6 + 1} (α := H) ((ψ : (a : G) → H) 1 : H) (1 : H)
⊢ HPow.hPow (α := H) ((ψ : (a : G) → H) x : H) (orderOf x) = 1

Tactic:
rw [← map_pow, pow_orderOf_eq_one]

Premises used: map_pow, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
ψ : G →* H
x : G
⊢ Eq.{u_6 + 1} (α := H) ((ψ : (a : G) → H) 1 : H) (1 : H)

Tactic:
apply map_one

Premises used: map_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
pos : ∀ (h0 : orderOf x = 0), ∃ (m : ℕ), (x ^ n) ^ m = x
neg : ∀ (h0 : ¬orderOf x = 0), ∃ (m : ℕ), (x ^ n) ^ m = x
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
by_cases h0 : orderOf x = 0

Premises used: orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ n = 1

Tactic:
rw [h0, coprime_zero_right] at h

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
h₁ : n = 1
⊢ orderOf x = 0

Tactic:
rw [h0, coprime_zero_right] at h

Premises used: Nat.coprime_zero_right
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
rw : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) x 1) 1 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
rw₂ rw₃ : x = x
⊢ HPow.hPow (β := ℕ) (x ^ n) 1 = x

Tactic:
rw [h, pow_one, pow_one]

Premises used: pow_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
exact ⟨1, by rw [h, pow_one, pow_one]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
pos : ∀ (h1 : orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
neg : ∀ (h1 : ¬orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
by_cases h1 : orderOf x = 1

Premises used: orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := G) 1 n) 0 = 1
rw₁ : HPow.hPow (α := G) (β := ℕ) 1 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := G) 1 1
⊢ HPow.hPow (β := ℕ) (x ^ n) 0 = x

Tactic:
rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]

Premises used: one_pow, Iff.mp, orderOf_eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ 1 < orderOf x

Tactic:
lia
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
neg : ∀ (m : ℕ) (h : n * m % orderOf x = 1), ∃ (m : ℕ), (x ^ n) ^ m = x
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by lia)

Premises used: Nat.exists_mul_mod_eq_one_of_coprime
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
rw : x ^ (n * m) = x
rw₁ : x ^ (n * m % orderOf x) = x
rw₂ : HPow.hPow (β := ℕ) x 1 = x
rw₃ rw₄ : x = x
⊢ (x ^ n) ^ m = x

Tactic:
rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]

Premises used: pow_mod_orderOf, pow_mul, pow_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h_1 : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ (m : ℕ), (x ^ n) ^ m = x

Tactic:
exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
obtain : ∀ (a : ℕ) (ha : n = orderOf x * a), orderOf x = n
⊢ orderOf x = n

Tactic:
obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)

Premises used: orderOf_dvd_of_pow_eq_one, exists_eq_mul_right_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
this : a = 1
⊢ orderOf x = n

Tactic:
simp [this, ha]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
suffices : a = 1
⊢ orderOf x = n

Tactic:
suffices a = 1 by simp [this, ha]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
by_contra : ∀ (h : ¬a = 1), False
⊢ a = 1

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ ∃ (b : ℕ), a = b * a.minFac

Tactic:
exists_eq_mul_left_of_dvd a.minFac_dvd

Premises used: Nat.minFac_dvd, exists_eq_mul_left_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
obtain : ∀ (b : ℕ) (hb : a = b * a.minFac), a.minFac ∣ n
⊢ a.minFac ∣ n

Tactic:
obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd

Premises used: Nat.minFac, Nat.minFac_dvd, exists_eq_mul_left_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * a.minFac
⊢ n = orderOf x * b * a.minFac

Tactic:
rw [hb, ← mul_assoc] at ha

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
b : ℕ
hb : a = b * a.minFac
ha₁ : n = orderOf x * b * a.minFac
⊢ a = b * a.minFac

Tactic:
rw [hb, ← mul_assoc] at ha

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
Dvd.intro_left (orderOf x * b) ha.symm

Premises used: HMul.hMul, Dvd.intro_left, orderOf, Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
exact Dvd.intro_left (orderOf x * b) ha.symm

Premises used: HMul.hMul, Dvd.intro_left, orderOf, Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
⊢ a.minFac ∣ n

Tactic:
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ False

Tactic:
hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_

Premises used: Nat.minFac, Nat.minFac_prime
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
refine : x ^ (n / a.minFac) = 1
⊢ False

Tactic:
refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_

Premises used: Nat.minFac, Nat.minFac_prime
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
rw : a.minFac ∣ a
rw₁ : IsOfFinOrder x
⊢ x ^ (n / a.minFac) = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]

Premises used: IsOfFinOrder.orderOf_pos, Nat.mul_dvd_mul_iff_left, mul_comm, Nat.dvd_div_iff_mul_dvd, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

Tactic:
Nat.minFac_dvd a

Premises used: Nat.minFac_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

Tactic:
exact Nat.minFac_dvd a

Premises used: Nat.minFac_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
rw : ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
Exists.intro n (id ⟨hn, hx⟩)

Premises used: id, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
exact Exists.intro n (id ⟨hn, hx⟩)

Premises used: id, Exists.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
H : Type u_6
inst_1 : Monoid H
y : H
simp_rw :
  orderOf x = orderOf y ↔ ∀ (n : ℕ), IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) n 1 ↔ IsPeriodicPt (fun (x : H) ↦ y * x) n 1
simp_rw₁ : orderOf x = orderOf y ↔ minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = minimalPeriod (fun (x : H) ↦ y * x) 1
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Tactic:
simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]

Premises used: Function.minimalPeriod_eq_minimalPeriod_iff, orderOf, isPeriodicPt_mul_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_6 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
simp_rw : ∀ (n : ℕ), HPow.hPow (α := H) ((f : (a : G) → H) x : H) n = 1 ↔ x ^ n = 1
simp_rw₁ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) (1 : H) ↔ x ^ n = 1
simp_rw₂ : ∀ (n : ℕ), Eq.{u_6 + 1} (α := H) ((f : (a : G) → H) (x ^ n) : H) ((f : (a : G) → H) 1 : H) ↔ x ^ n = 1
simp_rw₃ : ∀ (n : ℕ), True
⊢ orderOf.{u_6} (G := H) ((f : (a : G) → H) x : H) = orderOf x

Tactic:
simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]

Premises used: Function.Injective.eq_iff, MonoidHom.map_one, forall_const, orderOf_eq_orderOf_iff, MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Type u_6
inst_1 : Monoid H
e : G ≃* H
x : G
⊢ orderOf.{u_6} (G := H) ((e : (a : G) → H) x : H) = orderOf x

Tactic:
orderOf_injective e.toMonoidHom e.injective x

Premises used: MulEquiv.toMonoidHom, MulEquiv.injective, orderOf_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
x : G
inst_1 : Monoid H
f : G →* H
hf : Injective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
rw : 0 < orderOf.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x
rw₁ : 0 < orderOf x ↔ IsOfFinOrder x
rw₂ rw₃ : 0 < orderOf x ↔ 0 < orderOf x
⊢ IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) x : H) ↔ IsOfFinOrder x

Tactic:
rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]

Premises used: orderOf_pos_iff, orderOf_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
H : Submonoid G
y : ↥H
⊢ orderOf (↑y : G) = orderOf y

Tactic:
orderOf_injective H.subtype Subtype.coe_injective y

Premises used: Subtype.coe_injective, Submonoid.subtype, orderOf_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
y : Gˣ
⊢ orderOf (↑y : G) = orderOf y

Tactic:
orderOf_injective (Units.coeHom G) Units.val_injective y

Premises used: Units.coeHom, Units.val_injective, orderOf_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Subsingleton.{u_1 + 1} Gˣ
x : G
h : IsUnit x
⊢ orderOf x = 1

Tactic:
simp [isUnit_iff_eq_one.mp h]

Premises used: isUnit_iff_eq_one, Iff.mp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
u : Gˣ
⊢ IsOfFinOrder (↑u : G) ↔ IsOfFinOrder u

Tactic:
Units.coeHom_injective.isOfFinOrder_iff

Premises used: Function.Injective.isOfFinOrder_iff, Units.coeHom_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x_1 y : G
n m : ℕ
M : Type u_6
inst_1 : Monoid M
x : M
hx : IsOfFinOrder x
⊢ 1 ≤ orderOf x

Tactic:
hx.orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, Nat.lt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Monoid G
a b x_1 y : G
n m : ℕ
M : Type u_6
inst_1 : Monoid M
x : M
hx : IsOfFinOrder x
⊢ 1 ≤ orderOf x

Tactic:
exact hx.orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos