K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ a, ¬IsSquare a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
⊢ ∃ a, ¬IsSquare a
let sq : F → F := fun x => x ^ 2
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Injective sq
⊢ ∃ a, ¬IsSquare a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ a, ¬IsSquare a
have h : ¬Function.Injective sq := by
  simp only [Function.Injective, not_forall, exists_prop]
  refine' ⟨-1, 1, _, Ring.neg_one_ne_one_of_char_ne_two hF⟩
  simp only [one_pow, neg_one_sq]
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬IsSquare a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Injective sq
⊢ ∃ a, ¬IsSquare a
rw [Finite.injective_iff_surjective] at h
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬∃ r, r ^ 2 = a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬IsSquare a
simp_rw [IsSquare, ← pow_two, @eq_comm _ _ (_ ^ 2)]
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬∀ (b : F), ∃ a, sq a = b
⊢ ∃ a, ¬∃ r, r ^ 2 = a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬Function.Surjective sq
⊢ ∃ a, ¬∃ r, r ^ 2 = a
unfold Function.Surjective at h
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ∃ b, ∀ (a : F), (fun x => x ^ 2) a ≠ b
⊢ ∃ a, ∀ (r : F), r ^ 2 ≠ a
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ¬∀ (b : F), ∃ a, sq a = b
⊢ ∃ a, ¬∃ r, r ^ 2 = a
push_neg  at h⊢
no goals
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
h : ∃ b, ∀ (a : F), (fun x => x ^ 2) a ≠ b
⊢ ∃ a, ∀ (r : F), r ^ 2 ≠ a
exact h
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ x x_1, x ^ 2 = x_1 ^ 2 ∧ ¬x = x_1
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ¬Function.Injective sq
simp only [Function.Injective, not_forall, exists_prop]
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ (-1) ^ 2 = 1 ^ 2
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ ∃ x x_1, x ^ 2 = x_1 ^ 2 ∧ ¬x = x_1
refine' ⟨-1, 1, _, Ring.neg_one_ne_one_of_char_ne_two hF⟩
no goals
K : Type ?u.1094008
R : Type ?u.1094011
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
sq : F → F := fun x => x ^ 2
⊢ (-1) ^ 2 = 1 ^ 2
simp only [one_pow, neg_one_sq]