awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1

Tactic:
rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul,
    pow_two] at h₁

Premises used: pow_two, FiniteField.odd_card_of_char_ne_two, Nat.two_mul_odd_div_two, pow_mul, mul_comm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
mul_self_eq_one_iff.mp h₁

Premises used: mul_self_eq_one_iff, Iff.mp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
exact mul_self_eq_one_iff.mp h₁

Premises used: mul_self_eq_one_iff, Iff.mp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
obtain :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x),
    IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
rw : Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) a
⊢ Membership.mem (γ := Submonoid Fˣ) (Submonoid.powers g) a

Tactic:
rw [mem_powers_iff_mem_zpowers]

Premises used: mem_powers_iff_mem_zpowers
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
⊢ Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) a

Tactic:
apply hg
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
obtain : ∀ (n : ℕ) (hn : (fun (x : ℕ) ↦ g ^ x) n = a), IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg

Premises used: Submonoid.powers
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hn : (fun (x : ℕ) ↦ g ^ x) n = a
⊢ 2 * (Fintype.card F / 2) = Fintype.card F - 1

Tactic:
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hn : (fun (x : ℕ) ↦ g ^ x) n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
mp : IsSquare a → a ^ (Fintype.card F / 2) = 1
mpr : a ^ (Fintype.card F / 2) = 1 → IsSquare a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
mp : y ^ (Fintype.card F - 1) = 1
⊢ (y * y) ^ (Fintype.card F / 2) = 1

Tactic:
rw [← pow_two, ← pow_mul, hodd]

Premises used: pow_two, pow_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := Fˣ) Units.val

Tactic:
Units.val_injective

Premises used: Units.val_injective
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
mp : (↑(y ^ (Fintype.card F - 1)) : F) = (↑1 : F)
⊢ y ^ (Fintype.card F - 1) = 1

Tactic:
apply_fun Units.val using Units.val_injective

Premises used: Units.val, Units.val_injective
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
mp : (↑y : F) ^ (Fintype.card F - 1) = 1
⊢ (↑(y ^ (Fintype.card F - 1)) : F) = (↑1 : F)

Tactic:
push_cast
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
⊢ (↑y : F) ^ (Fintype.card F - 1) = 1

Tactic:
FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)

Premises used: Units.val, FiniteField.pow_card_sub_one_eq_one, Units.ne_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
y : Fˣ
hn : (fun (x : ℕ) ↦ g ^ x) n = y * y
⊢ (↑y : F) ^ (Fintype.card F - 1) = 1

Tactic:
exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)

Premises used: Units.val, FiniteField.pow_card_sub_one_eq_one, Units.ne_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hn : (fun (x : ℕ) ↦ g ^ x) n = a
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
mpr :
  HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Fintype.card F / 2) = 1 →
    IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a

Tactic:
subst a
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Fintype.card F / 2) = 1
⊢ 2 * (Nat.card F / 2) = Nat.card F - 1

Tactic:
rw [← Nat.card_eq_fintype_card] at hodd h

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Fintype.card F / 2) = 1
hodd₁ : 2 * (Nat.card F / 2) = Nat.card F - 1
⊢ HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1

Tactic:
rw [← Nat.card_eq_fintype_card] at hodd h

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
⊢ g ^ (n * (Nat.card F / 2)) = 1

Tactic:
rw [← pow_mul] at h

Premises used: pow_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : g ^ (n * (Nat.card F / 2)) = 1
rw : orderOf g ∣ n * (Nat.card F / 2)
⊢ 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)

Tactic:
rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]

Premises used: orderOf_eq_card_of_forall_mem_zpowers, Nat.card_units
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : g ^ (n * (Nat.card F / 2)) = 1
⊢ orderOf g ∣ n * (Nat.card F / 2)

Tactic:
apply orderOf_dvd_of_pow_eq_one h

Premises used: orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
⊢ 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)

Tactic:
have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) := by
        rw [← pow_mul] at h
        rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
        apply orderOf_dvd_of_pow_eq_one h
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ LT.lt (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
⊢ 0 < Nat.card F / 2

Tactic:
have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
this : 0 < Nat.card F / 2
mpr :
  ∀ (m : ℕ) (h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m)) (Nat.card F / 2) = 1)
    (key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)), IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m))
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)

Tactic:
obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key

Premises used: Nat.dvd_of_mul_dvd_mul_right, rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m)) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m))

Tactic:
⟨g ^ m, ?_⟩

