awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : 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
refine : ∀ (h : (↑(↑a : Kˣ) : K) ^ k - 1 = 0), a ^ k = 1
⊢ Eq.{u_1 + 1} (α := K) (Multiset.sum (Multiset.map (fun (x : ↥G) ↦ (↑(↑x : Kˣ) : K) ^ k) (val univ))) 0

Tactic:
refine hzero.resolve_left fun h => ha ?_

Premises used: Or.resolve_left
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
⊢ a ^ k = 1

Tactic:
ext
-- Module: Mathlib.FieldTheory.Finite.Basic
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)

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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₃ : (↑(↑a : Kˣ) : K) ^ k - (↑1 : K) = 0
a₄ : (↑(↑a : Kˣ) : K) ^ k - 1 = 0
⊢ (↑(↑(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]

Premises used: OneMemClass.coe_one, SubmonoidClass.coe_pow, Units.val_one, Units.val_pow_eq_pow_val
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
rw₁ rw₂ : a ^ (q - 1) = a ^ (q - 1)
⊢ a ^ (q - 1) = (↑(Units.mk0 a ha ^ (q - 1)) : K)

Tactic:
rw [Units.val_pow_eq_pow_val, Units.val_mk0]

Premises used: Units.val_pow_eq_pow_val, Units.val_mk0
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
rw : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
⊢ (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1

Tactic:
rw [← Fintype.card_units, pow_card_eq_one]

Premises used: pow_card_eq_one, Fintype.card_units
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := K) (↑1 : K) 1

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw₁ rw₂ rw₃ : Eq.{u_1 + 1} (α := K) (↑1 : K) 1
⊢ (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1

Tactic:
classical
        rw [← Fintype.card_units, pow_card_eq_one]
        rfl

Premises used: pow_card_eq_one, Fintype.card_units
-- Module: Mathlib.FieldTheory.Finite.Basic
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₂ : (↑(Units.mk0 a ha ^ (q - 1)) : K) = 1
⊢ a ^ (q - 1) = 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

Premises used: Units.val, HSub.hSub, Fintype.card, Units.mk0, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
pos : ∀ (h : a = 0), a ^ q = a
neg : ∀ (h : ¬a = 0), a ^ q = a
⊢ a ^ q = a

Tactic:
by_cases h : a = 0
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : a = 0
pos : HPow.hPow (α := K) 0 q = 0
⊢ a ^ q = a

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
h : a = 0
⊢ HPow.hPow (α := K) 0 q = 0

Tactic:
apply zero_pow Fintype.card_ne_zero

Premises used: Fintype.card_ne_zero, zero_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
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
neg₄ neg₅ : a = a
⊢ a ^ q = 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]

Premises used: FiniteField.pow_card_sub_one_eq_one, Nat.succ_pred_eq_of_pos, pow_succ, Nat.pred_eq_sub_one, Fintype.card_pos, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
⊢ a ^ HPow.hPow (β := ℕ) q 0 = a

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ (n + 1) = a

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

Premises used: pow_succ, pow_mul, FiniteField.pow_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : GroupWithZero K
inst_1 : Fintype K
n : ℕ
a : K
zero : a ^ HPow.hPow (β := ℕ) q 0 = a
succ : ∀ (n : ℕ) (ih : a ^ q ^ n = a), a ^ q ^ (n + 1) = a
⊢ a ^ q ^ n = a

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Premises used: pow_succ, pow_mul, FiniteField.pow_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
⊢ Fact (Nat.Prime p)

Tactic:
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
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
obtain : ∀ (n : ℕ) (h : q = Fintype.card (ZMod p) ^ n), ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)

Tactic:
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K

Premises used: ZMod, VectorSpace.card_fintype
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ q = p ^ n

Tactic:
rw [ZMod.card] at h

Premises used: ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : ℕ)

Tactic:
⟨⟨n, ?_⟩, hp.1, h⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Fact.out
-- Module: Mathlib.FieldTheory.Finite.Basic
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
refine : 0 < n
⊢ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)

Tactic:
refine ⟨⟨n, ?_⟩, hp.1, h⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
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
apply : ¬n = 0
⊢ 0 < n

Tactic:
apply Or.resolve_left (Nat.eq_zero_or_pos n)

