internlm/Lean-Github huggingface dataset:
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
c : C
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ ↔
    c ∈
      Finset.image AgreedTriple.contestant
        (Finset.filter (fun a => a.judgePair = p)
          (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))
Tactic:
constructor <;> intro h
Proof state after:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ c ∈
    Finset.image AgreedTriple.contestant
      (Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))

case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h :
  c ∈
    Finset.image AgreedTriple.contestant
      (Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ c ∈
    Finset.image AgreedTriple.contestant
      (Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))
Tactic:
rw [Finset.mem_image]
Proof state after:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ ∃
    a ∈
      Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ),
    a.contestant = c
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ ∃
    a ∈
      Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ),
    a.contestant = c
Tactic:
refine ⟨⟨c, p⟩, ?_⟩
Proof state after:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ (c, p) ∈
      Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ) ∧
    AgreedTriple.contestant (c, p) = c
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h : c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
⊢ (c, p) ∈
      Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ) ∧
    AgreedTriple.contestant (c, p) = c
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h :
  c ∈
    Finset.image AgreedTriple.contestant
      (Finset.filter (fun a => a.judgePair = p)
        (Finset.filter (fun a => JudgePair.Agree r a.judgePair a.contestant ∧ a.judgePair.Distinct) Finset.univ))
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Tactic:
simp only [Finset.mem_filter, Finset.mem_image, Prod.exists] at h
Proof state after:
case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h :
  ∃ a a_1 b,
    (((a, a_1, b) ∈ Finset.univ ∧
          JudgePair.Agree r (AgreedTriple.judgePair (a, a_1, b)) (AgreedTriple.contestant (a, a_1, b)) ∧
            (AgreedTriple.judgePair (a, a_1, b)).Distinct) ∧
        AgreedTriple.judgePair (a, a_1, b) = p) ∧
      AgreedTriple.contestant (a, a_1, b) = c
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c : C
h :
  ∃ a a_1 b,
    (((a, a_1, b) ∈ Finset.univ ∧
          JudgePair.Agree r (AgreedTriple.judgePair (a, a_1, b)) (AgreedTriple.contestant (a, a_1, b)) ∧
            (AgreedTriple.judgePair (a, a_1, b)).Distinct) ∧
        AgreedTriple.judgePair (a, a_1, b) = p) ∧
      AgreedTriple.contestant (a, a_1, b) = c
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Tactic:
rcases h with ⟨_, ⟨_, ⟨_, ⟨h, _⟩⟩⟩⟩
Proof state after:
case a.mpr.intro.intro.intro.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c w✝² : C
w✝¹ w✝ : J
h :
  ((w✝², w✝¹, w✝) ∈ Finset.univ ∧
      JudgePair.Agree r (AgreedTriple.judgePair (w✝², w✝¹, w✝)) (AgreedTriple.contestant (w✝², w✝¹, w✝)) ∧
        (AgreedTriple.judgePair (w✝², w✝¹, w✝)).Distinct) ∧
    AgreedTriple.judgePair (w✝², w✝¹, w✝) = p
right✝ : AgreedTriple.contestant (w✝², w✝¹, w✝) = c
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mpr.intro.intro.intro.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h✝ : p.Distinct
c w✝² : C
w✝¹ w✝ : J
h :
  ((w✝², w✝¹, w✝) ∈ Finset.univ ∧
      JudgePair.Agree r (AgreedTriple.judgePair (w✝², w✝¹, w✝)) (AgreedTriple.contestant (w✝², w✝¹, w✝)) ∧
        (AgreedTriple.judgePair (w✝², w✝¹, w✝)).Distinct) ∧
    AgreedTriple.judgePair (w✝², w✝¹, w✝) = p
right✝ : AgreedTriple.contestant (w✝², w✝¹, w✝) = c
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Tactic:
cases h
Proof state after:
case a.mpr.intro.intro.intro.intro.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
c w✝² : C
w✝¹ w✝ : J
right✝¹ : AgreedTriple.contestant (w✝², w✝¹, w✝) = c
left✝ :
  (w✝², w✝¹, w✝) ∈ Finset.univ ∧
    JudgePair.Agree r (AgreedTriple.judgePair (w✝², w✝¹, w✝)) (AgreedTriple.contestant (w✝², w✝¹, w✝)) ∧
      (AgreedTriple.judgePair (w✝², w✝¹, w✝)).Distinct