Premises used: HPow.hPow, IsSquare, Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m)) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
mpr : (fun (x : ℕ) ↦ g ^ x) (2 * m) = g ^ m * g ^ m
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m))

Tactic:
refine ⟨g ^ m, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) (2 * m)) (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
mpr : g ^ (m * 2) = g ^ m * g ^ m
mpr₁ : HPow.hPow (β := ℕ) (g ^ m) 2 = g ^ m * g ^ m
mpr₂ mpr₃ : g ^ m * g ^ m = g ^ m * g ^ m
⊢ g ^ (2 * m) = g ^ m * g ^ m

Tactic:
rw [mul_comm, pow_mul, pow_two]

Premises used: pow_two, pow_mul, mul_comm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
obtain :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x),
    IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
obtain₁ :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x) (n : ℕ)
    (hn : (fun (x : ℕ) ↦ g ^ x) n = a), IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
obtain₂ :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x) (n : ℕ)
    (hn : (fun (x : ℕ) ↦ g ^ x) n = a) (hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1),
    IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
mp :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x) (n : ℕ)
    (hn : (fun (x : ℕ) ↦ g ^ x) n = a) (hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1),
    IsSquare a → a ^ (Fintype.card F / 2) = 1
mpr mpr₁ :
  ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x) (n : ℕ)
    (hn : (fun (x : ℕ) ↦ g ^ x) n = a) (hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1),
    a ^ (Fintype.card F / 2) = 1 → IsSquare a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
classical
    obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
    obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg
    have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
    constructor
    · rintro ⟨y, rfl⟩
      rw [← pow_two, ← pow_mul, hodd]
      apply_fun Units.val using Units.val_injective
      push_cast
      exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
    · subst a; intro h
      rw [← Nat.card_eq_fintype_card] at hodd h
      have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) := by
        rw [← pow_mul] at h
        rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
        apply orderOf_dvd_of_pow_eq_one h
      have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
      obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
      refine ⟨g ^ m, ?_⟩
      dsimp
      rw [mul_comm, pow_mul, pow_two]

Premises used: Units.val, pow_two, IsCyclic.exists_generator, pow_mul, mul_comm, Units.val_injective, rfl, Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ HPow.hPow (α := Fˣ) (Units.mk0 a ha : Fˣ) (Fintype.card F / 2) = 1 ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
simp [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
_ : IsSquare (α := Fˣ) (Units.mk0 a ha : Fˣ) ↔ IsSquare a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
apply
    (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))

Premises used: iff_congr, FiniteField.unit_isSquare_iff, Units.mk0, Iff.mp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
simp : (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) ↔ ∃ (r : F), a = r * r
⊢ IsSquare (α := Fˣ) (Units.mk0 a ha : Fˣ) ↔ IsSquare a

Tactic:
simp only [IsSquare, Units.ext_iff, Units.val_mk0, Units.val_mul]

Premises used: Units.ext_iff, IsSquare, Units.val_mk0, Units.val_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
mp : (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) → ∃ (r : F), a = r * r
mpr : (∃ (r : F), a = r * r) → ∃ (r : Fˣ), a = (↑r : F) * (↑r : F)
⊢ (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) ↔ ∃ (r : F), a = r * r

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = (↑y : F) * (↑y : F)
⊢ ∃ (r : F), a = r * r

Tactic:
⟨y, hy⟩

Premises used: Units.val, Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = (↑y : F) * (↑y : F)
⊢ ∃ (r : F), a = r * r

Tactic:
exact ⟨y, hy⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
ha : HMul.hMul (α := F) 0 0 ≠ 0
⊢ False

Tactic:
simp at ha
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := by rintro rfl; simp at ha
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ (r : Fˣ), y * y = (↑r : F) * (↑r : F)

Tactic:
⟨Units.mk0 y hy, ?_⟩

Premises used: Units.mk0, Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
mpr : y * y = (↑(Units.mk0 y hy) : F) * (↑(Units.mk0 y hy) : F)
⊢ ∃ (r : Fˣ), y * y = (↑r : F) * (↑r : F)

Tactic:
refine ⟨Units.mk0 y hy, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = (↑(Units.mk0 y hy) : F) * (↑(Units.mk0 y hy) : F)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
inst_5 : Algebra (ZMod p) k
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ Module.finrank (ZMod p) (GaloisField p (Module.finrank (ZMod p) k * n)) = Module.finrank (ZMod p) k * n

