awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
refine_1 : (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬IsOfFinOrder x
refine_2 :
  ∀ (h : ¬IsOfFinOrder x) (n m : ℤ) (hnm : Eq.{u_1 + 1} (α := G) ((fun (n : ℤ) ↦ x ^ n) n) ((fun (n : ℤ) ↦ x ^ n) m)),
    n = m
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨?_, fun h n m hnm => ?_⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
refine_1 : (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ Eq.{u_1 + 1} (α := G) ((fun (n : ℤ) ↦ x ^ n) (↑n : ℤ)) ((fun (n : ℤ) ↦ x ^ n) 0)

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False

Tactic:
exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)

Premises used: Iff.mpr, LT.lt.ne', Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : Eq.{u_1 + 1} (α := G) ((fun (n : ℤ) ↦ x ^ n) n) ((fun (n : ℤ) ↦ x ^ n) m)
refine_2 : ∀ (hnm : n ≡ m [ZMOD (↑(orderOf x) : ℤ)]), n = m
refine_2₁ : ∀ (hnm : n ≡ m [ZMOD (↑0 : ℤ)]), n = m
refine_2₂ : ∀ (hnm : n ≡ m [ZMOD 0]), n = m
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : ∀ (hnm : n = m), n = m
⊢ n = m

Tactic:
rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm

Premises used: Iff.mpr, Int.modEq_zero_iff, orderOf_eq_zero_iff, Nat.cast_zero, zpow_eq_zpow_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ Eq (α := Subgroup G) (zpowers x) (zpowers x)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
⊢ Eq (α := Subgroup G) (zpowers x) (zpowers x⁻¹)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
refine : ∀ (h : Eq (α := Subgroup G) (zpowers x) (zpowers y)), x = y ∨ x⁻¹ = y
⊢ Eq (α := Subgroup G) (zpowers x) (zpowers y) ↔ x = y ∨ x⁻¹ = y

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
⊢ Membership.mem (γ := Subgroup G) (zpowers y) x

Tactic:
simp [← h]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
⊢ Membership.mem (γ := Subgroup G) (zpowers y) x

Tactic:
have hx_mem : x ∈ zpowers y := by simp [← h]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
hx_mem : Membership.mem (γ := Subgroup G) (zpowers y) x
⊢ Membership.mem (γ := Subgroup G) (zpowers x) y

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
hx_mem : Membership.mem (γ := Subgroup G) (zpowers y) x
⊢ Membership.mem (γ := Subgroup G) (zpowers x) y

Tactic:
have hy_mem : y ∈ zpowers x := by simp [h]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
hx_mem : Membership.mem (γ := Subgroup G) (zpowers y) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) y
obtain :
  ∀ (k : ℤ) (h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k)))
    (hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x)
    (hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)), x = x ^ k ∨ x⁻¹ = x ^ k
⊢ x = y ∨ x⁻¹ = y

Tactic:
obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp hy_mem

Premises used: Iff.mp, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
obtain : ∀ (l : ℤ) (hl : (x ^ k) ^ l = x), x = x ^ k ∨ x⁻¹ = x ^ k
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
obtain ⟨l, hl⟩ := mem_zpowers_iff.mp hx_mem

Premises used: Iff.mp, Subgroup.mem_zpowers_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : (x ^ k) ^ l = x
⊢ x ^ (k * l) = x

Tactic:
rw [← zpow_mul] at hl

Premises used: zpow_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : x ^ (k * l) = x
⊢ x ^ (k * l) = HPow.hPow (β := ℤ) x 1

Tactic:
nth_rewrite 2 [← zpow_one x] at hl

Premises used: zpow_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : x ^ (k * l) = HPow.hPow (β := ℤ) x 1
⊢ k * l = 1

Tactic:
have h1 := (injective_zpow_iff_not_isOfFinOrder.mpr hx) hl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : x ^ (k * l) = HPow.hPow (β := ℤ) x 1
h1 : k * l = 1
inl : ∀ (h : k = 1 ∧ l = 1), x = x ^ k ∨ x⁻¹ = x ^ k
inr : ∀ (h : k = -1 ∧ l = -1), x = x ^ k ∨ x⁻¹ = x ^ k
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h)

