awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
α : Type u_6
inst_1 : MulAction G α
hx : Membership.mem (γ := Subgroup G) (zpowers y) x
a : α
hs : y • a = a
obtain : ∀ (k : ℤ) (hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)), y ^ k • a = a
⊢ x • a = a

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

Premises used: Iff.mp, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
y : G
α : Type u_6
inst_1 : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)
rw : (HPow.hPow (α := Equiv.Perm α) (MulAction.toPerm y) k : (a : α) → α) a = a
⊢ y ^ k • a = a

Tactic:
rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, map_zpow _ y k,
    MulAction.toPermHom_apply]

Premises used: MulAction.toPerm_apply, MulAction.toPermHom_apply, map_zpow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
y : G
α : Type u_6
inst_1 : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)
⊢ IsFixedPt (⇑(MulAction.toPerm y) : (a : α) → α) a

Tactic:
hs

Premises used: Function.IsFixedPt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
y : G
α : Type u_6
inst_1 : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)
⊢ IsFixedPt (⇑(MulAction.toPerm y) : (a : α) → α) a

Tactic:
exact hs
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
y : G
α : Type u_6
inst_1 : MulAction G α
a : α
hs : y • a = a
k : ℤ
hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)
⊢ (HPow.hPow (α := Equiv.Perm α) (MulAction.toPerm y) k : (a : α) → α) a = a

Tactic:
exact Function.IsFixedPt.perm_zpow (by exact hs) k

Premises used: Function.IsFixedPt.perm_zpow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_6
inst : AddGroup G
x y : G
α : Type u_7
inst_1 : AddAction G α
hx : Membership.mem (γ := AddSubgroup G) (AddSubgroup.zmultiples y) x
a : α
hs : y +ᵥ a = a
⊢ x +ᵥ a = a

Tactic:
@smul_eq_self_of_mem_zpowers (Multiplicative G) _ _ _ α _ hx a hs

Premises used: smul_eq_self_of_mem_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : IsOfFinOrder x
h : Membership.mem (γ := Submonoid G) (powers x) y
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = y
⊢ (fun (x_1 : ℤ) ↦ x ^ x_1) (↑n : ℤ) = y

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
hx : IsOfFinOrder x
h : Membership.mem (γ := Subgroup G) (zpowers x) y
i : ℤ
hi : (fun (x_1 : ℤ) ↦ x ^ x_1) i = y
rwa : HPow.hPow (β := ℤ) x (↑(i % (↑(orderOf x) : ℤ)).natAbs : ℤ) = y
rwa₁ : x ^ (i % (↑(orderOf x) : ℤ)) = y
rwa₂ rwa₃ rwa₄ rwa₅ : x ^ i = y
⊢ x ^ (i % (↑(orderOf x) : ℤ)).natAbs = y

Tactic:
rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]

Premises used: zpow_natCast, Iff.mpr, IsOfFinOrder.orderOf_pos, zpow_mod_orderOf, Int.natCast_ne_zero_iff_pos, Int.natAbs_of_nonneg, Int.emod_nonneg
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : IsOfFinOrder x
⊢ (↑(powers x) : Set G) = (↑(zpowers x) : Set G)

Tactic:
Set.ext fun _ ↦ hx.mem_powers_iff_mem_zpowers

Premises used: Set.ext, IsOfFinOrder.mem_powers_iff_mem_zpowers
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : DecidableEq G
hx : IsOfFinOrder x
⊢ 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:
hx.mem_powers_iff_mem_zpowers.symm.trans hx.mem_powers_iff_mem_range_orderOf

Premises used: IsOfFinOrder.mem_powers_iff_mem_zpowers, IsOfFinOrder.mem_powers_iff_mem_range_orderOf, Iff.trans, Iff.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ Eq (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)

Tactic:
le_antisymm ?_ (le_closure_toSubmonoid s)

Premises used: Subgroup.le_closure_toSubmonoid, le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
refine : LE.le (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)
⊢ Eq (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)

Tactic:
refine le_antisymm ?_ (le_closure_toSubmonoid s)

Premises used: Subgroup.le_closure_toSubmonoid, le_antisymm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
rw : LE.le (α := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) (Submonoid.closure s)
⊢ LE.le (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)

Tactic:
rw [closure_toSubmonoid]

Premises used: Subgroup.closure_toSubmonoid
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ LE.le (α := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) (Submonoid.closure s)

Tactic:
Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_

Premises used: Iff.mpr, Set.union_subset, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
refine : ∀ (x : G) (hx : x⁻¹ ∈ s), x ∈ (↑(Submonoid.closure s) : Set G)
⊢ LE.le (α := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) (Submonoid.closure s)

Tactic:
refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_

