use α'
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
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