Theorem: Imo1998P2.judge_pairs_card_lower_bound (Compfiles/Imo1998P2.lean)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card
Tactic:
let x := (Finset.univ.filter fun j => r c j).card
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card
Tactic:
let y := (Finset.univ.filter fun j => ¬r c j).card
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card
Tactic:
have h : (Finset.univ.filter fun p : JudgePair J => p.Agree r c).card = x * x + y * y := by
  simp [x, y, ← Finset.filter_product_card]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card
Tactic:
rw [h]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y
Tactic:
apply Int.le_of_ofNat_le_ofNat
State after:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑(2 * z * z + 2 * z + 1) ≤ ↑(x * x + y * y)

State before:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑(2 * z * z + 2 * z + 1) ≤ ↑(x * x + y * y)
Tactic:
simp only [Int.ofNat_add, Int.ofNat_mul]
State after:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑2 * ↑z * ↑z + ↑2 * ↑z + ↑1 ≤ ↑x * ↑x + ↑y * ↑y

State before:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑2 * ↑z * ↑z + ↑2 * ↑z + ↑1 ≤ ↑x * ↑x + ↑y * ↑y
Tactic:
apply norm_bound_of_odd_sum
State after:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑x + ↑y = 2 * ↑z + 1

State before:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ ↑x + ↑y = 2 * ↑z + 1
Tactic:
suffices x + y = 2 * z + 1 by simp [← Int.ofNat_add, this]
State after:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ x + y = 2 * z + 1

State before:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ x + y = 2 * z + 1
Tactic:
rw [Finset.filter_card_add_filter_neg_card_eq_card, ← hJ]
State after:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ Finset.univ.card = Fintype.card J

State before:
case a.h
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
⊢ Finset.univ.card = Fintype.card J
Tactic:
rfl
State after:
no goals

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
⊢ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
Tactic:
simp [x, y, ← Finset.filter_product_card]
State after:
no goals

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝ : Fintype J
z : ℕ
hJ : Fintype.card J = 2 * z + 1
c : C
x : ℕ := (Finset.filter (fun j => r c j) Finset.univ).card
y : ℕ := (Finset.filter (fun j => ¬r c j) Finset.univ).card
h : (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card = x * x + y * y
this : x + y = 2 * z + 1
⊢ ↑x + ↑y = 2 * ↑z + 1
Tactic:
simp [← Int.ofNat_add, this]
State after:
no goals