-- Mathlib/FieldTheory/Finite/Basic.lean
theorem isSquare_iff (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
    IsSquare a ↔ a ^ (Fintype.card F / 2) = 1

Proof state:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r

Tactic:
rintro ⟨y, rfl⟩

Result:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ 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))

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ IsSquare (Units.mk0 a ha) ↔ IsSquare a

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

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r

Proof state:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r

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

Result:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)

Proof state:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r

Tactic:
have hy : y ≠ 0 := by rintro rfl; simp at ha

Result:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ r, y * y = ↑r * ↑r

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False

Tactic:
simp at ha

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) ↔ ∃ r, a = r * r

Tactic:
constructor

Result:
case mp
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r

case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = r * r) → ∃ r, a = ↑r * ↑r

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
⊢ y ≠ 0

Tactic:
rintro rfl

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
ha : 0 * 0 ≠ 0
⊢ False

Proof state:
case mp
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (∃ r, a = ↑r * ↑r) → ∃ r, a = r * r

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r

Proof state:
case mpr.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
y : F
ha : y * y ≠ 0
hy : y ≠ 0
⊢ y * y = ↑(Units.mk0 y hy) * ↑(Units.mk0 y hy)

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
y : Fˣ
hy : a = ↑y * ↑y
⊢ ∃ r, a = r * r

Tactic:
exact ⟨y, hy⟩

Result:
no goals

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

Tactic:
simp [Units.ext_iff]

Result:
no goals