Premises used: Int.mul_eq_one_iff_eq_one_or_neg_one, Iff.mp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h_1 : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : x ^ (k * l) = HPow.hPow (β := ℤ) x 1
h1 : k * l = 1
h : k = 1 ∧ l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
simp [h.1]

Premises used: And.left
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h_1 : Eq (α := Subgroup G) (zpowers x) (zpowers (x ^ k))
hx_mem : Membership.mem (γ := Subgroup G) (zpowers (x ^ k)) x
hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
l : ℤ
hl : x ^ (k * l) = HPow.hPow (β := ℤ) x 1
h1 : k * l = 1
h : k = -1 ∧ l = -1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
simp [h.1]

Premises used: And.left
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
simp_rw₅ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), k * x ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
simp_rw₆ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = HPow.hPow (β := ℤ) g 1
simp_rw₇ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = g
simp_rw₈ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (g ^ k) ^ x = g
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1

Tactic:
simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]

Premises used: Int.modEq_iff_dvd, Int.sub_eq_iff_eq_add', dvd_def, zpow_mul, Nat.dvd_one, zpow_one, Int.gcd_dvd_iff, zpow_eq_zpow_iff_modEq, Subgroup.mem_zpowers_iff, Nat.cast_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
g : G
k : ℕ
rw : Membership.mem (γ := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑k : ℤ))) g ↔ k.gcd (orderOf g) = 1
rw₁ : Int.gcd (↑k : ℤ) (↑(orderOf g) : ℤ) = 1 ↔ k.gcd (orderOf g) = 1
rw₂ rw₃ : k.gcd (orderOf g) = 1 ↔ k.gcd (orderOf g) = 1
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (orderOf g) = 1

Tactic:
rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]

Premises used: zpow_natCast, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
obtain : ∀ (w : ℕ) (hw1 : w > 0) (hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1), ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1
⊢ ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1

Tactic:
obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x

Premises used: isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
⊢ ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1

Tactic:
⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩

Premises used: Iff.mpr, Int.natCast_ne_zero, ne_of_gt, Nat.cast, Exists.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
refine : HPow.hPow (β := ℤ) x (↑w : ℤ) = 1
⊢ ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1

Tactic:
refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
rw : x ^ w = 1
⊢ HPow.hPow (β := ℤ) x (↑w : ℤ) = 1

Tactic:
rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
⊢ x ^ w = 1

Tactic:
(isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

Premises used: isPeriodicPt_mul_iff_pow_eq_one, Iff.mp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
⊢ x ^ w = 1

Tactic:
exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

Premises used: isPeriodicPt_mul_iff_pow_eq_one, Iff.mp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : Finite G
⊢ Membership.mem (γ := Submonoid G) (powers x) y ↔ Membership.mem (γ := Subgroup G) (zpowers x) y

Tactic:
(isOfFinOrder_of_finite _).mem_powers_iff_mem_zpowers

Premises used: IsOfFinOrder.mem_powers_iff_mem_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
⊢ (↑(powers x) : Set G) = (↑(zpowers x) : Set G)

Tactic:
(isOfFinOrder_of_finite _).powers_eq_zpowers

Premises used: IsOfFinOrder.powers_eq_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : Finite G
inst_2 : DecidableEq G
⊢ Membership.mem (γ := Subgroup G) (zpowers x) y ↔
    Membership.mem (γ := Finset G) (Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (orderOf x))) y

Tactic:
(isOfFinOrder_of_finite _).mem_zpowers_iff_mem_range_orderOf

Premises used: IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : Finite G
h : orderOf x = orderOf y
n : ℕ
rw :
  Eq (α := Fin (orderOf y))
    ((finCongr h : (a : Fin (orderOf x)) → Fin (orderOf y)) ⟨n % orderOf x, ⋯⟩ : Fin (orderOf y))
    (⟨n % orderOf y, ⋯⟩ : Fin (orderOf y))
