awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₁ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₅ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), k * x ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
simp_rw₅ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), k * x ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₆ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = HPow.hPow (β := ℤ) g 1
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
simp_rw₅ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), k * x ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
simp_rw₆ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = HPow.hPow (β := ℤ) g 1
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₇ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = g
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℤ
simp_rw : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) ∣ 1
simp_rw₁ :
  Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), (↑1 : ℤ) = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₂ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 = k * x + (↑(orderOf g) : ℤ) * y
simp_rw₃ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ) (y : ℤ), 1 - k * x = (↑(orderOf g) : ℤ) * y
simp_rw₄ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (↑(orderOf g) : ℤ) ∣ 1 - k * x
simp_rw₅ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), k * x ≡ 1 [ZMOD (↑(orderOf g) : ℤ)]
simp_rw₆ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = HPow.hPow (β := ℤ) g 1
simp_rw₇ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), g ^ (k * x) = g
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (↑(orderOf g) : ℤ) = 1
have simp_rw₈ : Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ ∃ (x : ℤ), (g ^ k) ^ x = g
Tactic: simp_rw [← Nat.dvd_one, Int.gcd_dvd_iff, Nat.cast_one, ← Int.sub_eq_iff_eq_add', ← dvd_def,
    ← Int.modEq_iff_dvd, ← zpow_eq_zpow_iff_modEq, zpow_one, zpow_mul, ← mem_zpowers_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℕ
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (orderOf g) = 1
have rw : Membership.mem (γ := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑k : ℤ))) g ↔ k.gcd (orderOf g) = 1
Tactic: rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℕ
rw : Membership.mem (γ := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑k : ℤ))) g ↔ k.gcd (orderOf g) = 1
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (orderOf g) = 1
have rw₁ : Int.gcd (↑k : ℤ) (↑(orderOf g) : ℤ) = 1 ↔ k.gcd (orderOf g) = 1
Tactic: rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
g : G
k : ℕ
rw : Membership.mem (γ := Subgroup G) (zpowers (HPow.hPow (β := ℤ) g (↑k : ℤ))) g ↔ k.gcd (orderOf g) = 1
rw₁ : Int.gcd (↑k : ℤ) (↑(orderOf g) : ℤ) = 1 ↔ k.gcd (orderOf g) = 1
⊢ Membership.mem (γ := Subgroup G) (zpowers (g ^ k)) g ↔ k.gcd (orderOf g) = 1
have rw₂ : k.gcd (orderOf g) = 1 ↔ k.gcd (orderOf g) = 1
Tactic: rw [← zpow_natCast g k, mem_zpowers_zpow_iff, Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
⊢ ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1
have obtain : ∀ (w : ℕ) (hw1 : w > 0) (hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1), ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1
Tactic: obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
⊢ ∃ (i : ℤ) (_ : i ≠ 0), x ^ i = 1
have refine : HPow.hPow (β := ℤ) x (↑w : ℤ) = 1
Tactic: refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun (x_1 : G) ↦ x * x_1) w 1
⊢ HPow.hPow (β := ℤ) x (↑w : ℤ) = 1
have rw : x ^ w = 1
Tactic: rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
x y : G
inst_1 : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ Eq (α := ↥(zpowers y))
    ((zpowersEquivZPowers h : (a : ↥(zpowers x)) → ↥(zpowers y))
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (zpowers x) x_1) (x ^ n) ⋯) :
      ↥(zpowers y))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers y) x) (y ^ n) ⋯ : ↥(zpowers y))
have rw : Eq (α := Fin (orderOf y)) ((finCongr h : (a : Fin (orderOf x)) → Fin (orderOf y)) ⟨n % orderOf x, sorry⟩ : Fin (orderOf y))
  (⟨n % orderOf y, sorry⟩ : Fin (orderOf y))
