internlm/Lean-Github huggingface dataset:
Theorem: Imo1964P4.lemma1
Proof state before:
case pos
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∃ p3 p4, p3 ≠ p4 ∧ discusses ↑↑p3 ↑↑p4 = t2
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
obtain ⟨p3, p4, hp1, hp2⟩ := h6
Proof state after:
case pos.intro.intro.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Theorem: Imo1964P4.lemma1
Proof state before:
case pos.intro.intro.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
use t2
Proof state after:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Tactic:
let s1 : Finset Person := {p3.val.val}
Proof state after:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Tactic:
let s2 : Finset Person := Finset.cons p4.val s1
                           (by rw [Finset.mem_singleton]; intro hp
                               exact (hp1 (Subtype.val_injective
                                      (Subtype.val_injective hp)).symm).elim)
Proof state after:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Tactic:
let s3 : Finset Person := Finset.cons p2 s2
                           (by rw [Finset.mem_cons, Finset.mem_singleton]
                               intro hp
                               cases hp with
                               | inl hp =>
                                 exact (p4.val.property.symm hp).elim
                               | inr hp =>
                                 exact (p3.val.property.symm hp).elim)
Proof state after:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t2
Tactic:
use s3
Proof state after:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ 2 < s3.card ∧ ∀ p1 ∈ s3, ∀ p2 ∈ s3, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
case h
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ 2 < s3.card ∧ ∀ p1 ∈ s3, ∀ p2 ∈ s3, p1 ≠ p2 → discusses p1 p2 = t2
Tactic:
constructor
Proof state after:
case h.left
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ 2 < s3.card

case h.right
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
⊢ ∀ p1 ∈ s3, ∀ p2 ∈ s3, p1 ≠ p2 → discusses p1 p2 = t2
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
⊢ ↑↑p4 ∉ s1
Tactic:
rw [Finset.mem_singleton]
Proof state after:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
⊢ ¬↑↑p4 = ↑↑p3
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
⊢ ¬↑↑p4 = ↑↑p3
Tactic:
intro hp
Proof state after:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
hp : ↑↑p4 = ↑↑p3
⊢ False
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
hp : ↑↑p4 = ↑↑p3
⊢ False
Tactic:
exact (hp1 (Subtype.val_injective
       (Subtype.val_injective hp)).symm).elim
Proof state after:
no goals
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
⊢ p2 ∉ s2
Tactic:
rw [Finset.mem_cons, Finset.mem_singleton]
Proof state after:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
⊢ ¬(p2 = ↑↑p4 ∨ p2 = ↑↑p3)
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
⊢ ¬(p2 = ↑↑p4 ∨ p2 = ↑↑p3)
Tactic:
intro hp
Proof state after:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
p3 p4 : { x // x ∈ α }
hp1 : p3 ≠ p4
hp2 : discusses ↑↑p3 ↑↑p4 = t2
s1 : Finset Person := {↑↑p3}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
hp : p2 = ↑↑p4 ∨ p2 = ↑↑p3
⊢ False