awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have hodd : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have mp : IsSquare a → a ^ (Fintype.card F / 2) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have mpr : a ^ (Fintype.card F / 2) = 1 → IsSquare a
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 * y) ^ (Fintype.card F / 2) = 1
have mp : y ^ (Fintype.card F - 1) = 1
Tactic: rw [← pow_two, ← pow_mul, hodd]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 ^ (Fintype.card F - 1) = 1
have mp : (↑(y ^ (Fintype.card F - 1)) : F) = (↑1 : F)
Tactic: apply_fun Units.val using Units.val_injective
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 ^ (Fintype.card F - 1)) : F) = (↑1 : F)
have mp : (↑y : F) ^ (Fintype.card F - 1) = 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ a ^ (Fintype.card F / 2) = 1 → IsSquare a
have mpr : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Fintype.card F / 2) = 1 →
  IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
Tactic: subst a
Cleared hypotheses: a, hn
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
have hodd₁ : 2 * (Nat.card F / 2) = Nat.card F - 1
Tactic: rw [← Nat.card_eq_fintype_card] at hodd h
Cleared hypotheses: hodd, h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
have h₁ : HPow.hPow (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n) (Nat.card F / 2) = 1
Tactic: rw [← Nat.card_eq_fintype_card] at hodd h
Cleared hypotheses: hodd, h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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)
have h₁ : g ^ (n * (Nat.card F / 2)) = 1
Tactic: rw [← pow_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2)
have rw : orderOf g ∣ n * (Nat.card F / 2)
Tactic: rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
have key : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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)
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
have this : 0 < Nat.card F / 2
Tactic: have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare.{u_3} (α := Fˣ) ((fun (x : ℕ) ↦ g ^ x) n)
have 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))
Tactic: obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
Cleared hypotheses: n, h, key
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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))
have mpr : (fun (x : ℕ) ↦ g ^ x) (2 * m) = g ^ m * g ^ m
Tactic: refine ⟨g ^ m, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ g ^ (2 * m) = g ^ m * g ^ m
have mpr : g ^ (m * 2) = g ^ m * g ^ m
Tactic: rw [mul_comm, pow_mul, pow_two]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ g ^ (2 * m) = g ^ m * g ^ m
have mpr₁ : HPow.hPow (β := ℕ) (g ^ m) 2 = g ^ m * g ^ m
Tactic: rw [mul_comm, pow_mul, pow_two]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ g ^ (2 * m) = g ^ m * g ^ m
have mpr₂ : g ^ m * g ^ m = g ^ m * g ^ m
Tactic: rw [mul_comm, pow_mul, pow_two]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have obtain : ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x),
  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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have 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
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have _ : IsSquare (α := Fˣ) (Units.mk0 a ha : Fˣ) ↔ IsSquare a
Tactic: apply
    (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have simp : (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) ↔ ∃ (r : F), a = r * r
Tactic: simp only [IsSquare, Units.ext_iff, Units.val_mk0, Units.val_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) ↔ ∃ (r : F), a = r * r
have mp : (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) → ∃ (r : F), a = r * r
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (∃ (r : Fˣ), a = (↑r : F) * (↑r : F)) ↔ ∃ (r : F), a = r * r
have mpr : (∃ (r : F), a = r * r) → ∃ (r : Fˣ), a = (↑r : F) * (↑r : F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ (r : Fˣ), y * y = (↑r : F) * (↑r : F)
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := by rintro rfl; simp at ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
have mpr : y * y = (↑(Units.mk0 y hy) : F) * (↑(Units.mk0 y hy) : F)
Tactic: refine ⟨Units.mk0 y hy, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
have h : inst_5 = this
Tactic: convert!
    GaloisField.finrank p (n := Module.finrank (ZMod p) k * n) <|
      mul_ne_zero Module.finrank_pos.ne' <| NeZero.ne n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ Nat.card (Extension k p n) = Nat.card k ^ n
have rw : p ^ Module.finrank (ZMod p) (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ Nat.card (Extension k p n) = Nat.card k ^ n
have rw₁ : p ^ Module.finrank (ZMod p) (Extension k p n) = (p ^ Module.finrank (ZMod p) k) ^ n
Tactic: rw [← pow_finrank_eq_natCard p, ← pow_finrank_eq_natCard p, finrank_zmod_extension, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ Nat.card (Extension k p n) = Nat.card k ^ n
have rw₂ : p ^ (Module.finrank (ZMod p) k * n) = (p ^ Module.finrank (ZMod p) k) ^ n
Tactic: rw [← pow_finrank_eq_natCard p, ← pow_finrank_eq_natCard p, finrank_zmod_extension, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ Nat.card (Extension k p n) = Nat.card k ^ n
have rw₃ : (p ^ Module.finrank (ZMod p) k) ^ n = (p ^ Module.finrank (ZMod p) k) ^ n
Tactic: rw [← pow_finrank_eq_natCard p, ← pow_finrank_eq_natCard p, finrank_zmod_extension, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
have refine : Eq (α := ℕ) ((fun (x : ℕ) ↦ Nat.card k ^ x) (Module.finrank k (Extension k p n))) ((fun (x : ℕ) ↦ Nat.card k ^ x) n)
Tactic: refine Nat.pow_right_injective (Finite.one_lt_card : 2 ≤ Nat.card k) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Extension (goal)
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
⊢ IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
have have : ∀ (this : Fintype (Extension k p n)),
  IsSplittingField k (Extension k p n) (HPow.hPow (α := k[X]) X (Nat.card k ^ n) - X)
Tactic: have := Fintype.ofFinite (Extension k p n)