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

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

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

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

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

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

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

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