Theorem: Imo1998P2.distinct_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 ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
let s := Finset.univ.filter fun p : JudgePair J => p.Agree r c
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) 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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
let t := Finset.univ.filter fun p : JudgePair J => p.Distinct
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) 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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
have hs : 2 * z * z + 2 * z + 1 ≤ s.card := judge_pairs_card_lower_bound r hJ c
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) 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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
have hst' : (s \ t).card = 2 * z + 1 := by rw [hst, Finset.diag_card, ← hJ]; rfl
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) 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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
rw [Finset.filter_and, ← Finset.sdiff_sdiff_self_left s t, Finset.card_sdiff]
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ s.card - (s \ t).card

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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ s \ t ⊆ s

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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
⊢ s \ t = Finset.univ.diag
Tactic:
ext p
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
⊢ p ∈ s \ t ↔ p ∈ Finset.univ.diag

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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
⊢ p ∈ s \ t ↔ p ∈ Finset.univ.diag
Tactic:
constructor <;> intros hp
State after:
case a.mp
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ s \ t
⊢ p ∈ Finset.univ.diag

case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p ∈ s \ t

State before:
case a.mp
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ s \ t
⊢ p ∈ Finset.univ.diag
Tactic:
unfold_let s t at hp
State after:
case a.mp
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ \ Finset.filter (fun p => p.Distinct) Finset.univ
⊢ p ∈ Finset.univ.diag

State before:
case a.mp
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ \ Finset.filter (fun p => p.Distinct) Finset.univ
⊢ p ∈ Finset.univ.diag
Tactic:
aesop
State after:
no goals

State before:
case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p ∈ s \ t
Tactic:
unfold_let s t
State after:
case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ \ Finset.filter (fun p => p.Distinct) Finset.univ

State before:
case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ \ Finset.filter (fun p => p.Distinct) Finset.univ
Tactic:
suffices p.judge₁ = p.judge₂ by simp [this]
State after:
case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p.judge₁ = p.judge₂

State before:
case a.mpr
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
⊢ p.judge₁ = p.judge₂
Tactic:
aesop
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
p : JudgePair J
hp : p ∈ Finset.univ.diag
this : p.judge₁ = p.judge₂
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ \ Finset.filter (fun p => p.Distinct) Finset.univ
Tactic:
simp [this]
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
⊢ (s \ t).card = 2 * z + 1
Tactic:
rw [hst, Finset.diag_card, ← hJ]
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
⊢ Finset.univ.card = Fintype.card J

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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
⊢ 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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ s.card - (s \ t).card
Tactic:
rw [hst']
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ s.card - (2 * z + 1)

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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ 2 * z * z ≤ s.card - (2 * z + 1)
Tactic:
exact Nat.le_sub_of_add_le hs
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
s : Finset (JudgePair J) := Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ
t : Finset (JudgePair J) := Finset.filter (fun p => p.Distinct) Finset.univ
hs : 2 * z * z + 2 * z + 1 ≤ s.card
hst : s \ t = Finset.univ.diag
hst' : (s \ t).card = 2 * z + 1
⊢ s \ t ⊆ s
Tactic:
apply Finset.sdiff_subset
State after:
no goals