awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
⊢ a ^ k = 1
have a₁ : (↑(↑(a ^ k) : Kˣ) : K) = (↑(↑1 : Kˣ) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
⊢ (↑(↑(a ^ k) : Kˣ) : K) = (↑(↑1 : Kˣ) : K)
have a₁ : (↑(↑(a ^ k) : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
⊢ (↑(↑(a ^ k) : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
have a₁ : (↑((↑a : Kˣ) ^ k) : K) - (↑(↑1 : Kˣ) : K) = 0
Tactic: simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, Units.val_one, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
a₁ : (↑((↑a : Kˣ) ^ k) : K) - (↑(↑1 : Kˣ) : K) = 0
⊢ (↑(↑(a ^ k) : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
have a₂ : (↑(↑a : Kˣ) : K) ^ k - (↑(↑1 : Kˣ) : K) = 0
Tactic: simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, Units.val_one, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : CommRing K
inst_1 : NoZeroDivisors K
G : Subgroup Kˣ
inst_2 : Fintype ↥G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card.{u_1} ↥G
h_1 : Nontrivial K
this : IsDomain K
a : ↥G
ha : a ^ k ≠ 1
h_multiset_map :
  Eq.{u_1 + 1} (α := Multiset K) (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))
    (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k * (↑(↑a : Kˣ) : K) ^ k) (val univ))
h_multiset_map_sum :
  Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) =
    Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ)) * (↑(↑a : Kˣ) : K) ^ k
hzero :
  (↑(↑a : Kˣ) : K) ^ k - 1 = 0 ∨
    Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (i : ↥G) ↦ (↑(↑i : Kˣ) : K) ^ k) (val univ))) 0
