awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
h : ∃ (m : ℕ), x ^ p ^ m = 1
w : ℕ
hm : x ^ p ^ w = 1
k : ℕ
left : k ≤ w
hk : orderOf x = p ^ k
⊢ ∃ (k : ℕ), orderOf x = p ^ k

Tactic:
exact ⟨k, hk⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
pos : ∀ (h : ringChar R = 2), orderOf.{u_6} (G := R) (-1) = 1
neg : ∀ (h : ¬ringChar R = 2), orderOf.{u_6} (G := R) (-1) = 2
⊢ orderOf.{u_6} (G := R) (-1) = if ringChar R = 2 then 1 else 2

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ringChar R = 2
pos : orderOf.{u_6} (G := R) 1 = 1
pos₁ pos₂ : Eq (α := ℕ) 1 1
⊢ orderOf.{u_6} (G := R) (-1) = 1

Tactic:
rw [neg_one_eq_one_iff.2 h, orderOf_one]

Premises used: Iff.mpr, orderOf_one, neg_one_eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ¬ringChar R = 2
neg : HPow.hPow (α := R) (β := ℕ) (-1) 2 = 1
neg₁ : Ne.{u_6 + 1} (α := R) (-1) 1
⊢ orderOf.{u_6} (G := R) (-1) = 2

Tactic:
apply orderOf_eq_prime

Premises used: orderOf_eq_prime
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ¬ringChar R = 2
⊢ HPow.hPow (α := R) (β := ℕ) (-1) 2 = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
h : ¬ringChar R = 2
⊢ Ne.{u_6 + 1} (α := R) (-1) 1

Tactic:
simpa [neg_one_eq_one_iff] using h

Premises used: neg_one_eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst_3 : CharP R p
x : R
simp : x = -1 → ¬x = 1
⊢ orderOf x = 2 ↔ x = -1

Tactic:
simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
    and_iff_left_iff_imp]

Premises used: sq_eq_one_iff, orderOf_eq_prime_iff, false_or, ne_eq, and_not_self, or_and_right, and_iff_left_iff_imp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst_3 : CharP R p
⊢ ¬Eq.{u_6 + 1} (α := R) (-1) 1

Tactic:
fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

Premises used: ringChar.eq, Eq.rec, Iff.mp, Not, neg_one_eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst_3 : CharP R p
⊢ ¬Eq.{u_6 + 1} (α := R) (-1) 1

Tactic:
exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

Premises used: ringChar.eq, Eq.rec, Iff.mp, neg_one_eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : Fin (orderOf x)
⊢ Eq (α := ↥(powers x)) ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) n : ↥(powers x))
    (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ (↑n : ℕ)) ⋯ : ↥(powers x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
rw :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    ((finEquivPowers hx : (a : Fin (orderOf x)) → ↥(powers x)) (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)))
rw₁ :
  Eq (α := ↥(powers x)) (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯)
    (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1)
      (x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)) ⋯)
rw₂ : x ^ n = x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)
rw₃ : x ^ (n % orderOf x) = x ^ (↑(⟨n % orderOf x, ⋯⟩ : Fin (orderOf x)) : ℕ)
rw₄ rw₅ : x ^ (n % orderOf x) = x ^ (n % orderOf x)
⊢ ((finEquivPowers hx).symm : (a : ↥(powers x)) → Fin (orderOf x))
      (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Submonoid G) (powers x) x_1) (x ^ n) ⋯) =
    (⟨n % orderOf x, ⋯⟩ : Fin (orderOf x))

Tactic:
rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]

Premises used: finEquivPowers_apply, pow_mod_orderOf, Fin.val_mk, Equiv.symm_apply_eq, Subtype.mk_eq_mk
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
inr :
  ∀ (this : ∀ {n m : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]) (hmn : ¬m ≤ n),
    x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
wlog : ∀ {n m : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
hmn : ¬m ≤ n
inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
inr₂ inr₃ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]

Premises used: le_of_not_ge, eq_comm, Nat.ModEq.comm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n_1 m_1 : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n m_1 : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
rw : k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]

Premises used: pow_add, IsUnit.pow, IsUnit.mul_eq_left, IsOfFinOrder.isUnit, pow_eq_one_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n m_1 : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

Premises used: Nat.ModEq.add_left, Iff.intro, Nat.ModEq.add_left_cancel'
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
n m_1 : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Monoid G
x : G
hx : IsOfFinOrder x
n m : ℕ
⊢ x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

Tactic:
hx.pow_eq_pow_iff_modEq

Premises used: Nat.ModEq, IsOfFinOrder.pow_eq_pow_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m n : ℕ
inr :
  ∀ (this : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]) (hmn : ¬m ≤ n),
    x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
wlog : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
hmn : ¬m ≤ n
inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
inr₂ inr₃ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]

Premises used: le_of_not_ge, eq_comm, Nat.ModEq.comm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n_1 m n : ℕ
hmn : m ≤ n
obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
rw : k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]

Premises used: pow_add, HPow.hPow, mul_one, mul_left_cancel_iff, pow_eq_one_iff_modEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

Premises used: Nat.ModEq.add_left, Iff.intro, Nat.ModEq.add_left_cancel'
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]

Tactic:
exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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, modEq_zero_iff] at hnm

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

Tactic:
pow_eq_pow_iff_modEq

Premises used: pow_eq_pow_iff_modEq, Nat.ModEq
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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, modEq_zero_iff]

Premises used: pow_eq_pow_iff_modEq, Nat.modEq_zero_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : ¬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 : LeftCancelMonoid 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, injective_pow_iff_not_isOfFinOrder
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
rw : a ^ m * a ^ (n - m) = a ^ m * 1
rw₁ : a ^ (m + (n - m)) = a ^ m * 1
rw₂ : a ^ n = a ^ m * 1
rw₃ : a ^ n = a ^ n * 1
rw₄ rw₅ : a ^ n = a ^ n
⊢ a ^ (n - m) = 1

Tactic:
rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

Premises used: pow_add, LT.lt.le, mul_one, mul_left_cancel_iff, add_tsub_cancel_of_le
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
⊢ (↑(powers a) : Set G).Infinite ↔ ¬IsOfFinOrder a

Tactic:
finite_powers.not

Premises used: finite_powers, Iff.not, Set.Infinite
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a

Tactic:
exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp

Premises used: finEquivPowers, Nat.card_congr, Equiv.symm, Eq.trans
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : LeftCancelMonoid 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 : LeftCancelMonoid 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 : LeftCancelMonoid 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 : RightCancelMonoid G
x : G
m n : ℕ
inr :
  ∀ (this : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]) (hmn : ¬m ≤ n),
    x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
wlog : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
wlog hmn : m ≤ n generalizing m n
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
hmn : ¬m ≤ n
inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
inr₂ inr₃ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]

Premises used: le_of_not_ge, eq_comm, Nat.ModEq.comm
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n_1 m n : ℕ
hmn : m ≤ n
obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
mp : x ^ (m + k) = x ^ m → m + k ≡ m [MOD orderOf x]
mpr : m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]

Tactic:
constructor
-- 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
apply : x ^ k * x ^ m = 1 * x ^ m
⊢ x ^ k = 1

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

Premises used: Iff.mp, mul_right_cancel_iff
-- 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 * x ^ m = x ^ (k + m)

Tactic:
(pow_add _ _ _).symm

Premises used: pow_add, 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 + m) = x ^ (m + k)

Tactic:
simp [Nat.add_comm]

Premises used: Nat.add_comm
-- 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 + k) = x ^ m

Tactic:
h