Premises used: Iff.mpr, Set.union_subset, Submonoid.subset_closure, Submonoid.closure_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
a : Membership.mem (γ := Submonoid G) (powers x⁻¹) x
⊢ x ∈ (↑(Submonoid.closure s) : Set G)

Tactic:
apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)

Premises used: Iff.mpr, Submonoid.subset_closure, Submonoid.powers_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ Membership.mem (γ := Submonoid G) (powers x⁻¹) x

Tactic:
simp [(hs _ hx).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
x : G
hx : IsOfFinOrder x
n : Fin (orderOf x)
⊢ Eq (α := ↥(zpowers x)) ((finEquivZPowers hx : (a : Fin (orderOf x)) → ↥(zpowers x)) n : ↥(zpowers x))
    (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ (↑n : ℕ)) ⋯ : ↥(zpowers x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : Group G
x y : G
i : ℤ
hx : IsOfFinOrder x
n : ℕ
⊢ (fun (x_1 : ℤ) ↦ x ^ x_1) (↑n : ℤ) = x ^ n

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (((Equiv.setCongr (s := (↑(powers x) : Set G)) (t := (↑(zpowers x) : Set G)) ⋯).symm :
          (a : ↥(zpowers x)) → ↥(powers x))
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ n) ⋯)) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))

Tactic:
finEquivPowers_symm_apply _ n

Premises used: finEquivPowers_symm_apply
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (((Equiv.setCongr (s := (↑(powers x) : Set G)) (t := (↑(zpowers x) : Set G)) ⋯).symm :
          (a : ↥(zpowers x)) → ↥(powers x))
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ n) ⋯)) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))

Tactic:
exact finEquivPowers_symm_apply _ n

Premises used: finEquivPowers_symm_apply
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
hx : IsOfFinOrder x
a : ↥(zpowers x)
⊢ x ^ (↑(((finEquivZPowers hx).symm : (a : ↥(zpowers x)) → Fin (orderOf x)) a) : ℕ) = (↑a : G)

Tactic:
simpa only [finEquivZPowers_apply] using
    congr_arg Subtype.val ((finEquivZPowers hx).apply_symm_apply a)

Premises used: Equiv.apply_symm_apply, finEquivZPowers, congr_arg, finEquivZPowers_apply, Subtype.val
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommMonoid G
x y : G
hx : IsOfFinOrder x
hy : IsOfFinOrder y
⊢ IsOfFinOrder (x * y)

Tactic:
(Commute.all x y).isOfFinOrder_mul hx hy

Premises used: Commute.isOfFinOrder_mul, Commute.all
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
⊢ IsMulTorsionFree G

Tactic:
⟨fun n hn a b hab ↦ ?_⟩

Premises used: IsMulTorsionFree.mk
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
refine :
  ∀ (n : ℕ) (hn : n ≠ 0) (a b : G) (hab : Eq.{u_1 + 1} (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b)),
    a = b
⊢ IsMulTorsionFree G

Tactic:
refine ⟨fun n hn a b hab ↦ ?_⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : Eq.{u_1 + 1} (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b)
rw : ∀ (hab : HDiv.hDiv (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b) = 1), a / b = 1
⊢ a = b

Tactic:
rw [← div_eq_one] at hab ⊢

Premises used: div_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : HDiv.hDiv (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b) = 1
⊢ (a / b) ^ n = 1

Tactic:
simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG

Premises used: div_pow, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
n : ℕ
hn : n ≠ 0
a b : G
hab : HDiv.hDiv (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b) = 1
hab₁ : (a / b) ^ n = 1
⊢ ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1

Tactic:
simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG

Premises used: div_pow, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
a b : G
hab : (a / b) ^ n = 1
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1
⊢ a / b = 1

Tactic:
of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

Premises used: And.intro, Exists.intro, of_not_not, Ne.bot_lt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
hn : n ≠ 0
a b : G
hab : (a / b) ^ n = 1
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1
⊢ a / b = 1

Tactic:
exact of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

Premises used: And.intro, Exists.intro, of_not_not, Ne.bot_lt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
⊢ ¬IsMulTorsionFree G ↔ ∃ (a : G), a ≠ 1 ∧ IsOfFinOrder a

Tactic:
simp [isMulTorsionFree_iff_not_isOfFinOrder]

Premises used: isMulTorsionFree_iff_not_isOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g : G
inl : ∀ (h : |g|ₘ = g ∧ 1 ≤ g), Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
inr : ∀ (h : |g|ₘ = g⁻¹ ∧ g < 1), Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
⊢ Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)

Tactic:
rcases mabs_cases g with h | h

Premises used: mabs_cases
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g : G
h : |g|ₘ = g ∧ 1 ≤ g
⊢ Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)

Tactic:
simp only [h, zpowers_inv]

