awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : x ^ (orderOf x - 1 + 1) = 1
rw₁ : x ^ orderOf x = 1
rw₂ rw₃ : Eq.{u_6 + 1} (α := M) 1 1
⊢ x * x ^ (orderOf x - 1) = 1

Tactic:
rw [← _root_.pow_succ', tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

Premises used: tsub_add_cancel_of_le, pow_orderOf_eq_one, pow_succ'
-- 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
rw : x ^ (orderOf x - 1 + 1) = 1
rw₁ : x ^ orderOf x = 1
rw₂ rw₃ : Eq.{u_6 + 1} (α := M) 1 1
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

Premises used: pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
M : Type u_6
inst : Monoid M
x : M
hx : IsOfFinOrder x
⊢ IsUnit x

Tactic:
⟨hx.unit, rfl⟩

Premises used: IsUnit, IsOfFinOrder.unit, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : n ≠ 0
rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
rw₁ rw₂ : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n

Tactic:
rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]

Premises used: Function.minimalPeriod_iterate_eq_div_gcd, mul_left_iterate
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
rw : orderOf x / (orderOf x).gcd n = orderOf x / n
rw₁ rw₂ : orderOf x / n = orderOf x / n
⊢ orderOf (x ^ n) = orderOf x / n

Tactic:
rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]

Premises used: orderOf_pow', Nat.gcd_eq_right
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
rw : orderOf x / n ≠ 0
⊢ orderOf (x ^ (orderOf x / n)) = n

Tactic:
rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]

Premises used: orderOf_pow_of_dvd, Nat.div_dvd_of_dvd, Nat.div_div_self
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n * n ≠ 0

Tactic:
rw [← Nat.div_mul_cancel hn] at hx

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
hx₁ : orderOf x / n * n ≠ 0
⊢ n ∣ orderOf x

Tactic:
rw [← Nat.div_mul_cancel hn] at hx

Premises used: Nat.div_mul_cancel
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
left_ne_zero_of_mul hx

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
exact left_ne_zero_of_mul hx

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
rw : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod.{u_1} (α := G) (fun (x_1 : G) ↦ x * x_1)^[n] 1
rw₁ rw₂ : minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 = minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1
⊢ minimalPeriod (fun (x_1 : G) ↦ x ^ n * x_1) 1 =
    minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 / (minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1).gcd n

Tactic:
rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]

Premises used: mul_left_iterate, Function.minimalPeriod_iterate_eq_div_gcd'
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
pos : ∀ (hg : IsOfFinOrder y), orderOf (y ^ m) = orderOf y
neg : ∀ (hg : ¬IsOfFinOrder y), orderOf (y ^ m) = orderOf y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
by_cases hg : IsOfFinOrder y

Premises used: IsOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
pos : orderOf y / (orderOf y).gcd m = orderOf y
pos₁ : orderOf y / 1 = orderOf y
pos₂ pos₃ : orderOf y = orderOf y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]

Premises used: IsOfFinOrder.orderOf_pow, Nat.div_one, Nat.Coprime.gcd_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
neg : orderOf (HPow.hPow (β := ℕ) y 1) = orderOf y
neg₁ neg₂ : orderOf y = orderOf y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]

Premises used: Eq.rec, pow_one, Nat.coprime_zero_left, Iff.mp, orderOf_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card.{u_1} (↑(↑(powers a) : Set G) : Type u_1) ≤ orderOf a

Tactic:
simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range]
    using Finset.card_image_le (s := Finset.range (orderOf a))

Premises used: Finset.card_range, Finset.card_image_le, IsOfFinOrder.powers_eq_image_range_orderOf, Nat.Iio_eq_range
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card.{u_1} (↑(↑(powers a) : Set G) : Type u_1) ≤ orderOf a

Tactic:
classical
  simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range]
    using Finset.card_image_le (s := Finset.range (orderOf a))

Premises used: Finset.card_range, Finset.card_image_le, Nat.Iio_eq_range
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
rw : (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite
⊢ (↑(powers a) : Set G).Finite

Tactic:
rw [ha.powers_eq_image_range_orderOf]

Premises used: IsOfFinOrder.powers_eq_image_range_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite

Tactic:
Finset.finite_toSet _

Premises used: Finset.finite_toSet
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite

Tactic:
exact Finset.finite_toSet _

Premises used: Finset.finite_toSet
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
a : G
ha : IsOfFinOrder a
classical classical₁ classical₂ classical₃ :
  (↑(Finset.image (fun (x : ℕ) ↦ a ^ x) (Finset.range (orderOf a))) : Set G).Finite
⊢ (↑(powers a) : Set G).Finite

Tactic:
classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

Premises used: Finset.finite_toSet
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
rw : minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)
⊢ orderOf (x * y) ∣ (orderOf x).lcm (orderOf y)

Tactic:
rw [orderOf, ← comp_mul_left]

