-- Mathlib/FieldTheory/Finite/Basic.lean
theorem unit_isSquare_iff (hF : ringChar F ≠ 2) (a : Fˣ) :
    IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Proof state:
case intro.intro.mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x => g ^ x) n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x => g ^ x) n)

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

Result:
case intro.intro.mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x => g ^ x) n ^ (Nat.card F / 2) = 1
⊢ IsSquare ((fun x => g ^ x) n)

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g

Tactic:
apply hg

Result:
no goals

Proof state:
case intro.intro.mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (fun x => g ^ x) (2 * m) ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ IsSquare ((fun x => g ^ x) (2 * m))

Tactic:
refine ⟨g ^ m, ?_⟩

Result:
case intro.intro.mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (fun x => g ^ x) (2 * m) ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ (fun x => g ^ x) (2 * m) = g ^ m * g ^ m

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Submonoid.powers g

Tactic:
rw [mem_powers_iff_mem_zpowers]

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ a ∈ Subgroup.zpowers g

Proof state:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hn : (fun x => g ^ x) n = a
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Tactic:
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)

Result:
case intro.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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

Proof state:
case intro.intro.mp.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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

Tactic:
push_cast

Result:
case intro.intro.mp.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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

Proof state:
case intro.intro.mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (fun x => g ^ x) (2 * m) ^ (Nat.card F / 2) = 1
key : 2 * (Nat.card F / 2) ∣ 2 * m * (Nat.card F / 2)
⊢ (fun x => g ^ x) (2 * m) = g ^ m * g ^ m

Tactic:
dsimp

Result:
case intro.intro.mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
this : 0 < Nat.card F / 2
m : ℕ
h : (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

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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)

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

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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)

Proof state:
case intro.intro.mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
⊢ (fun x => g ^ x) n ^ (Fintype.card F / 2) = 1 → IsSquare ((fun x => g ^ x) n)

Tactic:
intro h

Result:
case intro.intro.mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x => g ^ x) n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x => g ^ x) n)

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

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

Result:
case intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Proof state:
case intro.intro.mp
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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:
rintro ⟨y, rfl⟩

Result:
case intro.intro.mp.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
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