Premises used: Or.resolve_left, Nat.eq_zero_or_pos
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ q = 1

Tactic:
rw [pow_zero] at h

Premises used: pow_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ Eq.{u_1 + 1} (α := K) 0 1

Tactic:
apply Fintype.card_le_one_iff.mp (le_of_eq h)

Premises used: Fintype.card_le_one_iff, Iff.mp, le_of_eq
-- Module: Mathlib.FieldTheory.Finite.Basic
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
⊢ Eq.{u_1 + 1} (α := K) 0 1

Tactic:
have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this_1 : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
h : q = 1
this : Eq.{u_1 + 1} (α := K) 0 1
⊢ False

Tactic:
absurd this zero_ne_one

Premises used: zero_ne_one, absurd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
inst_2 : CharP K p
hp : Fact (Nat.Prime p)
this_1 : Module (ZMod p) K :=
  let __src : Module (ZMod p) K := RingHom.toModule (ZMod.castHom ⋯ K);
  __src
h : q = 1
this : Eq.{u_1 + 1} (α := K) 0 1
⊢ False

Tactic:
exact absurd this zero_ne_one

Premises used: zero_ne_one, absurd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
⊢ ∃ (p : ℕ), CharP K p ∧ ∃ (n : ℕ+), Nat.Prime p ∧ q = p ^ (↑n : ℕ)

Tactic:
let ⟨p, hc⟩ := CharP.exists K
  ⟨p, hc, @FiniteField.card K _ _ p hc⟩

Premises used: PNat.val, Nat.Prime, CharP.exists, Exists, Fintype.card, And, FiniteField.card, HPow.hPow, And.intro, Exists.intro, CharP, _private.0.FiniteField.card'.match_1, Eq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
obtain : ∀ (p : ℕ), CharP K p → ∀ (n : ℕ+) (hp : Nat.Prime p) (hn : q = p ^ (↑n : ℕ)), IsPrimePow q
⊢ IsPrimePow q

Tactic:
obtain ⟨p, _, n, hp, hn⟩ := card' K

Premises used: FiniteField.card'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
left : CharP K p
n : ℕ+
hp : Nat.Prime p
hn : q = p ^ (↑n : ℕ)
⊢ IsPrimePow q

Tactic:
⟨p, n, Nat.prime_iff.mp hp, n.prop, hn.symm⟩

Premises used: PNat.val, Nat.prime_iff, IsPrimePow, Subtype.prop, And.intro, Exists.intro, Iff.mp, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p : ℕ
left : CharP K p
n : ℕ+
hp : Nat.Prime p
hn : q = p ^ (↑n : ℕ)
⊢ IsPrimePow q

Tactic:
exact ⟨p, n, Nat.prime_iff.mp hp, n.prop, hn.symm⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
⊢ Eq.{u_1 + 1} (α := K) (↑q : K) 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
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

Tactic:
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.FieldTheory.Finite.Basic
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
rw : (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ q - 1 ∣ i

Tactic:
rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
      orderOf_dvd_iff_pow_eq_one]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.card_units, orderOf_dvd_iff_pow_eq_one, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
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
mpr : x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ x ^ i = 1

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Kˣ), x ^ i = 1
⊢ x ^ i = 1

Tactic:
apply h
-- Module: Mathlib.FieldTheory.Finite.Basic
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ˣ
⊢ ∀ (x_1 : Kˣ), Membership.mem (γ := Submonoid Kˣ) (Submonoid.powers x) x_1

Tactic:
simp_rw [← mem_powers_iff_mem_zpowers] at hx

Premises used: mem_powers_iff_mem_zpowers
-- Module: Mathlib.FieldTheory.Finite.Basic
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
mpr : ∀ (j : ℕ), HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1
⊢ y ^ i = 1

Tactic:
rcases hx y with ⟨j, rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
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
mpr₄ mpr₅ : Eq.{u_1 + 1} (α := Kˣ) 1 1
⊢ HPow.hPow (α := Kˣ) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) i = 1

Tactic:
rw [← pow_mul, mul_comm, pow_mul, h, one_pow]

Premises used: one_pow, pow_mul, mul_comm
-- Module: Mathlib.FieldTheory.Finite.Basic
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
mpr mpr₁ :
  ∀ (x : Kˣ) (hx : ∀ (x_1 : Kˣ), Membership.mem (γ := Subgroup Kˣ) (Subgroup.zpowers x) x_1),
    x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 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]

