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

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ =
    Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))
Tactic:
ext p
State after:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ ↔
    p ∈ Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))

State before:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ p ∈ Finset.filter (fun p => JudgePair.Agree r p c ∧ p.Distinct) Finset.univ ↔
    p ∈ Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))
Tactic:
simp only [A, Finset.mem_univ, Finset.mem_filter, Finset.mem_image, true_and_iff, exists_prop]
State after:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct ↔
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p

State before:
case a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct ↔
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p
Tactic:
constructor
State after:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct →
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p

case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ (∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p) →
    JudgePair.Agree r p c ∧ p.Distinct

State before:
case a.mp
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
⊢ JudgePair.Agree r p c ∧ p.Distinct →
    ∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case a.mp.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h₁ : JudgePair.Agree r p c
h₂ : p.Distinct
⊢ ∃ a,
    ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧ (AgreedTriple.judgePair a).Distinct) ∧
        AgreedTriple.contestant a = c) ∧
      a.2 = p

State before:
case a.mp.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h₁ : JudgePair.Agree r p c
h₂ : p.Distinct
⊢ ∃ a,
    ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧ (AgreedTriple.judgePair a).Distinct) ∧
        AgreedTriple.contestant a = c) ∧
      a.2 = p
Tactic:
refine ⟨(c, p), ?_⟩
State after:
case a.mp.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h₁ : JudgePair.Agree r p c
h₂ : p.Distinct
⊢ ((JudgePair.Agree r (AgreedTriple.judgePair (c, p)) (AgreedTriple.contestant (c, p)) ∧
        (AgreedTriple.judgePair (c, p)).Distinct) ∧
      AgreedTriple.contestant (c, p) = c) ∧
    (c, p).2 = p

State before:
case a.mp.intro
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h₁ : JudgePair.Agree r p c
h₂ : p.Distinct
⊢ ((JudgePair.Agree r (AgreedTriple.judgePair (c, p)) (AgreedTriple.contestant (c, p)) ∧
        (AgreedTriple.judgePair (c, p)).Distinct) ∧
      AgreedTriple.contestant (c, p) = c) ∧
    (c, p).2 = p
Tactic:
tauto
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
c : C
p : JudgePair J
⊢ (∃ a,
      ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧
            (AgreedTriple.judgePair a).Distinct) ∧
          AgreedTriple.contestant a = c) ∧
        a.2 = p) →
    JudgePair.Agree r p c ∧ p.Distinct
Tactic:
intro h
State after:
case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h :
  ∃ a,
    ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧ (AgreedTriple.judgePair a).Distinct) ∧
        AgreedTriple.contestant a = c) ∧
      a.2 = p
⊢ JudgePair.Agree r p c ∧ p.Distinct

State before:
case a.mpr
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
p : JudgePair J
h :
  ∃ a,
    ((JudgePair.Agree r (AgreedTriple.judgePair a) (AgreedTriple.contestant a) ∧ (AgreedTriple.judgePair a).Distinct) ∧
        AgreedTriple.contestant a = c) ∧
      a.2 = p
⊢ JudgePair.Agree r p c ∧ p.Distinct
Tactic:
aesop
State after:
no goals