right✝ : AgreedTriple.judgePair (w✝², w✝¹, w✝) = p
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof state before:
case a.mpr.intro.intro.intro.intro.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
c w✝² : C
w✝¹ w✝ : J
right✝¹ : AgreedTriple.contestant (w✝², w✝¹, w✝) = c
left✝ :
  (w✝², w✝¹, w✝) ∈ Finset.univ ∧
    JudgePair.Agree r (AgreedTriple.judgePair (w✝², w✝¹, w✝)) (AgreedTriple.contestant (w✝², w✝¹, w✝)) ∧
      (AgreedTriple.judgePair (w✝², w✝¹, w✝)).Distinct
right✝ : AgreedTriple.judgePair (w✝², w✝¹, w✝) = p
⊢ c ∈ Finset.filter (fun c => JudgePair.Agree r p c) Finset.univ
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ (agreedContestants r p).card = (Finset.filter (fun a => a.judgePair = p) (A r)).card
Tactic:
rw [A_fibre_over_judgePair r h]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ (Finset.image AgreedTriple.contestant (Finset.filter (fun a => a.judgePair = p) (A r))).card =
    (Finset.filter (fun a => a.judgePair = p) (A r)).card
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ (Finset.image AgreedTriple.contestant (Finset.filter (fun a => a.judgePair = p) (A r))).card =
    (Finset.filter (fun a => a.judgePair = p) (A r)).card
Tactic:
apply Finset.card_image_of_injOn
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ Set.InjOn AgreedTriple.contestant ↑(Finset.filter (fun a => a.judgePair = p) (A r))
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ Set.InjOn AgreedTriple.contestant ↑(Finset.filter (fun a => a.judgePair = p) (A r))
Tactic:
unfold Set.InjOn
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ ∀ ⦃x₁ : AgreedTriple C J⦄,
    x₁ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) →
      ∀ ⦃x₂ : AgreedTriple C J⦄,
        x₂ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) → x₁.contestant = x₂.contestant → x₁ = x₂
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
⊢ ∀ ⦃x₁ : AgreedTriple C J⦄,
    x₁ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) →
      ∀ ⦃x₂ : AgreedTriple C J⦄,
        x₂ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r)) → x₁.contestant = x₂.contestant → x₁ = x₂
Tactic:
intros
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝ = x₂✝
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝ = x₂✝
Tactic:
ext
Proof state after:
case H.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.1 = x₂✝.1

case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.1 = x₂✝.2.1

case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.2 = x₂✝.2.2
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
case H.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.1 = x₂✝.1

case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.1 = x₂✝.2.1

