awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)) : ℕ)
⊢ ((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))
have rw₄ : x ^ (n % orderOf x) = x ^ (n % orderOf x)
Tactic: rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have 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]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have wlog : ∀ {n m : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₂ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n_1 m_1 : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Monoid G
x : G
n m_1 : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
have rw : k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Tactic: rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m n : ℕ
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have 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]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have wlog : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₂ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n_1 m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
have rw : k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Tactic: rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
⊢ (Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n) ↔ ¬IsOfFinOrder x
have refine : ∀ (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 => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ n = m
have rwa : ∀ (hnm : n ≡ m [MOD orderOf x]), n = m
Tactic: rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have rwa₁ : ∀ (hnm : n ≡ m [MOD 0]), n = m
Tactic: rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have rwa₂ : ∀ (hnm : n = m), n = m
Tactic: rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m
have rw : n ≡ m [MOD orderOf x] ↔ n = m
Tactic: rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
rw : n ≡ m [MOD orderOf x] ↔ n = m
⊢ x ^ n = x ^ m ↔ n = m
have rw₁ : n ≡ m [MOD 0] ↔ n = m
Tactic: rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n = x ^ m ↔ n = m
have rw₂ : n = m ↔ n = m
Tactic: rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ False
have apply : IsOfFinOrder x
Tactic: apply h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ IsOfFinOrder x
have rw : ∀ (contra : ∃ (n_1 : ℕ), 0 < n_1 ∧ (x ^ n) ^ n_1 = 1), ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
have obtain : ∀ (m : ℕ) (hm : 0 < m) (hm' : (x ^ n) ^ m = 1), ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: obtain ⟨m, hm, hm'⟩ := contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
x : G
h : ¬IsOfFinOrder x
s : Set G := (fun (n : ℕ) ↦ x ^ n) '' {n : ℕ | 0 < n}
⊢ Set.Infinite.{u_1} (α := G) {y : G | ¬IsOfFinOrder y}
have hs : 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]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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}
⊢ Set.Infinite.{u_1} (α := G) {y : G | ¬IsOfFinOrder y}
have suffices : s.Infinite
Tactic: suffices s.Infinite by exact this.mono hs
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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}
⊢ s.Infinite
have contrapose! : ∀ (h : s.Finite), IsOfFinOrder x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
have this : ¬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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ ¬Injective.{1, u_1 + 1} (β := G) fun (n : ℕ) ↦ x ^ n
have 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)
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ IsOfFinOrder x
have this : ¬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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ IsOfFinOrder x
have rwa : ∀ (this : ¬¬IsOfFinOrder x), IsOfFinOrder x
Tactic: rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ IsOfFinOrder x
have rwa₁ : ∀ (this : IsOfFinOrder x), IsOfFinOrder x
Tactic: rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
⊢ (↑(powers a) : Set G).Finite ↔ IsOfFinOrder a
have refine : ∀ (h : (↑(powers a) : Set G).Finite), IsOfFinOrder a
Tactic: refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
⊢ IsOfFinOrder a
have obtain : ∀ (m n : ℕ) (hmn : m < n) (ha : a ^ m = a ^ n), 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])
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
have refine : a ^ (n - m) = 1
Tactic: refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ a ^ (n - m) = 1
have rw : a ^ m * a ^ (n - m) = a ^ m * 1
Tactic: rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ a ^ (n - m) = 1
have rw₁ : a ^ (m + (n - m)) = a ^ m * 1
Tactic: rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ a ^ (n - m) = 1
have rw₂ : a ^ n = a ^ m * 1
Tactic: rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ a ^ (n - m) = 1
have rw₃ : a ^ n = a ^ n * 1
Tactic: rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ a ^ (n - m) = 1
have rw₄ : a ^ n = a ^ n
Tactic: rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have pos : ∀ (ha : IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
Tactic: by_cases ha : IsOfFinOrder a
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
pos : ∀ (ha : IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have neg : ∀ (ha : ¬IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
Tactic: by_cases ha : IsOfFinOrder a
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have this : Infinite.{u_1 + 1} (↑(↑(powers a) : Set G) : Type u_1)
Tactic: have := (infinite_powers.2 ha).to_subtype
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have neg : Nat.card.{u_1} ↥(powers a) = 0
Tactic: rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have pos : ∀ (ha : IsOfFinOrder 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : LeftCancelMonoid G
a : G
pos : ∀ (ha : IsOfFinOrder a), Nat.card.{u_1} ↥(powers a) = orderOf a
⊢ Nat.card.{u_1} ↥(powers a) = orderOf a
have neg : ∀ (ha : ¬IsOfFinOrder 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m n : ℕ
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have 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]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have wlog : ∀ {m n : ℕ} (hmn : m ≤ n), x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Tactic: wlog hmn : m ≤ n generalizing m n
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr : x ^ m = x ^ n ↔ n ≡ m [MOD orderOf x]
Tactic: rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₁ : x ^ m = x ^ n ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have inr₂ : m ≡ n [MOD orderOf x] ↔ m ≡ n [MOD orderOf x]
Tactic: rw [eq_comm, Nat.ModEq.comm, this (le_of_not_ge hmn)]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n_1 m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid G
x : G
m_1 n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
have mp : x ^ (m + k) = x ^ m → m + k ≡ m [MOD orderOf x]
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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]
⊢ x ^ (m + k) = x ^ m ↔ m + k ≡ m [MOD orderOf x]
have mpr : m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
have apply : x ^ k * x ^ m = 1 * x ^ m
Tactic: apply (mul_right_cancel_iff (a := x ^ m)).1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 = 1 * x ^ m
have x₁ : x ^ (k + m) = x ^ (m + k)
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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 ^ k * x ^ m = 1 * x ^ m
have x₂ : 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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ m + k ≡ m [MOD orderOf x]
have hk : 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