Premises used: Subgroup.zpowers_inv
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g : G
h : |g|ₘ = g⁻¹ ∧ g < 1
⊢ Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)

Tactic:
simp only [h, zpowers_inv]

Premises used: Subgroup.zpowers_inv
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
inl : orderOf.{u_1} (G := G) 1 ≤ 1
inr : ∀ (ha : g ≠ 1), orderOf g ≤ 1
⊢ orderOf g ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne g 1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
⊢ orderOf.{u_1} (G := G) 1 ≤ 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g = 0

Tactic:
rw [ne_eq, ← isOfFinOrder_iff_eq_one, ← orderOf_eq_zero_iff] at ha

Premises used: orderOf_eq_zero_iff, isOfFinOrder_iff_eq_one, ne_eq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
ha : orderOf g = 0
⊢ orderOf g ≤ 1

Tactic:
simp [ha]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
⊢ ∑ m ∈ n.divisors, Finset.card.{u_1} (α := G) {x : G | orderOf x = m} = Finset.card.{u_1} (α := G) {x : G | x ^ n = 1}

Tactic:
(Finset.card_biUnion ?_).symm.trans ?_

Premises used: Finset.card_biUnion, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
refine_1 : Set.PairwiseDisjoint.{u_1, 0} (α := Finset G) (↑n.divisors : Set ℕ) fun (m : ℕ) ↦ {x : G | orderOf x = m}
refine_2 :
  Finset.card.{u_1} (α := G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) =
    Finset.card.{u_1} (α := G) {x : G | x ^ n = 1}
⊢ ∑ m ∈ n.divisors, Finset.card.{u_1} (α := G) {x : G | orderOf x = m} = Finset.card.{u_1} (α := G) {x : G | x ^ n = 1}

Tactic:
refine (Finset.card_biUnion ?_).symm.trans ?_

Premises used: Finset.card_biUnion, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
⊢ Set.PairwiseDisjoint.{u_1, 0} (α := Finset G) (↑n.divisors : Set ℕ) fun (m : ℕ) ↦ {x : G | orderOf x = m}

Tactic:
simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]

Premises used: Set.PairwiseDisjoint, disjoint_iff, Finset.ext_iff, Set.Pairwise
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
refine_2 : Eq.{u_1 + 1} (α := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) {x : G | x ^ n = 1}
⊢ Finset.card.{u_1} (α := G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) =
    Finset.card.{u_1} (α := G) {x : G | x ^ n = 1}

Tactic:
congr
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
refine_2 :
  ∀ (a : G),
    Membership.mem (γ := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) a ↔
      Membership.mem (γ := Finset G) {x : G | x ^ n = 1} a
⊢ Eq.{u_1 + 1} (α := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) {x : G | x ^ n = 1}

Tactic:
ext
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
a : G
⊢ Membership.mem (γ := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) a ↔
    Membership.mem (γ := Finset G) {x : G | x ^ n = 1} a

Tactic:
simp [hn, orderOf_dvd_iff_pow_eq_one]

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
inst_1 : Fintype G
⊢ orderOf x ≤ card G

Tactic:
Finset.le_card_of_inj_on_range (x ^ ·) (fun _ _ ↦ Finset.mem_univ _) pow_injOn_Iio_orderOf

Premises used: Finset.mem_univ, Finset.le_card_of_inj_on_range, pow_injOn_Iio_orderOf, Fintype.card, HPow.hPow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
inst_1 : Finite G
obtain : ∀ (val : Fintype G), orderOf x ≤ Nat.card G
⊢ orderOf x ≤ Nat.card G

Tactic:
obtain ⟨⟩ := nonempty_fintype G

Premises used: nonempty_fintype
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
inst_1 : Finite G
val : Fintype G
⊢ orderOf x ≤ Nat.card G

Tactic:
simpa using orderOf_le_card_univ

Premises used: orderOf_le_card_univ
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x : G
by_contra : ∀ (h : ¬IsOfFinOrder x), False
⊢ IsOfFinOrder x

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Tactic:
infinite_not_isOfFinOrder h <| Set.toFinite _

Premises used: infinite_not_isOfFinOrder, Set.toFinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x : G
h : ¬IsOfFinOrder x
⊢ False

Tactic:
exact infinite_not_isOfFinOrder h <| Set.toFinite _

Premises used: infinite_not_isOfFinOrder, Set.toFinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : LeftCancelMonoid G
inst_1 : Finite G
x_1 y : G
n : ℕ
x : G
rw : 1 ≤ orderOf x
⊢ x ^ (orderOf x - 1) * x = 1

Tactic:
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]

Premises used: pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : LeftCancelMonoid G
inst_1 : Finite G
x_1 y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x

