internlm/Lean-Github huggingface dataset:
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 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
p1' : Person
hp1' : p1' = p2 ∨ p1' = ↑↑p4 ∨ p1' = ↑↑p3
p2' : Person
hp2' : p2' = p2 ∨ p2' = ↑↑p4 ∨ p2' = ↑↑p3
hp1p2 : p1' ≠ p2'
hp4d : discusses p2 ↑↑p4 = t2
this : ↑p3 ∈ α
⊢ discusses p2 ↑↑p3 = t2
Tactic:
simp [α] at this
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 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
p1' : Person
hp1' : p1' = p2 ∨ p1' = ↑↑p4 ∨ p1' = ↑↑p3
p2' : Person
hp2' : p2' = p2 ∨ p2' = ↑↑p4 ∨ p2' = ↑↑p3
hp1p2 : p1' ≠ p2'
hp4d : discusses p2 ↑↑p4 = t2
this : discusses p2 ↑↑p3 = t2
⊢ discusses p2 ↑↑p3 = 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}
s2 : Finset Person := Finset.cons (↑↑p4) s1 ⋯
s3 : Finset Person := Finset.cons p2 s2 ⋯
p1' : Person
hp1' : p1' = p2 ∨ p1' = ↑↑p4 ∨ p1' = ↑↑p3
p2' : Person
hp2' : p2' = p2 ∨ p2' = ↑↑p4 ∨ p2' = ↑↑p3
hp1p2 : p1' ≠ p2'
hp4d : discusses p2 ↑↑p4 = t2
this : discusses p2 ↑↑p3 = t2
⊢ discusses p2 ↑↑p3 = t2
Tactic:
exact this
Proof state after:
no goals
Theorem: Imo1964P4.lemma1
Proof state before:
case neg
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:
push_neg at h6
Proof state after:
case neg
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 : { x // x ∈ α }), p3 ≠ p4 → 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 neg
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 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
use t3
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = ↑t3
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = ↑t3
Tactic:
let α' := Finset.map ⟨λ (x :Person') => x.val, Subtype.coe_injective⟩ α
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = ↑t3
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ ∃ s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = ↑t3
Tactic:
use α'
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α'.card ∧ ∀ p1 ∈ α', ∀ p2 ∈ α', p1 ≠ p2 → discusses p1 p2 = ↑t3
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α'.card ∧ ∀ p1 ∈ α', ∀ p2 ∈ α', p1 ≠ p2 → discusses p1 p2 = ↑t3
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α'.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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ ∀ p1 ∈ α', ∀ p2 ∈ α', p1 ≠ p2 → discusses p1 p2 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α'.card
Tactic:
rw [Finset.card_map]
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α.card
Theorem: Imo1964P4.lemma1
Proof state before:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ 2 < α.card
Tactic:
exact ht2
Proof state after:
no goals
Theorem: Imo1964P4.lemma1
Proof state before:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
⊢ ∀ p1 ∈ α', ∀ p2 ∈ α', p1 ≠ p2 → discusses p1 p2 = ↑t3
Tactic:
intro p3' hp3' p4' hp4' hp3p4'
Proof state after:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' : Person
hp3' : p3' ∈ α'
p4' : Person
hp4' : p4' ∈ α'
hp3p4' : p3' ≠ p4'
⊢ discusses p3' p4' = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' : Person
hp3' : p3' ∈ α'
p4' : Person
hp4' : p4' ∈ α'
hp3p4' : p3' ≠ p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
rw [Finset.mem_map] at hp3' hp4'
Proof state after:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' : Person
hp3' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p3'
p4' : Person
hp4' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p4'
hp3p4' : p3' ≠ p4'
⊢ discusses p3' p4' = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' : Person
hp3' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p3'
p4' : Person
hp4' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p4'
hp3p4' : p3' ≠ p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
obtain ⟨⟨p3, p3_ne⟩, p3_mem_α, p3_eq⟩ := hp3'
Proof state after:
case h.right.intro.mk.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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp4' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p4'
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p3, p3_ne⟩ = p3'
⊢ discusses p3' p4' = ↑t3