awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
neg : HPow.hPow (β := ℕ) (x ^ i) 0 = 1
⊢ (x ^ i) ^ orderOf x = 1
have neg₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [orderOf_eq_zero h, _root_.pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
h : IsOfFinOrder x
h' : Membership.mem (γ := Subgroup G) (zpowers x) y
⊢ IsOfFinOrder y
have obtain : ∀ (k : ℤ) (h' : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)), IsOfFinOrder (x ^ k)
Tactic: obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'
Cleared hypotheses: y, h'
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
h : Membership.mem (γ := Subgroup G) (zpowers x) y
⊢ orderOf y ∣ orderOf x
have obtain : ∀ (k : ℤ) (h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)), orderOf (x ^ k) ∣ orderOf x
Tactic: obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
k : ℤ
h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
⊢ orderOf (x ^ k) ∣ orderOf x
have rw : (x ^ k) ^ orderOf x = 1
Tactic: rw [orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x • a = a
have obtain : ∀ (k : ℤ) (hx : Membership.mem (γ := Subgroup G) (zpowers y) (y ^ k)), y ^ k • a = a
Tactic: obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ y ^ k • a = a
have rw : (HPow.hPow (α := Equiv.Perm α) (MulAction.toPerm y) k : (a : α) → α) a = a
Tactic: rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, map_zpow _ y k,
    MulAction.toPermHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ (i % (↑(orderOf x) : ℤ)).natAbs = y
have rwa : HPow.hPow (β := ℤ) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ (i % (↑(orderOf x) : ℤ)).natAbs = y
have rwa₁ : x ^ (i % (↑(orderOf x) : ℤ)) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
have refine : LE.le (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)
Tactic: refine le_antisymm ?_ (le_closure_toSubmonoid s)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ LE.le (α := Submonoid G) (toSubmonoid (closure s)) (Submonoid.closure s)
have rw : LE.le (α := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) (Submonoid.closure s)
Tactic: rw [closure_toSubmonoid]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
have refine : ∀ (x : G) (hx : x⁻¹ ∈ s), x ∈ (↑(Submonoid.closure s) : Set G)
Tactic: refine Submonoid.closure_le.mpr <| Set.union_subset Submonoid.subset_closure
    fun x (hx : x⁻¹ ∈ s) ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
x : G
hx : x⁻¹ ∈ s
⊢ x ∈ (↑(Submonoid.closure s) : Set G)
have a : Membership.mem (γ := Submonoid G) (powers x⁻¹) x
Tactic: apply Submonoid.powers_le.mpr (Submonoid.subset_closure hx)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : CommGroup G
hG : ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
⊢ IsMulTorsionFree G
have 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
Tactic: refine ⟨fun n hn a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ a = b
have rw : ∀ (hab : HDiv.hDiv (α := G) ((fun (a : G) ↦ a ^ n) a) ((fun (a : G) ↦ a ^ n) b) = 1), a / b = 1
Tactic: rw [← div_eq_one] at hab ⊢
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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 = 1
have hab₁ : (a / b) ^ n = 1
Tactic: simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG
Cleared hypotheses: hG, hab
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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 / b = 1
have hG₁ : ∀ ⦃a : G⦄, a ≠ 1 → ¬∃ (n : ℕ), 0 < n ∧ a ^ n = 1
Tactic: simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG
Cleared hypotheses: hG, hab
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g : G
⊢ Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
have inl : ∀ (h : |g|ₘ = g ∧ 1 ≤ g), Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
Tactic: rcases mabs_cases g with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
have inr : ∀ (h : |g|ₘ = g⁻¹ ∧ g < 1), Eq (α := Subgroup G) (zpowers |g|ₘ) (zpowers g)
Tactic: rcases mabs_cases g with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
⊢ orderOf g ≤ 1
have inl : orderOf.{u_1} (G := G) 1 ≤ 1
Tactic: obtain rfl | ha := eq_or_ne g 1
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
inl : orderOf.{u_1} (G := G) 1 ≤ 1
⊢ orderOf g ≤ 1
have inr : ∀ (ha : g ≠ 1), orderOf g ≤ 1
Tactic: obtain rfl | ha := eq_or_ne g 1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1
have ha₁ : orderOf g = 0
Tactic: rw [ne_eq, ← isOfFinOrder_iff_eq_one, ← orderOf_eq_zero_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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}
have refine_1 : Set.PairwiseDisjoint.{u_1, 0} (α := Finset G) (↑n.divisors : Set ℕ) fun (m : ℕ) ↦ {x : G | orderOf x = m}
Tactic: refine (Finset.card_biUnion ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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}
⊢ ∑ m ∈ n.divisors, Finset.card.{u_1} (α := G) {x : G | orderOf x = m} = Finset.card.{u_1} (α := G) {x : G | x ^ n = 1}
have 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}
Tactic: refine (Finset.card_biUnion ?_).symm.trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
⊢ 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}
have refine_2 : Eq.{u_1 + 1} (α := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) {x : G | x ^ n = 1}
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
n : ℕ
inst_1 : Fintype G
inst_2 : DecidableEq G
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Finset G) (n.divisors.biUnion fun (m : ℕ) ↦ {x : G | orderOf x = m}) {x : G | x ^ n = 1}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
inst_1 : Finite G
⊢ orderOf x ≤ Nat.card G
have obtain : ∀ (val : Fintype G), orderOf x ≤ Nat.card G
Tactic: obtain ⟨⟩ := nonempty_fintype G
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x : G
⊢ IsOfFinOrder x
have by_contra : ∀ (h : ¬IsOfFinOrder x), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ (orderOf x - 1) * x = 1
have rw : 1 ≤ orderOf x
Tactic: rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
inst_1 : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ 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))
have rw : Eq (α := Fin (orderOf y)) ((finCongr h : (a : Fin (orderOf x)) → Fin (orderOf y)) ⟨n % orderOf x, sorry⟩ : Fin (orderOf y))
  (⟨n % orderOf y, sorry⟩ : Fin (orderOf y))
