awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : m + k ≡ m [MOD orderOf x]
⊢ x ^ k = 1
have apply : k ≡ 0 [MOD orderOf x]
Tactic: apply pow_eq_one_iff_modEq.2
-- 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 : m + k ≡ m [MOD orderOf x]
⊢ x ^ (m + k) = x ^ m
have hk : 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)
-- 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 : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m * x ^ k
have rw : x ^ m * x ^ k = x ^ m * x ^ k
Tactic: rw [pow_add]
-- 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 : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
⊢ x ^ (m + k) = x ^ m
have x₁ : x ^ (m + k) = x ^ m * x ^ k
Tactic: calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]
-- 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 : m + k ≡ m [MOD orderOf x]
hk : x ^ k = 1
x₁ : x ^ (m + k) = x ^ m * x ^ k
⊢ x ^ (m + k) = x ^ m
have x₂ : x ^ m * x ^ k = x ^ m
Tactic: calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid 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 : 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)
⊢ 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, Nat.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have rwa₁ : ∀ (hnm : n ≡ m [MOD 0]), n = m
Tactic: rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, Nat.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ n = m
have rwa₂ : ∀ (hnm : n = m), n = m
Tactic: rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, Nat.modEq_zero_iff] at hnm
Cleared hypotheses: hnm
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid 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, Nat.modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid 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, Nat.modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ x ^ n = x ^ m ↔ n = m
have rw₂ : n = m ↔ n = m
Tactic: rw [pow_eq_pow_iff_modEq, h, Nat.modEq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ False
have apply : IsOfFinOrder x
Tactic: apply h
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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)
⊢ 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 : 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
⊢ ∃ (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 : RightCancelMonoid 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : 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
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 : 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)
⊢ ¬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 : RightCancelMonoid 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 : ¬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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ 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 : 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
⊢ 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : RightCancelMonoid G
a : G
h : (↑(powers a) : Set G).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) = 1
have apply : a ^ (n - m) * a ^ m = 1 * a ^ m
Tactic: apply (mul_right_cancel_iff (a := a ^ m)).1
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 = 1 * a ^ m
have a₁ : a ^ (n - m + m) = a ^ n
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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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 ^ (n - m) * a ^ m = 1 * a ^ m
have a₂ : 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
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : RightCancelMonoid 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : 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
⊢ 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 : RightCancelMonoid 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 : RightCancelMonoid 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 : Group G
x : G
i : ℤ
⊢ (↑(orderOf x) : ℤ) ∣ i ↔ x ^ i = 1
have inl : ∀ (i : ℕ), Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
Tactic: rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
inl : ∀ (i : ℕ), Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
⊢ (↑(orderOf x) : ℤ) ∣ i ↔ x ^ i = 1
have inr : ∀ (i : ℕ), Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
Tactic: rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
have inl : orderOf x ∣ i ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
Tactic: rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
inl : orderOf x ∣ i ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
have inl₁ : x ^ i = 1 ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
Tactic: rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (↑i : ℤ) = 1
have inl₂ : x ^ i = 1 ↔ x ^ i = 1
Tactic: rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℕ
inr : Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (↑i : ℤ) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr₁ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr₂ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr₃ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr₄ : orderOf x ∣ i ↔ x ^ i = 1
Tactic: rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Dvd.dvd (α := ℤ) (↑(orderOf x) : ℤ) (-(↑i : ℤ)) ↔ HPow.hPow (β := ℤ) x (-(↑i : ℤ)) = 1
have inr₅ : x ^ i = 1 ↔ x ^ i = 1
Tactic: rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
a b : ℤ
⊢ (↑(orderOf x) : ℤ) ∣ a - b ↔ x ^ a = x ^ b
have rw : x ^ (a - b) = 1 ↔ x ^ a = x ^ b
Tactic: rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
a b : ℤ
rw : x ^ (a - b) = 1 ↔ x ^ a = x ^ b
⊢ (↑(orderOf x) : ℤ) ∣ a - b ↔ x ^ a = x ^ b
have rw₁ : x ^ a * (x ^ b)⁻¹ = 1 ↔ x ^ a = x ^ b
Tactic: rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (↑(orderOf x) : ℤ) ∣ a - b ↔ x ^ a = x ^ b
have rw₂ : x ^ a = x ^ b ↔ x ^ a = x ^ b
Tactic: rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
z : ℤ
⊢ x ^ (z % (↑(orderOf x) : ℤ) + (↑(orderOf x) : ℤ) * (z / (↑(orderOf x) : ℤ))) = x ^ z
have rw : x ^ z = x ^ z
Tactic: rw [Int.emod_add_mul_ediv]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
⊢ (x ^ i) ^ orderOf x = 1
have pos : ∀ (h : IsOfFinOrder x), (x ^ i) ^ orderOf x = 1
Tactic: by_cases h : IsOfFinOrder x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
pos : ∀ (h : IsOfFinOrder x), (x ^ i) ^ orderOf x = 1
⊢ (x ^ i) ^ orderOf x = 1
have neg : ∀ (h : ¬IsOfFinOrder x), (x ^ i) ^ orderOf x = 1
Tactic: by_cases h : IsOfFinOrder x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
have pos : HPow.hPow (β := ℤ) (x ^ i) (↑(orderOf x) : ℤ) = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : IsOfFinOrder x
pos : HPow.hPow (β := ℤ) (x ^ i) (↑(orderOf x) : ℤ) = 1
⊢ (x ^ i) ^ orderOf x = 1
have pos₁ : x ^ (i * (↑(orderOf x) : ℤ)) = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (x ^ i) ^ orderOf x = 1
have pos₂ : x ^ ((↑(orderOf x) : ℤ) * i) = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (x ^ i) ^ orderOf x = 1
have pos₃ : HPow.hPow (β := ℤ) x (↑(orderOf x) : ℤ) ^ i = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (x ^ i) ^ orderOf x = 1
have pos₄ : (x ^ orderOf x) ^ i = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (x ^ i) ^ orderOf x = 1
have pos₅ : HPow.hPow (α := G) 1 i = 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ (x ^ i) ^ orderOf x = 1
have pos₆ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
have neg : HPow.hPow (β := ℕ) (x ^ i) 0 = 1
Tactic: rw [orderOf_eq_zero h, _root_.pow_zero]