⊢ Eq (α := ↥(zpowers y))
    ((zpowersEquivZPowers h : (a : ↥(zpowers x)) → ↥(zpowers y))
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ n) ⋯) :
      ↥(zpowers y))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers y) x) (y ^ n) ⋯ : ↥(zpowers y))

Tactic:
rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivZPowers_symm_apply]

Premises used: finEquivZPowers_symm_apply, Equiv.trans_apply, zpowersEquivZPowers, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ Eq (α := Fin (orderOf y))
    ((finCongr h : (a : Fin (orderOf x)) → Fin (orderOf y)) ⟨n % orderOf x, ⋯⟩ : Fin (orderOf y))
    (⟨n % orderOf y, ⋯⟩ : Fin (orderOf y))

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
s : Set G
⊢ ∀ x ∈ s, IsOfFinOrder x

Tactic:
simp [isOfFinOrder_of_finite]

Premises used: isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
⊢ card.{u_1} ↥(zpowers x) = orderOf x

Tactic:
(Fintype.card_eq.2 ⟨finEquivZPowers <| isOfFinOrder_of_finite _⟩).symm.trans <|
    Fintype.card_fin (orderOf x)

Premises used: Iff.mpr, Fintype.card_fin, finEquivZPowers, Fintype.card_eq, Nonempty.intro, orderOf, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
rw : orderOf a ≤ k
⊢ card.{u_1} ↥(zpowers a) ≤ k

Tactic:
rw [Fintype.card_zpowers]

Premises used: Fintype.card_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k

Tactic:
apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

Premises used: orderOf_le_of_pow_eq_one, Ne.bot_lt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
h : card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
⊢ orderOf x ∣ card G

Tactic:
use Fintype.card (G ⧸ zpowers x)

Premises used: Fintype.card, HasQuotient.Quotient, Subgroup.zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
h : card G = card.{u_1} ↥(zpowers x) * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
h₁ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x)) * card.{u_1} ↥(zpowers x)
h₂ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x) × ↥(zpowers x))
h₃ h₄ : card G = card G
⊢ card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))

Tactic:
rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]

Premises used: Fintype.card_congr, Subgroup.groupEquivQuotientProdSubgroup, Fintype.card_prod, mul_comm, Fintype.card_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
x : G
inl : ∀ (h : Fintype G), orderOf x ∣ Nat.card G
inr : ∀ (h : Infinite G), orderOf x ∣ Nat.card G
⊢ orderOf x ∣ Nat.card G

Tactic:
obtain h | h := fintypeOrInfinite G

Premises used: fintypeOrInfinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
x : G
h : Fintype G
⊢ orderOf x ∣ Nat.card G

Tactic:
simp only [Nat.card_eq_fintype_card, orderOf_dvd_card]

Premises used: orderOf_dvd_card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
x : G
h : Infinite G
⊢ orderOf x ∣ Nat.card G

Tactic:
simp only [card_eq_zero_of_infinite, dvd_zero]

Premises used: dvd_zero, Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card.{u_6} ↥s

Tactic:
simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
s : Subgroup G
hs : (↑s : Set G).Finite
x : G
hx : x ∈ s
⊢ orderOf x ≤ Nat.card.{u_6} ↥s

Tactic:
le_of_dvd (Nat.card_pos_iff.2 <| ⟨(OneMemClass.coe_nonempty s).to_subtype, hs.to_subtype⟩) <|
    s.orderOf_dvd_natCard hx

Premises used: Iff.mpr, OneMemClass.coe_nonempty, Set.Nonempty.to_subtype, Nat.card_pos_iff, Set.Finite.to_subtype, And.intro, Subgroup.orderOf_dvd_natCard, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
s : Submonoid G
hs : (↑s : Set G).Finite
x : G
hx : x ∈ s
rw : Nat.card.{u_6} ↥(powers x) ≤ Nat.card.{u_6} ↥s
⊢ orderOf x ≤ Nat.card.{u_6} ↥s

Tactic:
rw [← Nat.card_submonoidPowers]

