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

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => ¬IsSquare x) univ) = Fintype.card F / 2
Tactic:
have : (univ.filter fun x : F => ¬IsSquare x) = univ.filter fun x : F => x ≠ 0 ∧ ¬IsSquare x :=
  by
  refine' filter_congr _
  simp (config := { contextual := true }) [not_imp_not]
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => ¬IsSquare x) univ) = Fintype.card F / 2

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

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2
Tactic:
have cf := quadraticChar_sum_zero hF
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun a => ↑(quadraticChar F) a) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun a => ↑(quadraticChar F) a) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2
Tactic:
simp only [quadraticChar_apply, quadraticCharFun] at cf
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun x => if x = 0 then 0 else if IsSquare x then 1 else -1) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf : (Finset.sum univ fun x => if x = 0 then 0 else if IsSquare x then 1 else -1) = 0
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2
Tactic:
rw [sum_ite, sum_const_zero, zero_add, sum_ite, sum_const, sum_const, nsmul_eq_mul, nsmul_eq_mul,
  mul_neg, mul_one, mul_one, add_neg_eq_zero, Nat.cast_inj, filter_filter, filter_filter] at cf
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2 ∧
    Finset.card (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) = Fintype.card F / 2
Tactic:
rw [← cf, and_self_iff]
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2
Tactic:
have :
  ((univ.filter fun x : F => x ≠ 0 ∧ IsSquare x) ∪ univ.filter fun x : F => x ≠ 0 ∧ ¬IsSquare x) ∪
      {0} =
    univ :=
  by
  simp only [← filter_or, ← and_or_left, em, and_true_iff, filter_ne']
  rw [union_comm, ← insert_eq, insert_erase]
  exact mem_univ _
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2
Tactic:
have h' := congr_arg Finset.card this
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0}) =
    Finset.card univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0}) =
    Finset.card univ
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2
Tactic:
rw [card_disjoint_union, card_disjoint_union, card_singleton, card_univ, ← cf, ← two_mul, ←
  bit0_eq_two_mul, ← bit1] at h'
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' : bit1 (Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ)) = Fintype.card F
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2

F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) +
      Finset.card {0} =
    Finset.card univ
⊢ Disjoint (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ)

F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0}) =
    Finset.card univ
⊢ Disjoint (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) {0}

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
Tactic:
refine' filter_congr _
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ∀ x ∈ univ, ¬IsSquare x ↔ x ≠ 0 ∧ ¬IsSquare x

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ ∀ x ∈ univ, ¬IsSquare x ↔ x ≠ 0 ∧ ¬IsSquare x
Tactic:
simp (config := { contextual := true }) [not_imp_not]
State after:
no goals

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
Tactic:
simp only [← filter_or, ← and_or_left, em, and_true_iff, filter_ne']
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ erase univ 0 ∪ {0} = univ

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ erase univ 0 ∪ {0} = univ
Tactic:
rw [union_comm, ← insert_eq, insert_erase]
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ 0 ∈ univ

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
⊢ 0 ∈ univ
Tactic:
exact mem_univ _
State after:
no goals

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' : bit1 (Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ)) = Fintype.card F
⊢ Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) = Fintype.card F / 2
Tactic:
rw [← h', Nat.bit1_div_two]
State after:
no goals

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) +
      Finset.card {0} =
    Finset.card univ
⊢ Disjoint (filter (fun x => x ≠ 0 ∧ IsSquare x) univ) (filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ)
Tactic:
rw [Finset.disjoint_left]
State after:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) +
      Finset.card {0} =
    Finset.card univ
⊢ ∀ ⦃a : F⦄, a ∈ filter (fun x => x ≠ 0 ∧ IsSquare x) univ → a ∉ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) +
      Finset.card {0} =
    Finset.card univ
⊢ ∀ ⦃a : F⦄, a ∈ filter (fun x => x ≠ 0 ∧ IsSquare x) univ → a ∉ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
Tactic:
simp (config := { contextual := true })
State after:
no goals

State before:
F : Type u_1
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
this✝ : filter (fun x => ¬IsSquare x) univ = filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ
cf :
  Finset.card (filter (fun a => ¬a = 0 ∧ IsSquare a) univ) = Finset.card (filter (fun a => ¬a = 0 ∧ ¬IsSquare a) univ)
this : filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0} = univ
h' :
  Finset.card (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ ∪ {0}) =
    Finset.card univ
⊢ Disjoint (filter (fun x => x ≠ 0 ∧ IsSquare x) univ ∪ filter (fun x => x ≠ 0 ∧ ¬IsSquare x) univ) {0}
Tactic:
simp
State after:
no goals