Theorem: Imo1998P2.A_fibre_over_judgePair (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 = Finset.image AgreedTriple.contestant (Finset.filter (fun a => a.judgePair = p) (A r))
Tactic:
dsimp only [A, agreedContestants]
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.filter (fun c => JudgePair.Agree r p c) Finset.univ =
    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))

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.filter (fun c => JudgePair.Agree r p c) Finset.univ =
    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:
ext c
State after:
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))

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

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

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⟩, ?_⟩
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

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

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

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, _⟩⟩⟩⟩
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

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

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