internlm/Lean-Github huggingface dataset:
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
⊢ x < 2 * m + 1
Tactic:
by_contra! H
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
⊢ False
Tactic:
obtain ⟨z, hz⟩ : ∃ z, x = (2 * m + 1) + z := exists_add_of_le H
Proof state after:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
z : ℕ
hz : x = 2 * m + 1 + z
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : ∀ (x_1 : ℕ), ¬f (f x_1) = x
H : 2 * m + 1 ≤ x
z : ℕ
hz : x = 2 * m + 1 + z
⊢ False
Tactic:
rw [hz] at hx
Proof state after:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
⊢ False
Tactic:
have hzz := hx z
Proof state after:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬f (f z) = 2 * m + 1 + z
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬f (f z) = 2 * m + 1 + z
⊢ False
Tactic:
rw [hf z, add_comm] at hzz
Proof state after:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬2 * m + 1 + z = 2 * m + 1 + z
⊢ False
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a.intro
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
H : 2 * m + 1 ≤ x
z : ℕ
hx : ∀ (x : ℕ), ¬f (f x) = 2 * m + 1 + z
hz : x = 2 * m + 1 + z
hzz : ¬2 * m + 1 + z = 2 * m + 1 + z
⊢ False
Tactic:
exact (hzz rfl).elim
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ {n | n < 2 * m + 1} ⊆ A ∪ B
Tactic:
rw [ab_union]
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ {n | n < 2 * m + 1} ⊆ NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
⊢ {n | n < 2 * m + 1} ⊆ NN \ f '' (f '' NN)
Tactic:
intro x hx
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ NN \ f '' (f '' NN)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ NN \ f '' (f '' NN)
Tactic:
unfold_let NN A at *
Proof state after:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' Set.univ \ f '' (f '' Set.univ)
ab_disjoint : Disjoint (Set.univ \ f '' Set.univ) B
ab_union : Set.univ \ f '' Set.univ ∪ B = Set.univ \ f '' (f '' Set.univ)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
case a
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' Set.univ \ f '' (f '' Set.univ)
ab_disjoint : Disjoint (Set.univ \ f '' Set.univ) B
ab_union : Set.univ \ f '' Set.univ ∪ B = Set.univ \ f '' (f '' Set.univ)
x : ℕ
hx : x ∈ {n | n < 2 * m + 1}
⊢ x ∈ Set.univ \ f '' (f '' Set.univ)
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑(A ∪ B)
Tactic:
rw [ab_range]
Proof state after:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑{n | n < 2 * m + 1}
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
⊢ Fintype ↑{n | n < 2 * m + 1}
Tactic:
exact inferInstance
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1
Tactic:
have hc := @Fintype.card_congr' ↑(A ∪ B)
              {x | x < 2 * m + 1} _ _ (by rw [ab_range])
Proof state after:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
hc : Fintype.card ↑(A ∪ B) = Fintype.card ↑{x | x < 2 * m + 1}
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
hc : Fintype.card ↑(A ∪ B) = Fintype.card ↑{x | x < 2 * m + 1}
⊢ Fintype.card ↑(A ∪ B) = 2 * m + 1
Tactic:
simp only [hc, Fintype.card_ofFinset, Finset.card_range]
Proof state after:
no goals
Theorem: Imo1987P4.imo1987_p4_generalized
Proof state before:
m : ℕ
f : ℕ → ℕ
hf : ∀ (n : ℕ), f (f n) = n + (2 * m + 1)
f_injective : Function.Injective f
NN : Set ℕ := Set.univ
A : Set ℕ := NN \ f '' NN
B : Set ℕ := f '' A
hid : B = f '' NN \ f '' (f '' NN)
ab_disjoint : Disjoint A B
ab_union : A ∪ B = NN \ f '' (f '' NN)
ab_range : A ∪ B = {n | n < 2 * m + 1}
ab_fintype : Fintype ↑(A ∪ B)
⊢ ↑(A ∪ B) = ↑{x | x < 2 * m + 1}
Tactic:
rw [ab_range]
Proof state after:
no goals
Theorem: Imo1998P2.A_maps_to_offDiag_judgePair
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
a : AgreedTriple C J
⊢ a ∈ A r → a.judgePair ∈ Finset.univ.offDiag
Tactic:
simp [A, Finset.mem_offDiag]
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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
Proof 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))
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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]
Proof 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
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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
Proof 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
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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₂⟩
Proof 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
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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), ?_⟩
Proof 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
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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
Proof 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
Theorem: Imo1998P2.A_fibre_over_contestant
Proof 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
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof 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).card =
    (Finset.filter (fun a => a.contestant = c) (A r)).card
Tactic:
rw [A_fibre_over_contestant r]
Proof state after:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ (Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))).card =
    (Finset.filter (fun a => a.contestant = c) (A r)).card
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ (Finset.image Prod.snd (Finset.filter (fun a => a.contestant = c) (A r))).card =
    (Finset.filter (fun a => a.contestant = c) (A r)).card
Tactic:
apply Finset.card_image_of_injOn
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ Set.InjOn Prod.snd ↑(Finset.filter (fun a => a.contestant = c) (A r))
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ Set.InjOn Prod.snd ↑(Finset.filter (fun a => a.contestant = c) (A r))
Tactic:
unfold Set.InjOn
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ ∀ ⦃x₁ : C × JudgePair J⦄,
    x₁ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r)) →
      ∀ ⦃x₂ : C × JudgePair J⦄, x₂ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r)) → x₁.2 = x₂.2 → x₁ = x₂
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
⊢ ∀ ⦃x₁ : C × JudgePair J⦄,
    x₁ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r)) →
      ∀ ⦃x₂ : C × JudgePair J⦄, x₂ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r)) → x₁.2 = x₂.2 → x₁ = x₂
Tactic:
intros
Proof state after:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ x₁✝ = x₂✝
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
case H
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ x₁✝ = x₂✝
Tactic:
ext
Proof state after:
case H.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ 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
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ 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
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ x₁✝.2.2 = x₂✝.2.2
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
case H.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ 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
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ 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
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ x₁✝.2.2 = x₂✝.2.2
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_contestant_card
Proof state before:
case H.a.a
C : Type u_1
J : Type u_2
r : C → J → Prop
inst✝¹ : Fintype J
inst✝ : Fintype C
c : C
x₁✝ : C × JudgePair J
a✝² : x₁✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
x₂✝ : C × JudgePair J
a✝¹ : x₂✝ ∈ ↑(Finset.filter (fun a => a.contestant = c) (A r))
a✝ : x₁✝.2 = x₂✝.2
⊢ x₁✝.2.2 = x₂✝.2.2
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof 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]
Proof 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))
Theorem: Imo1998P2.A_fibre_over_judgePair
Proof 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
Proof 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))