internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : Even (Finset.card (filter (fun v => Odd (degree G v)) univ))
⊢ False
Tactic:
rw [h, Nat.even_iff_not_odd] at h'
Proof state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : ¬Odd (Fintype.card V)
⊢ False
Theorem: SimpleGraph.exists_even_degree
Proof state before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : ¬Odd (Fintype.card V)
⊢ False
Tactic:
exact h' hV
Proof state after:
no goals
Theorem: Nat.choose_le_two_pow
Proof state before:
n k : ℕ
⊢ choose n k ≤ 2 ^ n
Tactic:
cases' le_or_lt k n with h h
Proof state after:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ 2 ^ n

case inr
n k : ℕ
h : n < k
⊢ choose n k ≤ 2 ^ n
Theorem: Nat.choose_le_two_pow
Proof state before:
case inr
n k : ℕ
h : n < k
⊢ choose n k ≤ 2 ^ n
Tactic:
rw [choose_eq_zero_of_lt h]
Proof state after:
case inr
n k : ℕ
h : n < k
⊢ 0 ≤ 2 ^ n
Theorem: Nat.choose_le_two_pow
Proof state before:
case inr
n k : ℕ
h : n < k
⊢ 0 ≤ 2 ^ n
Tactic:
exact zero_le'
Proof state after:
no goals
Theorem: Nat.choose_le_two_pow
Proof state before:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ 2 ^ n
Tactic:
rw [← sum_range_choose n]
Proof state after:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ Finset.sum (range (n + 1)) fun m => choose n m
Theorem: Nat.choose_le_two_pow
Proof state before:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ Finset.sum (range (n + 1)) fun m => choose n m
Tactic:
refine' single_le_sum (fun _ _ => zero_le') _
Proof state after:
case inl
n k : ℕ
h : k ≤ n
⊢ k ∈ range (n + 1)
Theorem: Nat.choose_le_two_pow
Proof state before:
case inl
n k : ℕ
h : k ≤ n
⊢ k ∈ range (n + 1)
Tactic:
rwa [mem_range_succ_iff]
Proof state after:
no goals
Theorem: symmetric_isSquare
Proof state before:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : Fintype.card F % 4 ≠ 3
x✝¹ x✝ : F
h : (fun x y => IsSquare (x - y)) x✝¹ x✝
⊢ (fun x y => IsSquare (x - y)) x✝ x✝¹
Tactic:
simpa using h.mul (FiniteField.isSquare_neg_one_iff.2 hF)
Proof state after:
no goals
Theorem: card_non_zero_square_non_square
Proof 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]
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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]
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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]
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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 _
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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'
Proof 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}
Theorem: card_non_zero_square_non_square
Proof 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 _
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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]
Proof state after:
no goals
Theorem: card_non_zero_square_non_square
Proof 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']
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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]
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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 _
Proof state after:
no goals
Theorem: card_non_zero_square_non_square
Proof 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]
Proof state after:
no goals
Theorem: card_non_zero_square_non_square
Proof 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]
Proof 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
Theorem: card_non_zero_square_non_square
Proof 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 })
Proof state after:
no goals
Theorem: card_non_zero_square_non_square
Proof 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
Proof state after:
no goals
Theorem: card_square
Proof 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]
Proof 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
Theorem: card_square
Proof 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']
Proof 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
Theorem: card_square
Proof 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]
Proof 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
Theorem: card_square
Proof 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
Proof state after:
no goals
Theorem: MulLECancellable.hMul
Proof state before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
⊢ MulLECancellable (a * b)
Tactic:
intro x y h
Proof state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * b * x ≤ a * b * y
⊢ x ≤ y
Theorem: MulLECancellable.hMul
Proof state before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * b * x ≤ a * b * y
⊢ x ≤ y
Tactic:
rw [mul_assoc, mul_assoc] at h
Proof state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * (b * x) ≤ a * (b * y)
⊢ x ≤ y
Theorem: MulLECancellable.hMul
Proof state before:
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * (b * x) ≤ a * (b * y)
⊢ x ≤ y
Tactic:
exact hb (ha h)
Proof state after:
no goals
Theorem: MulLECancellable.of_hMul_left
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
⊢ MulLECancellable b
Tactic:
intro x y h
Proof state after:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ x ≤ y
Theorem: MulLECancellable.of_hMul_left
Proof state before:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ x ≤ y
Tactic:
apply hab
Proof state after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * b * x ≤ a * b * y
Theorem: MulLECancellable.of_hMul_left
Proof state before:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * b * x ≤ a * b * y
Tactic:
rw [mul_assoc, mul_assoc]
Proof state after:
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * (b * x) ≤ a * (b * y)