Premises used: comp_mul_left, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Tactic:
Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Premises used: Commute.function_commute_mul_left, Function.Commute.minimalPeriod_of_comp_dvd_lcm, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Tactic:
exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Premises used: Commute.function_commute_mul_left, Function.Commute.minimalPeriod_of_comp_dvd_lcm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
pos : ∀ (h0 : orderOf x = 0), orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
neg : ∀ (h0 : ¬orderOf x = 0), orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
by_cases h0 : orderOf x = 0

Premises used: orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
pos : orderOf y ∣ 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
rw [h0, lcm_zero_left]

Premises used: Nat.lcm_zero_left
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
rw : orderOf (x ^ (orderOf x).pred * (x * y))
| orderOf y

Tactic:
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]

Premises used: Nat.succ_pred_eq_of_pos, pow_succ, mul_assoc, pow_orderOf_eq_one, Nat.pos_of_ne_zero, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
neg : orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]

Premises used: Nat.succ_pred_eq_of_pos, pow_succ, mul_assoc, pow_orderOf_eq_one, Nat.pos_of_ne_zero, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
(((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
      (Nat.lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (Nat.dvd_lcm_left _ _), Nat.dvd_lcm_right _ _⟩)

Premises used: Iff.mpr, Commute.mul_right, orderOf_pow_dvd, Commute.pow_left, Nat.dvd_lcm_left, Commute.orderOf_mul_dvd_lcm, Commute.refl, Nat.lcm_dvd_iff, And.intro, Nat.dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
exact
    (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
      (Nat.lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (Nat.dvd_lcm_left _ _), Nat.dvd_lcm_right _ _⟩)

Premises used: Iff.mpr, Commute.mul_right, orderOf_pow_dvd, Commute.pow_left, Nat.dvd_lcm_left, Commute.orderOf_mul_dvd_lcm, Commute.refl, Nat.lcm_dvd_iff, And.intro, Nat.dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
⊢ orderOf (x * y) ∣ orderOf x * orderOf y

Tactic:
dvd_trans h.orderOf_mul_dvd_lcm (Nat.lcm_dvd_mul _ _)

Premises used: dvd_trans, Commute.orderOf_mul_dvd_lcm, Nat.lcm_dvd_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
rw : minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 = orderOf x * orderOf y
⊢ orderOf (x * y) = orderOf x * orderOf y

Tactic:
rw [orderOf, ← comp_mul_left]

Premises used: comp_mul_left, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 = orderOf x * orderOf y

Tactic:
h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

Premises used: Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime, Commute.function_commute_mul_left, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod.{u_1} (α := G) ((fun (x_1 : G) ↦ x * x_1) ∘ fun (x : G) ↦ y * x) 1 = orderOf x * orderOf y

Tactic:
exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

Premises used: Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime, Commute.function_commute_mul_left
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hx : IsOfFinOrder x
hy : IsOfFinOrder y
⊢ IsOfFinOrder (x * y)

Tactic:
orderOf_pos_iff.mp <|
    pos_of_dvd_of_pos h.orderOf_mul_dvd_mul_orderOf <| mul_pos hx.orderOf_pos hy.orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, Commute.orderOf_mul_dvd_mul_orderOf, mul_pos, orderOf_pos_iff, Iff.mp, Nat.pos_of_dvd_of_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
⊢ 0 < orderOf y

Tactic:
have hoy := hy.orderOf_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
⊢ orderOf x ∣ orderOf y

Tactic:
have hxy := dvd_of_forall_prime_mul_dvd hdvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
hx : (x * y) ^ orderOf y = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → (x * y) ^ (orderOf y / p) ≠ 1
⊢ orderOf (x * y) = orderOf y

Tactic:
apply orderOf_eq_of_pow_and_pow_div_prime hoy

Premises used: orderOf_eq_of_pow_and_pow_div_prime
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
hx : orderOf (x * y) ∣ orderOf y
⊢ (x * y) ^ orderOf y = 1

Tactic:
simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]

Premises used: Ne, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → (x * y) ^ (orderOf y / p) ≠ 1

Tactic:
simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]

Premises used: Ne, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

Tactic:
h.orderOf_mul_dvd_lcm.trans (Nat.lcm_dvd hxy dvd_rfl)

Premises used: Commute.orderOf_mul_dvd_lcm, Nat.lcm_dvd, dvd_rfl, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

Tactic:
exact h.orderOf_mul_dvd_lcm.trans (Nat.lcm_dvd hxy dvd_rfl)

Premises used: Commute.orderOf_mul_dvd_lcm, Nat.lcm_dvd, dvd_rfl, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p

Tactic:
fun p hp hpy hd => hp.ne_one ?_

Premises used: Nat.Prime.ne_one, Not
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
hd : ∀ (p : ℕ) (hp : Nat.Prime p) (hpy : p ∣ orderOf y) (hd : orderOf (x * y) ∣ orderOf y / p), p = 1
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p

Tactic:
refine fun p hp hpy hd => hp.ne_one ?_
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
hd₁ : orderOf y ∣ orderOf y / p
⊢ p = 1

Tactic:
rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]

Premises used: mul_dvd_mul_iff_right, Nat.dvd_one, LT.lt.ne', Nat.dvd_div_iff_mul_dvd, one_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
⊢ orderOf y ∣ orderOf y / p

Tactic:
(orderOf_dvd_lcm_mul h).trans (Nat.lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)

Premises used: Iff.mpr, Commute.orderOf_dvd_lcm_mul, Nat.lcm_dvd, Nat.dvd_div_iff_mul_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
hd₁ : p * orderOf x ∣ orderOf y
⊢ orderOf y ∣ orderOf y / p

Tactic:
refine (orderOf_dvd_lcm_mul h).trans (Nat.lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)

Premises used: Iff.mpr, Commute.orderOf_dvd_lcm_mul, Nat.lcm_dvd, Nat.dvd_div_iff_mul_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
pos : ∀ (h : p ∣ orderOf x), p * orderOf x ∣ orderOf y
neg : ∀ (h : ¬p ∣ orderOf x), p * orderOf x ∣ orderOf y
⊢ p * orderOf x ∣ orderOf y

Tactic:
by_cases h : p ∣ orderOf x

Premises used: orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h_1 : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y

Tactic:
hdvd p hp h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h_1 : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : ¬p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y

Tactic:
(hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy

Premises used: Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Nat.Coprime.mul_dvd_of_dvd_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h_1 : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
p : ℕ
hp : Nat.Prime p
hpy : p ∣ orderOf y
hd : orderOf (x * y) ∣ orderOf y / p
h : p ∣ orderOf x
⊢ p * orderOf x ∣ orderOf y

Tactic:
exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x y : G
h : Commute x y
hx : IsOfFinOrder x
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x
⊢ orderOf (x * y) = orderOf x

Tactic:
simpa [h.eq] using
    orderOf_mul_eq_right_of_forall_prime_mul_dvd (x := y) (y := x) h.symm hx hdvd

Premises used: Commute.symm, Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd, Commute.eq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
rw : minimalPeriod (fun (x_1 : G) ↦ x * x_1) 1 = p ↔ x ^ p = 1 ∧ x ≠ 1
rw₁ : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₂ : x ^ p = 1 ∧ ¬IsFixedPt (fun (x_1 : G) ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₃ : x ^ p = 1 ∧ ¬x * 1 = 1 ↔ x ^ p = 1 ∧ x ≠ 1
rw₄ rw₅ : x ^ p = 1 ∧ ¬x = 1 ↔ x ^ p = 1 ∧ x ≠ 1
⊢ orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1

Tactic:
rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]

Premises used: orderOf, isPeriodicPt_mul_iff_pow_eq_one, Function.minimalPeriod_eq_prime_iff, Function.IsFixedPt, mul_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
hg : x ^ p = 1
hg1 : x ≠ 1
⊢ orderOf x = p

Tactic:
orderOf_eq_prime_iff.mpr ⟨hg, hg1⟩

Premises used: Iff.mpr, orderOf_eq_prime_iff, And.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
hk : ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ n) 1
hk1 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ (n + 1)) 1
⊢ orderOf x = p ^ (n + 1)