Premises used: Nat.card_submonoidPowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
s : Submonoid G
hs : (↑s : Set G).Finite
x : G
hx : x ∈ s
⊢ Nat.card.{u_6} ↥(powers x) ≤ Nat.card.{u_6} ↥s

Tactic:
Nat.card_mono hs <| powers_le.2 hx

Premises used: Iff.mpr, Nat.card_mono, Submonoid.powers_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
s : Submonoid G
hs : (↑s : Set G).Finite
x : G
hx : x ∈ s
⊢ Nat.card.{u_6} ↥(powers x) ≤ Nat.card.{u_6} ↥s

Tactic:
exact Nat.card_mono hs <| powers_le.2 hx

Premises used: Iff.mpr, Nat.card_mono, Submonoid.powers_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
x : G
⊢ x ^ Nat.card G = 1

Tactic:
orderOf_dvd_iff_pow_eq_one.mp <| orderOf_dvd_natCard _

Premises used: orderOf_dvd_natCard, Iff.mp, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
rw : x ^ Nat.card G = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ x ^ card G = 1

Tactic:
rw [← Nat.card_eq_fintype_card, pow_card_eq_one']

Premises used: pow_card_eq_one', Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
n : ℕ
⊢ x ^ n.gcd (card G) = 1 ↔ x ^ n = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
rw : Eq (α := G ⧸ H) (↑(g ^ H.index) : G ⧸ H) 1
rw₁ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) H.index = 1
rw₂ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) (Nat.card.{u_6} (G ⧸ H)) = 1
rw₃ rw₄ : Eq.{u_6 + 1} (α := G ⧸ H) 1 1
⊢ g ^ H.index ∈ H

Tactic:
rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

Premises used: pow_card_eq_one', QuotientGroup.mk_pow, Subgroup.index, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
K : Subgroup G
g : G
hg : g ∈ K
⊢ g ^ H.relIndex K ∈ H

Tactic:
pow_index_mem (H.subgroupOf K) ⟨g, hg⟩

Premises used: Subgroup.subgroupOf, Set.Mem, setOf, Subgroup.pow_index_mem, Subgroup.relIndex, Subtype.mk, Set.preimage
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℕ
rw : a ^ n = a ^ (n % card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % card G)
rw₂ : a ^ (n % card G % orderOf a) = a ^ (n % card G)
rw₃ rw₄ : a ^ (n % card G) = a ^ (n % card G)
⊢ a ^ (n % card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

Premises used: pow_mod_orderOf, orderOf_dvd_card, eq_comm, Nat.mod_mod_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
rw₂ : a ^ (n % (↑(card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
rw₃ rw₄ : a ^ (n % (↑(card G) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
⊢ a ^ (n % (↑(card G) : ℤ)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]

Premises used: Iff.mpr, zpow_mod_orderOf, orderOf_dvd_card, eq_comm, Int.emod_emod_of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
a : G
n : ℕ
rw : a ^ n = a ^ (n % Nat.card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % Nat.card G)
rw₂ : a ^ (n % Nat.card G % orderOf a) = a ^ (n % Nat.card G)
rw₃ rw₄ : a ^ (n % Nat.card G) = a ^ (n % Nat.card G)
⊢ a ^ (n % Nat.card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

Premises used: pow_mod_orderOf, eq_comm, Nat.mod_mod_of_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : Group G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(Nat.card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
rw₂ : a ^ (n % (↑(Nat.card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
rw₃ rw₄ : a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
⊢ a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]

Premises used: Iff.mpr, zpow_mod_orderOf, eq_comm, Int.emod_emod_of_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G_1 : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Group G_1
x_1 y : G_1
inst_1 : Fintype G_1
x : G_1
n : ℕ
G : Type u_6
inst_2 : Group G
h : (Nat.card G).Coprime n
g : G
⊢ Eq.{u_6 + 1} (α := G) ((fun (x : ℤ) ↦ g ^ x) (↑((Nat.card G).gcd n) : ℤ))
    ((fun (x : ℤ) ↦ g ^ x) ((↑(Nat.card G) : ℤ) * (Nat.card G).gcdA n + (↑n : ℤ) * (Nat.card G).gcdB n))

Tactic:
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)