Tactic: rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivZPowers_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card.{u_1} ↥(zpowers a) ≤ k
have rw : orderOf a ≤ k
Tactic: rw [Fintype.card_zpowers]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
⊢ orderOf x ∣ card G
have h : card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
Tactic: use Fintype.card (G ⧸ zpowers x)
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
⊢ card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
have h : card G = card.{u_1} ↥(zpowers x) * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
Tactic: rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
h : card G = card.{u_1} ↥(zpowers x) * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
⊢ card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
have h₁ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x)) * card.{u_1} ↥(zpowers x)
Tactic: rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
h : card G = card.{u_1} ↥(zpowers x) * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
h₁ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x)) * card.{u_1} ↥(zpowers x)
⊢ card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
have h₂ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x) × ↥(zpowers x))
Tactic: rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
h : card G = card.{u_1} ↥(zpowers x) * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
h₁ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x)) * card.{u_1} ↥(zpowers x)
h₂ : card G = card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x) × ↥(zpowers x))
⊢ card G = orderOf x * card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (zpowers x))
have h₃ : card G = card G
Tactic: rw [← card_zpowers, mul_comm, ← Fintype.card_prod,
    ← Fintype.card_congr groupEquivQuotientProdSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
x : G
⊢ orderOf x ∣ Nat.card G
have inl : ∀ (h : Fintype G), orderOf x ∣ Nat.card G
Tactic: obtain h | h := fintypeOrInfinite G
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
x : G
inl : ∀ (h : Fintype G), orderOf x ∣ Nat.card G
⊢ orderOf x ∣ Nat.card G
have inr : ∀ (h : Infinite G), orderOf x ∣ Nat.card G
Tactic: obtain h | h := fintypeOrInfinite G
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
s : Submonoid G
hs : (↑s : Set G).Finite
x : G
hx : x ∈ s
⊢ orderOf x ≤ Nat.card.{u_6} ↥s
have rw : Nat.card.{u_6} ↥(powers x) ≤ Nat.card.{u_6} ↥s
Tactic: rw [← Nat.card_submonoidPowers]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
⊢ x ^ card G = 1
have rw : x ^ Nat.card G = 1
Tactic: rw [← Nat.card_eq_fintype_card, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
x : G
rw : x ^ Nat.card G = 1
⊢ x ^ card G = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← Nat.card_eq_fintype_card, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
⊢ g ^ H.index ∈ H
have rw : Eq (α := G ⧸ H) (↑(g ^ H.index) : G ⧸ H) 1
Tactic: rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
rw : Eq (α := G ⧸ H) (↑(g ^ H.index) : G ⧸ H) 1
⊢ g ^ H.index ∈ H
have rw₁ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) H.index = 1
Tactic: rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
rw : Eq (α := G ⧸ H) (↑(g ^ H.index) : G ⧸ H) 1
rw₁ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) H.index = 1
⊢ g ^ H.index ∈ H
have rw₂ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) (Nat.card.{u_6} (G ⧸ H)) = 1
Tactic: rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
H : Subgroup G
inst_1 : H.Normal
g : G
rw : Eq (α := G ⧸ H) (↑(g ^ H.index) : G ⧸ H) 1
rw₁ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) H.index = 1
rw₂ : HPow.hPow (α := G ⧸ H) (↑g : G ⧸ H) (Nat.card.{u_6} (G ⧸ H)) = 1
⊢ g ^ H.index ∈ H
have rw₃ : Eq.{u_6 + 1} (α := G ⧸ H) 1 1
Tactic: rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G) = a ^ n
have rw : a ^ n = a ^ (n % card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℕ
rw : a ^ n = a ^ (n % card G)
⊢ a ^ (n % card G) = a ^ n
have rw₁ : a ^ (n % orderOf a) = a ^ (n % card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℕ
rw : a ^ n = a ^ (n % card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % card G)
⊢ a ^ (n % card G) = a ^ n
have rw₂ : a ^ (n % card G % orderOf a) = a ^ (n % card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℕ
rw : a ^ n = a ^ (n % card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % card G)
rw₂ : a ^ (n % card G % orderOf a) = a ^ (n % card G)
⊢ a ^ (n % card G) = a ^ n
have rw₃ : a ^ (n % card G) = a ^ (n % card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℤ
⊢ a ^ (n % (↑(card G) : ℤ)) = a ^ n
have rw : a ^ n = a ^ (n % (↑(card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(card G) : ℤ))
⊢ a ^ (n % (↑(card G) : ℤ)) = a ^ n
have rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
⊢ a ^ (n % (↑(card G) : ℤ)) = a ^ n
have rw₂ : a ^ (n % (↑(card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
rw₂ : a ^ (n % (↑(card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
⊢ a ^ (n % (↑(card G) : ℤ)) = a ^ n
have rw₃ : a ^ (n % (↑(card G) : ℤ)) = a ^ (n % (↑(card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ n
have rw : a ^ n = a ^ (n % Nat.card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℕ
rw : a ^ n = a ^ (n % Nat.card G)
⊢ a ^ (n % Nat.card G) = a ^ n
have rw₁ : a ^ (n % orderOf a) = a ^ (n % Nat.card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℕ
rw : a ^ n = a ^ (n % Nat.card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % Nat.card G)
⊢ a ^ (n % Nat.card G) = a ^ n
have rw₂ : a ^ (n % Nat.card G % orderOf a) = a ^ (n % Nat.card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℕ
rw : a ^ n = a ^ (n % Nat.card G)
rw₁ : a ^ (n % orderOf a) = a ^ (n % Nat.card G)
rw₂ : a ^ (n % Nat.card G % orderOf a) = a ^ (n % Nat.card G)
⊢ a ^ (n % Nat.card G) = a ^ n
have rw₃ : a ^ (n % Nat.card G) = a ^ (n % Nat.card G)
Tactic: rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℤ
⊢ a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ n
have rw : a ^ n = a ^ (n % (↑(Nat.card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(Nat.card G) : ℤ))
⊢ a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ n
have rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(Nat.card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
⊢ a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ n
have rw₂ : a ^ (n % (↑(Nat.card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_6
inst : Group G
a : G
n : ℤ
rw : a ^ n = a ^ (n % (↑(Nat.card G) : ℤ))
rw₁ : a ^ (n % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
rw₂ : a ^ (n % (↑(Nat.card G) : ℤ) % (↑(orderOf a) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
⊢ a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ n
have rw₃ : a ^ (n % (↑(Nat.card G) : ℤ)) = a ^ (n % (↑(Nat.card G) : ℤ))
Tactic: rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]