Tactic: rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivPowers_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Finite.{u_1 + 1} Gˣ
x : G
⊢ IsOfFinOrder x ↔ IsUnit x
have mpr : IsUnit x → IsOfFinOrder x
Tactic: use IsOfFinOrder.isUnit
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
inst_1 : Finite.{u_1 + 1} Gˣ
u : Gˣ
⊢ IsOfFinOrder (↑u : G)
have mpr : IsOfFinOrder u
Tactic: rw [Units.isOfFinOrder_val]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : Finite G₀
a : G₀
⊢ orderOf a = 0 ↔ a = 0
have this : Finite.{u_6 + 1} G₀ˣ
Tactic: have : Finite G₀ˣ := .of_injective _ Units.val_injective
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD (↑(orderOf x) : ℤ)]
have rw : x ^ n = 1 ↔ (↑(orderOf x) : ℤ) ∣ n
Tactic: rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
n : ℤ
rw : x ^ n = 1 ↔ (↑(orderOf x) : ℤ) ∣ n
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD (↑(orderOf x) : ℤ)]
have rw₁ : x ^ n = 1 ↔ x ^ n = 1
Tactic: rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
m n : ℤ
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw : x ^ m * (x ^ n)⁻¹ = 1 ↔ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
m n : ℤ
rw : x ^ m * (x ^ n)⁻¹ = 1 ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₁ : x ^ (m - n) = 1 ↔ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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) : ℤ)]
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₂ : m - n ≡ 0 [ZMOD (↑(orderOf x) : ℤ)] ↔ 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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) : ℤ)]
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₃ : (↑(orderOf x) : ℤ) ∣ 0 - (m - 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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) : ℤ)]
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₄ : (↑(orderOf x) : ℤ) ∣ 0 - (m - n) ↔ (↑(orderOf x) : ℤ) ∣ n - m
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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₅ : (↑(orderOf x) : ℤ) ∣ -(m - n) ↔ (↑(orderOf x) : ℤ) ∣ n - m
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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD (↑(orderOf x) : ℤ)]
have rw₆ : (↑(orderOf x) : ℤ) ∣ n - m ↔ (↑(orderOf x) : ℤ) ∣ n - m
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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) ↔ ¬IsOfFinOrder x
have refine_1 : (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬IsOfFinOrder x
Tactic: refine ⟨?_, fun h n m hnm => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
refine_1 : (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬IsOfFinOrder x
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) ↔ ¬IsOfFinOrder x
have 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
Tactic: refine ⟨?_, fun h n m hnm => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬IsOfFinOrder x
have refine_1 : (Injective.{1, u_1 + 1} (β := G) fun (n : ℤ) ↦ x ^ n) → ¬∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: simp_rw [isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ n = m
have refine_2 : ∀ (hnm : n ≡ m [ZMOD (↑(orderOf x) : ℤ)]), n = m
Tactic: rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have refine_2₁ : ∀ (hnm : n ≡ m [ZMOD (↑0 : ℤ)]), n = m
Tactic: rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have refine_2₂ : ∀ (hnm : n ≡ m [ZMOD 0]), n = m
Tactic: rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have refine_2₃ : ∀ (hnm : 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
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ Eq (α := Subgroup G) (zpowers x) (zpowers y) ↔ x = y ∨ x⁻¹ = y
have refine : ∀ (h : Eq (α := Subgroup G) (zpowers x) (zpowers y)), x = y ∨ x⁻¹ = y
Tactic: refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : Group G
x y : G
hx : ¬IsOfFinOrder x
h : Eq (α := Subgroup G) (zpowers x) (zpowers y)
⊢ x = y ∨ x⁻¹ = y
have hx_mem : Membership.mem (γ := Subgroup G) (zpowers y) x
Tactic: have hx_mem : x ∈ zpowers y := by simp [← h]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ x = y ∨ x⁻¹ = y
have hy_mem : Membership.mem (γ := Subgroup G) (zpowers x) y
Tactic: have hy_mem : y ∈ zpowers x := by simp [h]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x = y ∨ x⁻¹ = y
have 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
Tactic: obtain ⟨k, rfl⟩ := mem_zpowers_iff.mp hy_mem
Cleared hypotheses: y, h, hx_mem, hy_mem
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
have obtain : ∀ (l : ℤ) (hl : (x ^ k) ^ l = x), x = x ^ k ∨ x⁻¹ = x ^ k
Tactic: obtain ⟨l, hl⟩ := mem_zpowers_iff.mp hx_mem
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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 = x ^ k ∨ x⁻¹ = x ^ k
have hl₁ : x ^ (k * l) = x
Tactic: rw [← zpow_mul] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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 = x ^ k ∨ x⁻¹ = x ^ k
have hl₁ : x ^ (k * l) = HPow.hPow (β := ℤ) x 1
Tactic: nth_rewrite 2 [← zpow_one x] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
have h1 : k * l = 1
Tactic: have h1 := (injective_zpow_iff_not_isOfFinOrder.mpr hx) hl
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
have inl : ∀ (h : k = 1 ∧ l = 1), x = x ^ k ∨ x⁻¹ = x ^ k
Tactic: rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
have inr : ∀ (h : k = -1 ∧ l = -1), x = x ^ k ∨ x⁻¹ = x ^ k
Tactic: rcases (Int.mul_eq_one_iff_eq_one_or_neg_one).mp h1 with (h | h)