awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ m = 1 * x ^ m

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
x₁ : x ^ (k + m) = x ^ (m + k)
x₂ : x ^ m = 1 * x ^ m
⊢ x ^ k * x ^ m = 1 * x ^ m

Tactic:
calc
        x ^ k * x ^ m = x ^ (k + m) := (pow_add _ _ _).symm
        _ = x ^ (m + k) := by simp [Nat.add_comm]
        _ = x ^ m := h
        _ = 1 * x ^ m := by simp

Premises used: pow_add, HAdd.hAdd, Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
⊢ x ^ k = 1

Tactic:
have hk : x ^ k = 1 := by
      apply (mul_right_cancel_iff (a := x ^ m)).1
      calc
        x ^ k * x ^ m = x ^ (k + m) := (pow_add _ _ _).symm
        _ = x ^ (m + k) := by simp [Nat.add_comm]
        _ = x ^ m := h
        _ = 1 * x ^ m := by simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
hk : x ^ k = 1
⊢ m + k ≡ m [MOD orderOf x]

Tactic:
simpa using Nat.ModEq.add_left m (pow_eq_one_iff_modEq.1 hk)

Premises used: Nat.ModEq.add_left, Iff.mp, pow_eq_one_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
apply : k ≡ 0 [MOD orderOf x]
⊢ x ^ k = 1

Tactic:
apply pow_eq_one_iff_modEq.2

Premises used: Iff.mpr, pow_eq_one_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ m + k ≡ m + 0 [MOD orderOf x]

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ k ≡ 0 [MOD orderOf x]

Tactic:
exact Nat.ModEq.add_left_cancel' m (by simpa using h)

Premises used: Nat.ModEq.add_left_cancel'
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ x ^ k = 1

Tactic:
have hk : x ^ k = 1 := by
      apply pow_eq_one_iff_modEq.2
      exact Nat.ModEq.add_left_cancel' m (by simpa using h)
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
rw rw₁ : x ^ m * x ^ k = x ^ m * x ^ k
⊢ x ^ (m + k) = x ^ m * x ^ k

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ m * x ^ k = x ^ m

Tactic:
simp [hk]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
x₁ : x ^ (m + k) = x ^ m * x ^ k
x₂ : x ^ m * x ^ k = x ^ m
⊢ x ^ (m + k) = x ^ m

Tactic:
calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

Premises used: HAdd.hAdd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n) ↔ ¬IsOfFinOrder x

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

Premises used: not_isOfFinOrder_of_injective_pow, Iff.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
refine :
  ∀ (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 => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
n m : ℕ
hnm : Eq.{u_1 + 1} (α := G) ((fun (n : ℕ) ↦ x ^ n) n) ((fun (n : ℕ) ↦ x ^ n) m)
rwa : ∀ (hnm : n ≡ m [MOD orderOf x]), n = m
rwa₁ : ∀ (hnm : n ≡ m [MOD 0]), n = m
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hnm : n = m), n = m
⊢ n = m

Tactic:
rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, Nat.modEq_zero_iff] at hnm

Premises used: Iff.mpr, RightCancelMonoid.pow_eq_pow_iff_modEq, orderOf_eq_zero_iff, Nat.modEq_zero_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
n m : ℕ
⊢ x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

Tactic:
pow_eq_pow_iff_modEq

Premises used: RightCancelMonoid.pow_eq_pow_iff_modEq, Nat.ModEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
rw : n ≡ m [MOD orderOf x] ↔ n = m
rw₁ : n ≡ m [MOD 0] ↔ n = m
rw₂ rw₃ : n = m ↔ n = m
⊢ x ^ n = x ^ m ↔ n = m

Tactic:
rw [pow_eq_pow_iff_modEq, h, Nat.modEq_zero_iff]

Premises used: RightCancelMonoid.pow_eq_pow_iff_modEq, Nat.modEq_zero_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
apply : IsOfFinOrder x
⊢ False

Tactic:
apply h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
n : ℕ
hn : 0 < n
contra : IsOfFinOrder (x ^ n)
rw : ∀ (contra : ∃ (n_1 : ℕ), 0 < n_1 ∧ (x ^ n) ^ n_1 = 1), ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ IsOfFinOrder x

Tactic:
rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢

Premises used: isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
n : ℕ
hn : 0 < n
contra : ∃ (n_1 : ℕ), 0 < n_1 ∧ (x ^ n) ^ n_1 = 1
obtain : ∀ (m : ℕ) (hm : 0 < m) (hm' : (x ^ n) ^ m = 1), ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := contra
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' rwa rwa₁ rwa₂ rwa₃ : (x ^ n) ^ m = 1
⊢ x ^ (n * m) = 1

Tactic:
rwa [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
n : ℕ
hn : 0 < n
m : ℕ
hm : 0 < m
hm' : (x ^ n) ^ m = 1
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
⊢ s ⊆ {y : G | ¬IsOfFinOrder y}

Tactic:
have hs : s ⊆ { y : G | ¬IsOfFinOrder y } := by
    rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
    apply h
    rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
    obtain ⟨m, hm, hm'⟩ := contra
    exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
this : s.Infinite
⊢ Set.Infinite.{u_1} (α := G) {y : G | ¬IsOfFinOrder y}

Tactic:
this.mono hs

Premises used: Set.Infinite.mono
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
this : s.Infinite
⊢ Set.Infinite.{u_1} (α := G) {y : G | ¬IsOfFinOrder y}

Tactic:
exact this.mono hs

Premises used: Set.Infinite.mono
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
suffices : s.Infinite
⊢ Set.Infinite.{u_1} (α := G) {y : G | ¬IsOfFinOrder y}

Tactic:
suffices s.Infinite by exact this.mono hs
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
contrapose! : ∀ (h : s.Finite), IsOfFinOrder x
⊢ s.Infinite

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
⊢ ¬Set.InjOn.{0, u_1} (β := G) (fun (n : ℕ) ↦ x ^ n) (Set.Ioi 0)

Tactic:
have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Set.InjOn.{0, u_1} (β := G) (fun (n : ℕ) ↦ x ^ n) (Set.Ioi 0)
contrapose :
  ∀ (this : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n),
    Set.InjOn.{0, u_1} (β := G) (fun (n : ℕ) ↦ x ^ n) (Set.Ioi 0)
⊢ ¬Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n

Tactic:
contrapose this
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
this : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
⊢ Set.InjOn.{0, u_1} (β := G) (fun (n : ℕ) ↦ x ^ n) (Set.Ioi 0)

Tactic:
Set.injOn_of_injective this

Premises used: Set.injOn_of_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
this : Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
⊢ Set.InjOn.{0, u_1} (β := G) (fun (n : ℕ) ↦ x ^ n) (Set.Ioi 0)

Tactic:
exact Set.injOn_of_injective this

Premises used: Set.injOn_of_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
⊢ ¬Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n

Tactic:
have : ¬Function.Injective fun n : ℕ => x ^ n := by
    have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h
    contrapose this
    exact Set.injOn_of_injective this
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
hs : s ⊆ {y : G | ¬IsOfFinOrder y}
h : s.Finite
this : ¬Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
rwa : ∀ (this : ¬¬IsOfFinOrder x), IsOfFinOrder x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : IsOfFinOrder x), IsOfFinOrder x
⊢ IsOfFinOrder x

Tactic:
rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

Premises used: Classical.not_not, RightCancelMonoid.injective_pow_iff_not_isOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
⊢ (↑(powers a) : Set G).Finite ↔ IsOfFinOrder a

Tactic:
⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩

Premises used: IsOfFinOrder.finite_powers, Iff.intro
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
refine : ∀ (h : (↑(powers a) : Set G).Finite), IsOfFinOrder a
⊢ (↑(powers a) : Set G).Finite ↔ IsOfFinOrder a

Tactic:
refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
n : ℕ
⊢ (fun (n : ℕ) ↦ a ^ n) n ∈ (↑(powers a) : Set G)

Tactic:
simp [mem_powers_iff]

Premises used: Submonoid.mem_powers_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
obtain : ∀ (m n : ℕ) (hmn : m < n) (ha : a ^ m = a ^ n), IsOfFinOrder a
⊢ IsOfFinOrder a

Tactic:
obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])

Premises used: Set.Finite.exists_lt_map_eq_of_forall_mem
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ IsOfFinOrder a

Tactic:
isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩

Premises used: Iff.mpr, tsub_pos_iff_lt, HSub.hSub, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
refine : a ^ (n - m) = 1
⊢ IsOfFinOrder a

Tactic:
refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩

Premises used: Iff.mpr, tsub_pos_iff_lt, HSub.hSub, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
apply : a ^ (n - m) * a ^ m = 1 * a ^ m
⊢ a ^ (n - m) = 1

Tactic:
apply (mul_right_cancel_iff (a := a ^ m)).1

Premises used: Iff.mp, mul_right_cancel_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) * a ^ m = a ^ (n - m + m)

Tactic:
(pow_add _ _ _).symm

Premises used: pow_add, Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m + m) = a ^ n

Tactic:
simp [tsub_add_cancel_of_le hmn.le]

Premises used: tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ n = a ^ m

Tactic:
ha.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ m = 1 * a ^ m

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
a₁ : a ^ (n - m + m) = a ^ n
a₂ : a ^ m = 1 * a ^ m
⊢ a ^ (n - m) * a ^ m = 1 * a ^ m

Tactic:
calc
    a ^ (n - m) * a ^ m = a ^ (n - m + m) := (pow_add _ _ _).symm
    _ = a ^ n := by simp [tsub_add_cancel_of_le hmn.le]
    _ = a ^ m := ha.symm
    _ = 1 * a ^ m := by simp

Premises used: HSub.hSub, pow_add, HAdd.hAdd, Eq.symm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
⊢ (↑(powers a) : Set G).Infinite ↔ ¬IsOfFinOrder a

Tactic:
finite_powers.not