case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.2 = x₂✝.2.2
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_judgePair_card
Proof state before:
case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
p : JudgePair J
h : p.Distinct
x₁✝ : AgreedTriple C J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
x₂✝ : AgreedTriple C J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.judgePair = p) (A r))
a✝ : x₁✝.contestant = x₂✝.contestant
⊢ x₁✝.2.2 = x₂✝.2.2
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * (Fintype.card J * Fintype.card J - Fintype.card J)
Tactic:
change _ ≤ k * (Finset.card _ * Finset.card _ - Finset.card _)
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * (Finset.univ.card * Finset.univ.card - Finset.univ.card)
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * (Finset.univ.card * Finset.univ.card - Finset.univ.card)
Tactic:
rw [← Finset.offDiag_card]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * Finset.univ.offDiag.card
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ (A r).card ≤ k * Finset.univ.offDiag.card
Tactic:
apply Finset.card_le_mul_card_image_of_maps_to (A_maps_to_offDiag_judgePair r)
Proof state after:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ ∀ a ∈ Finset.univ.offDiag, (Finset.filter (fun x => x.judgePair = a) (A r)).card ≤ k
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
⊢ ∀ a ∈ Finset.univ.offDiag, (Finset.filter (fun x => x.judgePair = a) (A r)).card ≤ k
Tactic:
intro p hp
Proof state after:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
⊢ (Finset.filter (fun x => x.judgePair = p) (A r)).card ≤ k
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
⊢ (Finset.filter (fun x => x.judgePair = p) (A r)).card ≤ k
Tactic:
have hp' : p.Distinct := by simp [Finset.mem_offDiag] at hp; exact hp
Proof state after:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ (Finset.filter (fun x => x.judgePair = p) (A r)).card ≤ k
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ (Finset.filter (fun x => x.judgePair = p) (A r)).card ≤ k
Tactic:
rw [← A_fibre_over_judgePair_card r hp']
Proof state after:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ (agreedContestants r p).card ≤ k
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
case hn
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ (agreedContestants r p).card ≤ k
Tactic:
apply hk
Proof state after:
case hn.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ p.Distinct
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
case hn.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
hp' : p.Distinct
⊢ p.Distinct
Tactic:
exact hp'
Proof state after:
no goals
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : p ∈ Finset.univ.offDiag
⊢ p.Distinct
Tactic:
simp [Finset.mem_offDiag] at hp
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : ¬p.1 = p.2
⊢ p.Distinct
Theorem: Imo1998P2.A_card_upper_bound
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
k : ℕ
hk : ∀ (p : JudgePair J), p.Distinct → (agreedContestants r p).card ≤ k
p : JudgePair J
hp : ¬p.1 = p.2
⊢ p.Distinct
Tactic:
exact hp
Proof state after:
no goals
Theorem: Imo1998P2.add_sq_add_sq_sub
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
α : Type u_3
inst✝ : Ring α
x y : α
⊢ (x + y) * (x + y) + (x - y) * (x - y) = 2 * x * x + 2 * y * y
Tactic:
noncomm_ring
Proof state after:
no goals
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y
Tactic:
suffices 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y by
  rw [← mul_le_mul_left (zero_lt_two' ℤ)]; ring_nf at this ⊢; exact this
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Tactic:
have h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1 := by rw [h]; ring
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
Tactic:
rw [← add_sq_add_sq_sub, h', add_le_add_iff_left]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 1 ≤ (x - y) * (x - y)
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 1 ≤ (x - y) * (x - y)
Tactic:
suffices 0 < (x - y) * (x - y) by apply Int.add_one_le_of_lt this
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 0 < (x - y) * (x - y)
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ 0 < (x - y) * (x - y)
Tactic:
rw [mul_self_pos, sub_ne_zero]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ x ≠ y
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
⊢ x ≠ y
Tactic:
apply Int.ne_of_odd_add ⟨z, h⟩
Proof state after:
no goals
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * z * z + 2 * z + 1 ≤ x * x + y * y
Tactic:
rw [← mul_le_mul_left (zero_lt_two' ℤ)]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * (2 * z * z + 2 * z + 1) ≤ 2 * (x * x + y * y)
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 4 * z * z + 4 * z + 1 + 1 ≤ 2 * x * x + 2 * y * y
⊢ 2 * (2 * z * z + 2 * z + 1) ≤ 2 * (x * x + y * y)
Tactic:
ring_nf at this ⊢
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
⊢ 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
this : 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
⊢ 2 + z * 4 + z ^ 2 * 4 ≤ x ^ 2 * 2 + y ^ 2 * 2
Tactic:
exact this
Proof state after:
no goals
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (x + y) * (x + y) = 4 * z * z + 4 * z + 1
Tactic:
rw [h]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (2 * z + 1) * (2 * z + 1) = 4 * z * z + 4 * z + 1
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
⊢ (2 * z + 1) * (2 * z + 1) = 4 * z * z + 4 * z + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1998P2.norm_bound_of_odd_sum
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
x y z : ℤ
h : x + y = 2 * z + 1
h' : (x + y) * (x + y) = 4 * z * z + 4 * z + 1
this : 0 < (x - y) * (x - y)
⊢ 1 ≤ (x - y) * (x - y)
Tactic:
apply Int.add_one_le_of_lt this
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
⊢ 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
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
⊢ 2 * z * z + 2 * z + 1 ≤ (Finset.filter (fun p => JudgePair.Agree r p c) Finset.univ).card