internlm/Lean-Github huggingface dataset:
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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
Proof 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)
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: Imo1998P2.judge_pairs_card_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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]
Proof 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₂
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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]
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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]
Proof 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
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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']
Proof 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)
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.distinct_judge_pairs_card_lower_bound
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.A_card_lower_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
z : ℕ
hJ : Fintype.card J = 2 * z + 1
⊢ 2 * z * z * Fintype.card C ≤ (A r).card
Tactic:
have h : ∀ a, a ∈ A r → Prod.fst a ∈ @Finset.univ C _ := by intros; apply Finset.mem_univ
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
z : ℕ
hJ : Fintype.card J = 2 * z + 1
h : ∀ a ∈ A r, a.1 ∈ Finset.univ
⊢ 2 * z * z * Fintype.card C ≤ (A r).card
Theorem: Imo1998P2.A_card_lower_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
z : ℕ
hJ : Fintype.card J = 2 * z + 1
h : ∀ a ∈ A r, a.1 ∈ Finset.univ
⊢ 2 * z * z * Fintype.card C ≤ (A r).card
Tactic:
apply Finset.mul_card_image_le_card_of_maps_to h
Proof state after:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
z : ℕ
hJ : Fintype.card J = 2 * z + 1
h : ∀ a ∈ A r, a.1 ∈ Finset.univ
⊢ ∀ a ∈ Finset.univ, 2 * z * z ≤ (Finset.filter (fun x => x.1 = a) (A r)).card