Premises used: one_pow, Nat.card_units, IsCyclic.exists_generator, pow_mul, mul_comm, mem_powers_iff_mem_zpowers, orderOf_dvd_iff_pow_eq_one, rfl, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
⊢ HPow.hPow (α := K) (↑1 : K) i = 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
⊢ ∀ (x y : Kˣ), (↑(x * y) : K) ^ i = (↑x : K) ^ i * (↑y : K) ^ i

Tactic:
simp [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
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' := ⋯ }
⊢ Decidable (φ = 1)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Finite.Basic
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' := ⋯ }
⊢ Decidable (φ = 1)

Tactic:
classical infer_instance
-- Module: Mathlib.FieldTheory.Finite.Basic
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' := ⋯ }
have : ∀ (this : Decidable (φ = 1)), Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) (if q - 1 ∣ i then -1 else 0)
⊢ 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
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Decidable (φ = 1)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (φ : (a : Kˣ) → K) x) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K)

Tactic:
sum_hom_units φ

Premises used: sum_hom_units
-- Module: Mathlib.FieldTheory.Finite.Basic
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
simp : Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if φ = 1 then -1 else 0)
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if q - 1 ∣ i then -1 else 0)

Tactic:
simp only [this]
-- Module: Mathlib.FieldTheory.Finite.Basic
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)
neg : ¬φ = 1 → Eq.{u_1 + 1} (α := K) (↑0 : K) 0
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if φ = 1 then -1 else 0)

Tactic:
split_ifs
-- Module: Mathlib.FieldTheory.Finite.Basic
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
h : ¬φ = 1
⊢ Eq.{u_1 + 1} (α := K) (↑0 : K) 0

Tactic:
Nat.cast_zero

Premises used: Nat.cast_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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
h : ¬φ = 1
⊢ Eq.{u_1 + 1} (α := K) (↑0 : K) 0

Tactic:
exact Nat.cast_zero

Premises used: Nat.cast_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
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
h : φ = 1
pos : 1 ≤ q
⊢ Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} Kˣ) : K) (-1)

Tactic:
rw [Fintype.card_units, Nat.cast_sub,
              cast_card_eq_zero, Nat.cast_one, zero_sub]

Premises used: Nat.cast_sub, FiniteField.cast_card_eq_zero, Fintype.card_units, Nat.cast_one, zero_sub
-- Module: Mathlib.FieldTheory.Finite.Basic
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
h : φ = 1
⊢ 1 ≤ q

Tactic:
Fintype.card_pos_iff.mpr ⟨0⟩

Premises used: Iff.mpr, Nonempty.intro, OfNat.ofNat, Fintype.card_pos_iff, Nat.lt
-- Module: Mathlib.FieldTheory.Finite.Basic
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
h : φ = 1
⊢ 1 ≤ q

Tactic:
exact Fintype.card_pos_iff.mpr ⟨0⟩

Premises used: Iff.mpr, Nonempty.intro, OfNat.ofNat, Fintype.card_pos_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Decidable (φ = 1)
suffices : 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)

Tactic:
suffices q - 1 ∣ i ↔ φ = 1 by
          simp only [this]
          split_ifs; swap
          · exact Nat.cast_zero
          · rw [Fintype.card_units, Nat.cast_sub,
              cast_card_eq_zero, Nat.cast_one, zero_sub]
            show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Decidable (φ = 1)
rw : (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), Eq (α := K) ((φ : (a : Kˣ) → K) x : K) ((1 : (a : Kˣ) → K) x : K)
⊢ q - 1 ∣ i ↔ φ = 1

Tactic:
rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]

Premises used: FiniteField.forall_pow_eq_one_iff, DFunLike.ext_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
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 : Decidable (φ = 1)
h : ∀ (a : Kˣ), a ^ i = 1 ↔ Eq (α := K) ((φ : (a : Kˣ) → K) a : K) ((1 : (a : Kˣ) → K) a : K)
⊢ (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), Eq (α := K) ((φ : (a : Kˣ) → K) x : K) ((1 : (a : Kˣ) → K) x : K)

Tactic:
apply forall_congr'

Premises used: forall_congr'