Premises used: Iff.not, RightCancelMonoid.finite_powers, Set.Infinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
pos : ∀ (ha : IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
neg : ∀ (ha : ¬IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a

Tactic:
by_cases ha : IsOfFinOrder a

Premises used: IsOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card (Fin (orderOf a)) = orderOf a

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Infinite.{u_1 + 1} (↑(↑(powers a) : Set G) : Type u_1)

Tactic:
have := (infinite_powers.2 ha).to_subtype
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
this : Infinite.{u_1 + 1} (↑(↑(powers a) : Set G) : Type u_1)
neg : Nat.card.{u_1} ↥(powers a) = 0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a

Tactic:
rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite, orderOf_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
a : G
pos : ∀ (ha : IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
neg neg₁ : ∀ (ha : ¬IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a

Tactic:
classical
  by_cases ha : IsOfFinOrder a
  · exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp
  · have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite, IsOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
⊢ IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x

Tactic:
simp [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
i : ℤ
inl : ∀ (i : ℕ), Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
inr : ∀ (i : ℕ), Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
⊢ (↑(orderOf x) : ℤ) ∣ i ↔ x ^ i = 1

Tactic:
rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
inl : orderOf x ∣ i ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
inl₁ : x ^ i = 1 ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
inl₂ inl₃ : x ^ i = 1 ↔ x ^ i = 1
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1

Tactic:
rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]

Premises used: zpow_natCast, orderOf_dvd_iff_pow_eq_one, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
inr : Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
inr₁ : orderOf x ∣ i ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
inr₂ : orderOf x ∣ i ↔ (HPow.hPow (β := ℤ) x (↑i : ℤ))⁻¹ = 1
inr₃ : orderOf x ∣ i ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
inr₄ : orderOf x ∣ i ↔ x ^ i = 1
inr₅ inr₆ : x ^ i = 1 ↔ x ^ i = 1
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1

Tactic:
rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]

Premises used: zpow_natCast, inv_eq_one, dvd_neg, zpow_neg, orderOf_dvd_iff_pow_eq_one, Int.natCast_dvd_natCast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
⊢ orderOf x⁻¹ = orderOf x

Tactic:
simp [orderOf_eq_orderOf_iff]

Premises used: orderOf_eq_orderOf_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
a b : ℤ
rw : x ^ (a - b) = 1 ↔ x ^ a = x ^ b
rw₁ : x ^ a * (x ^ b)⁻¹ = 1 ↔ x ^ a = x ^ b
rw₂ rw₃ : x ^ a = x ^ b ↔ x ^ a = x ^ b
⊢ (↑(orderOf x) : ℤ) ∣ a - b ↔ x ^ a = x ^ b

Tactic:
rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Premises used: mul_inv_eq_one, orderOf_dvd_iff_zpow_eq_one, zpow_sub
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : ↥H
⊢ orderOf (↑a : G) = orderOf a

Tactic:
orderOf_injective H.subtype Subtype.coe_injective _

Premises used: Subgroup.subtype, Subtype.coe_injective, orderOf_injective
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
ha : a ∈ H
⊢ orderOf (Subtype.mk (p := fun (x : G) ↦ x ∈ H) a ha) = orderOf a

Tactic:
(orderOf_coe _).symm

Premises used: Eq.symm, Subgroup.orderOf_coe
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
z : ℤ
⊢ x ^ (z % (↑(orderOf x) : ℤ)) = x ^ (z % (↑(orderOf x) : ℤ) + (↑(orderOf x) : ℤ) * (z / (↑(orderOf x) : ℤ)))

Tactic:
simp [zpow_add, zpow_mul, pow_orderOf_eq_one]

Premises used: zpow_add, zpow_mul, pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
z : ℤ
rw rw₁ : x ^ z = x ^ z
⊢ x ^ (z % (↑(orderOf x) : ℤ) + (↑(orderOf x) : ℤ) * (z / (↑(orderOf x) : ℤ))) = x ^ z

Tactic:
rw [Int.emod_add_mul_ediv]

Premises used: Int.emod_add_mul_ediv
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
pos : ∀ (h : IsOfFinOrder x), (x ^ i) ^ orderOf x = 1
neg : ∀ (h : ¬IsOfFinOrder x), (x ^ i) ^ orderOf x = 1
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
by_cases h : IsOfFinOrder x

Premises used: IsOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : IsOfFinOrder x
pos : HPow.hPow (β := ℤ) (x ^ i) (↑(orderOf x) : ℤ) = 1
pos₁ : x ^ (i * (↑(orderOf x) : ℤ)) = 1
pos₂ : x ^ ((↑(orderOf x) : ℤ) * i) = 1
pos₃ : HPow.hPow (β := ℤ) x (↑(orderOf x) : ℤ) ^ i = 1
pos₄ : (x ^ orderOf x) ^ i = 1
pos₅ : HPow.hPow (α := G) 1 i = 1
pos₆ pos₇ : Eq.{u_1 + 1} (α := G) 1 1
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]

Premises used: zpow_natCast, zpow_mul, one_zpow, pow_orderOf_eq_one, mul_comm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
neg : HPow.hPow (β := ℕ) (x ^ i) 0 = 1
neg₁ neg₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
rw [orderOf_eq_zero h, _root_.pow_zero]

Premises used: pow_zero, orderOf_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : IsOfFinOrder x
i : ℤ
⊢ IsOfFinOrder (x ^ i)

Tactic:
isOfFinOrder_iff_pow_eq_one.mpr ⟨orderOf x, h.orderOf_pos, zpow_pow_orderOf⟩

Premises used: Iff.mpr, IsOfFinOrder.orderOf_pos, zpow_pow_orderOf, orderOf, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
h : IsOfFinOrder x
h' : Membership.mem (γ := Subgroup G) (zpowers x) y
obtain : ∀ (k : ℤ) (h' : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)), IsOfFinOrder (x ^ k)
⊢ IsOfFinOrder y

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

Premises used: Iff.mp, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
⊢ IsOfFinOrder (x ^ k)

Tactic:
h.zpow

Premises used: IsOfFinOrder.zpow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
h : IsOfFinOrder x
k : ℤ
h' : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
⊢ IsOfFinOrder (x ^ k)

Tactic:
exact h.zpow

Premises used: IsOfFinOrder.zpow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x y : G
h : Membership.mem (γ := Subgroup G) (zpowers x) y
obtain : ∀ (k : ℤ) (h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)), orderOf (x ^ k) ∣ orderOf x
⊢ orderOf y ∣ orderOf x

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

Premises used: Iff.mp, Subgroup.mem_zpowers_iff, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
k : ℤ
h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
rw : (x ^ k) ^ orderOf x = 1
⊢ orderOf (x ^ k) ∣ orderOf x

Tactic:
rw [orderOf_dvd_iff_pow_eq_one]

Premises used: orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
k : ℤ
h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
⊢ (x ^ k) ^ orderOf x = 1

Tactic:
zpow_pow_orderOf

Premises used: zpow_pow_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
x : G
k : ℤ
h : Membership.mem (γ := Subgroup G) (zpowers x) (x ^ k)
⊢ (x ^ k) ^ orderOf x = 1

Tactic:
exact zpow_pow_orderOf

Premises used: zpow_pow_orderOf