Tactic:
(isOfFinOrder_of_finite x).orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, isOfFinOrder_of_finite, 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 : LeftCancelMonoid G
inst_1 : Finite G
x_1 y : G
n : ℕ
x : G
⊢ 1 ≤ orderOf x

Tactic:
exact (isOfFinOrder_of_finite x).orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
H_1 : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst : LeftCancelMonoid G
inst_1 : Finite G
x y : G
n : ℕ
H : Type u_6
inst_2 : RightCancelMonoid H
inst_3 : Finite H
this_1 : Finite.{u_6 + 1} Hᵐᵒᵖ := ⋯
this : Group Hᵐᵒᵖ := LeftCancelMonoid.groupOfFinite
⊢ Group H

Tactic:
exact (MulEquiv.opOp H).toEquiv.group

Premises used: MulEquiv.opOp, MulEquiv.toEquiv, Equiv.group
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x : G
⊢ 0 < orderOf x

Tactic:
(isOfFinOrder_of_finite x).orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos, isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
n : ℕ
x : G
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
(isOfFinOrder_of_finite _).orderOf_pow ..

Premises used: IsOfFinOrder.orderOf_pow, isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x y : G
inst_2 : DecidableEq G
⊢ 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' (orderOf_pos x) <| pow_mod_orderOf _

Premises used: Set.Mem, pow_mod_orderOf, setOf, Finset.mem_range_iff_mem_finset_range_of_mod_eq', Set.range, orderOf_pos
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x y : 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 (α := ↥(powers y))
    ((powersEquivPowers h : (a : ↥(powers x)) → ↥(powers y))
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) :
      ↥(powers y))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (powers y) x) (y ^ n) ⋯ : ↥(powers y))

Tactic:
rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivPowers_symm_apply]

Premises used: Equiv.trans_apply, powersEquivPowers, finEquivPowers_symm_apply, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x y : 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 : LeftCancelMonoid G
inst_1 : Fintype G
x : G
⊢ orderOf x = card.{u_1} ↥(powers x)

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

Premises used: Iff.mpr, Fintype.card_fin, Fintype.card_eq, finEquivPowers, isOfFinOrder_of_finite, Nonempty.intro, orderOf, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Finite.{u_1 + 1} Gˣ
x : G
mpr : IsUnit x → IsOfFinOrder x
⊢ IsOfFinOrder x ↔ IsUnit x

Tactic:
use IsOfFinOrder.isUnit

Premises used: IsOfFinOrder.isUnit
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Finite.{u_1 + 1} Gˣ
u : Gˣ
mpr : IsOfFinOrder u
⊢ IsOfFinOrder (↑u : G)

Tactic:
rw [Units.isOfFinOrder_val]

Premises used: Units.isOfFinOrder_val
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Finite.{u_1 + 1} Gˣ
u : Gˣ
⊢ IsOfFinOrder u

Tactic:
apply isOfFinOrder_of_finite

Premises used: isOfFinOrder_of_finite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : Finite G₀
a : G₀
⊢ Finite.{u_6 + 1} G₀ˣ

Tactic:
have : Finite G₀ˣ := .of_injective _ Units.val_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : Finite G₀
a : G₀
this : Finite.{u_6 + 1} G₀ˣ
⊢ orderOf a = 0 ↔ a = 0

Tactic:
simp [isOfFinOrder_iff_isUnit]

Premises used: isOfFinOrder_iff_isUnit
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
n : ℤ
rw : x ^ n = 1 ↔ (↑(orderOf x) : ℤ) ∣ n
rw₁ rw₂ : x ^ n = 1 ↔ x ^ n = 1
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD (↑(orderOf x) : ℤ)]

Tactic:
rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

Premises used: orderOf_dvd_iff_zpow_eq_one, Int.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
m n : ℤ
rw : x ^ m * (x ^ n)⁻¹ = 1 ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
rw₁ : x ^ (m - n) = 1 ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
rw₂ : m - n ≡ 0 [ZMOD (↑(orderOf x) : ℤ)] ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
rw₃ : (↑(orderOf x) : ℤ) ∣ 0 - (m - n) ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
rw₄ : (↑(orderOf x) : ℤ) ∣ 0 - (m - n) ↔ (↑(orderOf x) : ℤ) ∣ n - m
rw₅ : (↑(orderOf x) : ℤ) ∣ -(m - n) ↔ (↑(orderOf x) : ℤ) ∣ n - m
rw₆ rw₇ : (↑(orderOf x) : ℤ) ∣ n - m ↔ (↑(orderOf x) : ℤ) ∣ n - m
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]

Tactic:
rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd,
    zero_sub, neg_sub]

Premises used: Int.modEq_iff_dvd, neg_sub, mul_inv_eq_one, zpow_eq_one_iff_modEq, zpow_sub, zero_sub
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
⟨?_, fun h n m hnm => ?_⟩

Premises used: Iff.intro