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

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

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

State before:
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
Tactic:
intro c _
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
c : C
a✝ : c ∈ Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun x => x.1 = c) (A r)).card

State before:
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
c : C
a✝ : c ∈ Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun x => x.1 = c) (A r)).card
Tactic:
rw [← A_fibre_over_contestant_card]
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
c : C
a✝ : c ∈ Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card

State before:
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
c : C
a✝ : c ∈ Finset.univ
⊢ 2 * z * z ≤ (Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ).card
Tactic:
apply distinct_judge_pairs_card_lower_bound r hJ
State after:
no goals

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
⊢ ∀ a ∈ A r, a.1 ∈ Finset.univ
Tactic:
intros
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
a✝¹ : AgreedTriple C J
a✝ : a✝¹ ∈ A r
⊢ a✝¹.1 ∈ Finset.univ

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
a✝¹ : AgreedTriple C J
a✝ : a✝¹ ∈ A r
⊢ a✝¹.1 ∈ Finset.univ
Tactic:
apply Finset.mem_univ
State after:
no goals