Tactic:
apply minimalPeriod_eq_prime_pow

Premises used: Function.minimalPeriod_eq_prime_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin : x ^ p ^ (n + 1) = 1
hk hk₁ hk₂ hk₃ : ¬x ^ p ^ n = 1
⊢ ¬IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ 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
x : G
n p : ℕ
hp : Fact (Nat.Prime p)
hnot : ¬x ^ p ^ n = 1
hfin hk1 hk1₁ hk1₂ hk1₃ : x ^ p ^ (n + 1) = 1
⊢ IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) (p ^ (n + 1)) 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
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (k : ℕ), orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
rw : x ^ orderOf x = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ x ^ p ^ k = 1

Tactic:
rw [← hk, pow_orderOf_eq_one]

Premises used: pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (m : ℕ), x ^ p ^ m = 1
w : ℕ
hm : x ^ p ^ w = 1
obtain : ∀ k ≤ w, ∀ (hk : orderOf x = p ^ k), ∃ (k : ℕ), orderOf x = p ^ k
⊢ ∃ (k : ℕ), orderOf x = p ^ k

Tactic:
obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)

Premises used: orderOf_dvd_of_pow_eq_one, Fact.elim, Iff.mp, Nat.dvd_prime_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (m : ℕ), x ^ p ^ m = 1
w : ℕ
hm : x ^ p ^ w = 1
k : ℕ
left : k ≤ w
hk : orderOf x = p ^ k
⊢ ∃ (k : ℕ), orderOf x = p ^ k

Tactic:
⟨k, hk⟩

Premises used: Exists.intro