Theorem: card_square (ExponentialRamsey/Prereq/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean)

State before:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Fintype.card F / 2 + 1
Tactic:
rw [← (card_non_zero_square_non_square hF).1]
State after:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) + 1

State before:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) + 1
Tactic:
simp only [and_comm, ← filter_filter, filter_ne']
State after:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (erase (filter (fun a => IsSquare a) univ) 0) + 1

State before:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter IsSquare univ) = Finset.card (erase (filter (fun a => IsSquare a) univ) 0) + 1
Tactic:
rw [card_erase_add_one]
State after:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ 0 ∈ filter (fun a => IsSquare a) univ

State before:
F✝ : Type u_1
inst✝⁴ : Fintype F✝
inst✝³ : Field F✝
F : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ 0 ∈ filter (fun a => IsSquare a) univ
Tactic:
simp
State after:
no goals