h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
a₁ : (↑((↑a : Kˣ) ^ k) : K) - (↑(↑1 : Kˣ) : K) = 0
a₂ : (↑(↑a : Kˣ) : K) ^ k - (↑(↑1 : Kˣ) : K) = 0
⊢ (↑(↑(a ^ k) : Kˣ) : K) - (↑(↑1 : Kˣ) : K) = 0
have a₃ : (↑(↑a : Kˣ) : K) ^ k - (↑1 : K) = 0
Tactic: simp_rw [SubmonoidClass.coe_pow, Units.val_pow_eq_pow_val, OneMemClass.coe_one, Units.val_one, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = (↑(Units.mk0 a ha ^ (q - 1)) : K)
have rw : a ^ (q - 1) = (↑(Units.mk0 a ha) : K) ^ (q - 1)
Tactic: rw [Units.val_pow_eq_pow_val, Units.val_mk0]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
rw : a ^ (q - 1) = (↑(Units.mk0 a ha) : K) ^ (q - 1)
⊢ a ^ (q - 1) = (↑(Units.mk0 a ha ^ (q - 1)) : K)
have rw₁ : a ^ (q - 1) = a ^ (q - 1)
Tactic: rw [Units.val_pow_eq_pow_val, Units.val_mk0]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
⊢ (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1
have rw : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
Tactic: rw [← Fintype.card_units, pow_card_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
⊢ (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1
have rw : (↑(Units.mk0 a ha ^ Fintype.card.{u_1} Kˣ) : K) = 1
Tactic: classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
rw : (↑(Units.mk0 a ha ^ Fintype.card.{u_1} Kˣ) : K) = 1
⊢ (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1
have rw₁ : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
Tactic: classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = 1
have a₁ : a ^ (q - 1) = (↑(Units.mk0 a ha ^ (q - 1)) : K)
Tactic: calc
    a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
      rw [Units.val_pow_eq_pow_val, Units.val_mk0]
    _ = 1 := by
      classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
a₁ : a ^ (q - 1) = (↑(Units.mk0 a ha ^ (q - 1)) : K)
⊢ a ^ (q - 1) = 1
have a₂ : (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1
Tactic: calc
    a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
      rw [Units.val_pow_eq_pow_val, Units.val_mk0]
    _ = 1 := by
      classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
⊢ a ^ q = a
have pos : ∀ (h : a = 0), a ^ q = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
pos : ∀ (h : a = 0), a ^ q = a
⊢ a ^ q = a
have neg : ∀ (h : ¬a = 0), a ^ q = a
Tactic: by_cases h : a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : a = 0
⊢ a ^ q = a
have pos : HPow.hPow (α := K) 0 q = 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : ¬a = 0
⊢ a ^ q = a
have neg : a ^ q.pred.succ = a
Tactic: rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
    pow_card_sub_one_eq_one a h, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : ¬a = 0
neg : a ^ q.pred.succ = a
⊢ a ^ q = a
have neg₁ : a ^ q.pred * a = a
Tactic: rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
    pow_card_sub_one_eq_one a h, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : ¬a = 0
neg : a ^ q.pred.succ = a
neg₁ : a ^ q.pred * a = a
⊢ a ^ q = a
have neg₂ : a ^ (q - 1) * a = a
Tactic: rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
    pow_card_sub_one_eq_one a h, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : ¬a = 0
neg : a ^ q.pred.succ = a
neg₁ : a ^ q.pred * a = a
neg₂ : a ^ (q - 1) * a = a
⊢ a ^ q = a
have neg₃ : 1 * a = a
Tactic: rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
    pow_card_sub_one_eq_one a h, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : ¬a = 0
neg : a ^ q.pred.succ = a
neg₁ : a ^ q.pred * a = a
neg₂ : a ^ (q - 1) * a = a
neg₃ : 1 * a = a
⊢ a ^ q = a
have neg₄ : a = a
Tactic: rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one,
    pow_card_sub_one_eq_one a h, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a
have zero : a ^ HPow.hPow (β := ℕ) q 0 = a
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
n : ℕ
a : K
zero : a ^ HPow.hPow (β := ℕ) q 0 = a
⊢ a ^ q ^ n = a
have succ : ∀ (n : ℕ) (ih : a ^ q ^ n = a), a ^ q ^ (n + 1) = a
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
have hp : Fact (Nat.Prime p)
Tactic: haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
have obtain : ∀ (n : ℕ) (h : q = Fintype.card (ZMod p) ^ n), ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
Tactic: obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
have h₁ : q = p ^ n
Tactic: rw [ZMod.card] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
n : ℕ
h : q = p ^ n
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
have refine : 0 < n
Tactic: refine ⟨⟨n, ?_⟩, hp.1, h⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
n : ℕ
h : q = p ^ n
⊢ 0 < n
have apply : ¬n = 0
Tactic: apply Or.resolve_left (Nat.eq_zero_or_pos n)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
h : q = HPow.hPow (β := ℕ) p 0
⊢ False
have h₁ : q = 1
Tactic: rw [pow_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
h : q = 1
⊢ False
have this₁ : Eq.{u_1 + 1} (α := K) 0 1
Tactic: have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
⊢ IsPrimePow q
have obtain : ∀ (p : ℕ), CharP K p → ∀ (n : ℕ+) (hp : Nat.Prime p) (hn : q = p ^ (↑n : ℕ)), IsPrimePow q
Tactic: obtain ⟨p, _, n, hp, hn⟩ := card' K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have obtain : ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
  (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
Tactic: obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have rw : (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
Tactic: rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
have mp : (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1
mp : (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
have mpr : x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1
h : x ^ i = 1
y : Kˣ
⊢ y ^ i = 1
have hx₁ : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
Tactic: simp_rw [← mem_powers_iff_mem_zpowers] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
y : Kˣ
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
⊢ y ^ i = 1
have mpr : ∀ (j : ℕ), HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
Tactic: rcases hx y with ⟨j, rfl⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
j : ℕ
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
have mpr : x ^ (j * i) = 1
Tactic: rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
j : ℕ
mpr : x ^ (j * i) = 1
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
have mpr₁ : x ^ (i * j) = 1
Tactic: rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
j : ℕ
mpr : x ^ (j * i) = 1
mpr₁ : x ^ (i * j) = 1
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
have mpr₂ : (x ^ i) ^ j = 1
Tactic: rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
j : ℕ
mpr : x ^ (j * i) = 1
mpr₁ : x ^ (i * j) = 1
mpr₂ : (x ^ i) ^ j = 1
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
have mpr₃ : HPow.hPow (α := Kˣ) 1 j = 1
Tactic: rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
x : Kˣ
h : x ^ i = 1
hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1
j : ℕ
mpr : x ^ (j * i) = 1
mpr₁ : x ^ (i * j) = 1
mpr₂ : (x ^ i) ^ j = 1
mpr₃ : HPow.hPow (α := Kˣ) 1 j = 1
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
have mpr₄ : Eq.{u_1 + 1} (α := Kˣ) 1 1
Tactic: rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have obtain : ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
  (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
Tactic: classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
    rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]
    constructor
    · intro h; apply h
    · intro h y
      simp_rw [← mem_powers_iff_mem_zpowers] at hx
      rcases hx y with ⟨j, rfl⟩
      rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
obtain :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have obtain₁ : ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
  (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
Tactic: classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
    rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]
    constructor
    · intro h; apply h
    · intro h y
      simp_rw [← mem_powers_iff_mem_zpowers] at hx
      rcases hx y with ⟨j, rfl⟩
      rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
obtain :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
obtain₁ :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have mp : ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
  (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
Tactic: classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
    rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]
    constructor
    · intro h; apply h
    · intro h y
      simp_rw [← mem_powers_iff_mem_zpowers] at hx
      rcases hx y with ⟨j, rfl⟩
      rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
obtain :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
obtain₁ :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
mp :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    (∀ (x : Kˣ), x ^ i = 1) → x ^ i = 1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i
have mpr : ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
  x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
Tactic: classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
    rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]
    constructor
    · intro h; apply h
    · intro h y
      simp_rw [← mem_powers_iff_mem_zpowers] at hx
      rcases hx y with ⟨j, rfl⟩
      rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
⊢ Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) (if q - 1 ∣ i then -1 else 0)
have have : ∀ (this : Decidable (φ = 1)), Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) (if q - 1 ∣ i then -1 else 0)
Tactic: have : Decidable (φ = 1) := by classical infer_instance
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
this_1 : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if q - 1 ∣ i then -1 else 0)
have simp : Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if φ = 1 then -1 else 0)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
this_1 : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if φ = 1 then -1 else 0)
have pos : φ = 1 → Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} Kˣ) : K) (-1)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
this_1 : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
pos : φ = 1 → Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} Kˣ) : K) (-1)
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if φ = 1 then -1 else 0)
have neg : ¬φ = 1 → Eq.{u_1 + 1} (α := K) (↑0 : K) 0
Tactic: split_ifs