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

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 _)
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)

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]
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

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)
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

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
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

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
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

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']
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

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
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

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'
State after:
no goals

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
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

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
State after:
no goals