Tactic:
GaloisField.finrank p (n := Module.finrank (ZMod p) k * n) <|
      mul_ne_zero Module.finrank_pos.ne' <| NeZero.ne n

Premises used: GaloisField.finrank, LT.lt.ne', mul_ne_zero, Module.finrank_pos, NeZero.ne
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
inst_5 : Algebra (ZMod p) k
this : Algebra (ZMod p) k := ZMod.algebra k p
h : inst_5 = this
⊢ Module.finrank (ZMod p) (GaloisField p (Module.finrank (ZMod p) k * n)) = Module.finrank (ZMod p) k * n

Tactic:
convert!
    GaloisField.finrank p (n := Module.finrank (ZMod p) k * n) <|
      mul_ne_zero Module.finrank_pos.ne' <| NeZero.ne n

Premises used: GaloisField.finrank, LT.lt.ne', mul_ne_zero, Module.finrank_pos, NeZero.ne
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
inst_5 : Algebra (ZMod p) k
this : Algebra (ZMod p) k := ZMod.algebra k p
⊢ inst_5 = this

Tactic:
subsingleton
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
inst_5 : Algebra (ZMod p) k
⊢ Nonempty.{max 1 (u_1 + 1)} (k →ₐ[ZMod p] Extension k p n)

Tactic:
nonempty_algHom_of_finrank_dvd (finrank_zmod_extension k p n ▸ dvd_mul_right _ _)

Premises used: FiniteField.nonempty_algHom_of_finrank_dvd, Eq.rec, FiniteField.finrank_zmod_extension, dvd_mul_right, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
⊢ Module.Finite k (Extension k p n)

Tactic:
.of_finite

Premises used: Module.Finite.of_finite
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
inst_5 : Algebra (ZMod p) k
⊢ IsScalarTower (ZMod p) k (Extension k p n)

Tactic:
.of_algebraMap_eq' <| Subsingleton.elim _ _

Premises used: IsScalarTower.of_algebraMap_eq', Subsingleton.elim
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Algebra (ZMod p) k := ZMod.algebra k p
rw : p ^ Module.finrank (ZMod p) (Extension k p n) = Nat.card k ^ n
rw₁ : p ^ Module.finrank (ZMod p) (Extension k p n) = (p ^ Module.finrank (ZMod p) k) ^ n
rw₂ : p ^ (Module.finrank (ZMod p) k * n) = (p ^ Module.finrank (ZMod p) k) ^ n
rw₃ rw₄ : (p ^ Module.finrank (ZMod p) k) ^ n = (p ^ Module.finrank (ZMod p) k) ^ n
⊢ Nat.card (Extension k p n) = Nat.card k ^ n

Tactic:
rw [← pow_finrank_eq_natCard p, ← pow_finrank_eq_natCard p, finrank_zmod_extension, pow_mul]

Premises used: FiniteField.pow_finrank_eq_natCard, FiniteField.finrank_zmod_extension, pow_mul
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
⊢ Module.finrank k (Extension k p n) = n

Tactic:
Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_

Premises used: Nat.pow_right_injective, Finite.one_lt_card
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
refine :
  Eq (α := ℕ) ((fun (x : ℕ) ↦ Nat.card k ^ x) (Module.finrank k (Extension k p n))) ((fun (x : ℕ) ↦ Nat.card k ^ x) n)
⊢ Module.finrank k (Extension k p n) = n

Tactic:
refine Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_

Premises used: Nat.pow_right_injective, Finite.one_lt_card
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
⊢ Eq (α := ℕ) ((fun (x : ℕ) ↦ Nat.card k ^ x) (Module.finrank k (Extension k p n))) ((fun (x : ℕ) ↦ Nat.card k ^ x) n)

Tactic:
simp only [← Module.natCard_eq_pow_finrank, natCard_extension]

Premises used: Module.natCard_eq_pow_finrank, FiniteField.natCard_extension
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
have :
  ∀ (this : Fintype (Extension k p n)),
    IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
⊢ IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)

Tactic:
have := Fintype.ofFinite (Extension k p n)
-- Module: Mathlib.FieldTheory.Finite.Extension
Goal:
k : Type u_1
inst : Field k
inst_1 : Finite k
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : CharP k p
n : ℕ
inst_4 : NeZero n
this : Fintype (Extension k p n)
⊢ IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Fintype.card (Extension k p n)) - X)

Tactic:
FiniteField.isSplittingField_sub (Extension k p n) k

Premises used: FiniteField.isSplittingField_sub, FiniteField.Extension