Theorem: Imo1964P4.lemma1 (Compfiles/Imo1964P4.lean)

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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
have p2 : Person := Nonempty.some (Fintype.card_pos_iff.mp (by omega))
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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
let Person' := {p3 // p3 ≠ p2}
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 }
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

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 }
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
have hfcα : 4 < Fintype.card Person' := by
  rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton]
  exact lt_tsub_of_add_lt_left card_person
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'
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

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'
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
have h1 : Fintype.card Topic * 2 < Fintype.card Person' := by omega
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'
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

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'
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
have h2 := Fintype.exists_lt_card_fiber_of_mul_lt_card
            (fun (p3: Person') ↦ discusses p2 p3.val) h1
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'
h2 : ∃ y, 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = y) Finset.univ).card
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

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'
h2 : ∃ y, 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = y) Finset.univ).card
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
obtain ⟨t2, ht2⟩ := h2
State after:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

State before:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
let α := (Finset.filter (fun (x : Person') ↦ discusses p2 ↑x = t2) Finset.univ)
State after:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

State before:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
let Topic' := {t3 // t3 ≠ t2}
State after:
case 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 }
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

State before:
case 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 }
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
have h4 : Fintype.card Topic' = 1 := by
  simp [Fintype.card_subtype_compl, card_topic, Topic']
State after:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

State before:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
obtain ⟨t3, ht3⟩ := Fintype.card_eq_one_iff.mp h4
State after:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t

State before:
case 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
⊢ ∃ t s, 2 < s.card ∧ ∀ p1 ∈ s, ∀ p2 ∈ s, p1 ≠ p2 → discusses p1 p2 = t
Tactic:
by_cases h6 : ∃ p3 p4 : α, p3 ≠ p4 ∧ discusses p3.val p4.val = t2
State after:
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

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

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
⊢ 0 < Fintype.card Person
Tactic:
omega
State after:
no goals

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 }
⊢ 4 < Fintype.card Person'
Tactic:
rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton]
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 }
⊢ 4 < Fintype.card Person - 1

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 }
⊢ 4 < Fintype.card Person - 1
Tactic:
exact lt_tsub_of_add_lt_left card_person
State after:
no goals

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'
⊢ Fintype.card Topic * 2 < Fintype.card Person'
Tactic:
omega
State after:
no goals

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 }
⊢ Fintype.card Topic' = 1
Tactic:
simp [Fintype.card_subtype_compl, card_topic, Topic']
State after:
no goals

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
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

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
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

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}
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

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)
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

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)
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

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
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

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
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

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]
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

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
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

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
State after:
no goals

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]
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)

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
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

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 ⋯
hp : p2 = ↑↑p4 ∨ p2 = ↑↑p3
⊢ False
Tactic:
cases hp with
| inl hp =>
  exact (p4.val.property.symm hp).elim
| inr hp =>
  exact (p3.val.property.symm hp).elim
State after:
no goals

State before:
case inl
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
⊢ False
Tactic:
exact (p4.val.property.symm hp).elim
State after:
no goals

State before:
case inr
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 = ↑↑p3
⊢ False
Tactic:
exact (p3.val.property.symm hp).elim
State after:
no goals

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
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
Tactic:
simp (config := {decide := true})
  only [Finset.card_cons, Finset.card_singleton, s1, s2, s3]
State after:
no goals

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
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
Tactic:
intro p1' hp1' p2' hp2' hp1p2
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
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' ∈ s3
p2' : Person
hp2' : p2' ∈ s3
hp1p2 : p1' ≠ p2'
⊢ discusses p1' p2' = t2

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
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' ∈ s3
p2' : Person
hp2' : p2' ∈ s3
hp1p2 : p1' ≠ p2'
⊢ discusses p1' p2' = t2
Tactic:
rw [Finset.mem_cons, Finset.mem_cons, Finset.mem_singleton] at hp1' hp2'
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
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'
⊢ discusses p1' p2' = t2

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
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'
⊢ discusses p1' p2' = t2
Tactic:
have hp4d : discusses p2 ↑↑p4 = t2 := by
   have := p4.property; simp [α] at this; exact this
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
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
⊢ discusses p1' p2' = t2

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
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
⊢ discusses p1' p2' = t2
Tactic:
have hp3d : discusses p2 ↑↑p3 = t2 := by
   have := p3.property; simp [α] at this; exact this
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
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
hp3d : discusses p2 ↑↑p3 = t2
⊢ discusses p1' p2' = t2

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
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
hp3d : discusses p2 ↑↑p3 = t2
⊢ discusses p1' p2' = t2
Tactic:
aesop
State after:
no goals

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'
⊢ discusses p2 ↑↑p4 = t2
Tactic:
have := p4.property
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'
this : ↑p4 ∈ α
⊢ discusses p2 ↑↑p4 = t2

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'
this : ↑p4 ∈ α
⊢ discusses p2 ↑↑p4 = t2
Tactic:
simp [α] at this
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'
this : discusses p2 ↑↑p4 = t2
⊢ discusses p2 ↑↑p4 = t2

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'
this : discusses p2 ↑↑p4 = t2
⊢ discusses p2 ↑↑p4 = t2
Tactic:
exact this
State after:
no goals

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
⊢ discusses p2 ↑↑p3 = t2
Tactic:
have := p3.property
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 : ↑p3 ∈ α
⊢ discusses p2 ↑↑p3 = t2

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
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

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
State after:
no goals

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
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

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
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

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⟩ α
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

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

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
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

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]
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

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
State after:
no goals

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

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

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

State before:
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
Tactic:
obtain ⟨⟨p4, p4_ne⟩, p4_mem_α, p4_eq⟩ := hp4'
State after:
case h.right.intro.mk.intro.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
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'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p4, p4_ne⟩ = p4'
⊢ discusses p3' p4' = ↑t3

State before:
case h.right.intro.mk.intro.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
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'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p4, p4_ne⟩ = p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
dsimp at p3_eq p4_eq
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3' p4' = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
rw [←p3_eq, ←p4_eq]
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3 p4 = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3 p4 = ↑t3
Tactic:
have hne : p3 ≠ p4 := by rwa [p3_eq, p4_eq]
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ discusses p3 p4 = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ discusses p3 p4 = ↑t3
Tactic:
have h8 := h6 ⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ⟨⟨p4, p4_ne⟩, p4_mem_α⟩
              (by simp[hne, Person', Topic'])
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
⊢ discusses p3 p4 = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
⊢ discusses p3 p4 = ↑t3
Tactic:
let t3': Topic' := ⟨discusses p3 p4, h8⟩
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
⊢ discusses p3 p4 = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
⊢ discusses p3 p4 = ↑t3
Tactic:
have h9 := ht3 t3'
State after:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
h9 : t3' = t3
⊢ discusses p3 p4 = ↑t3

State before:
case h.right.intro.mk.intro.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
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
h9 : t3' = t3
⊢ discusses p3 p4 = ↑t3
Tactic:
rw [←h9]
State after:
no goals

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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ p3 ≠ p4
Tactic:
rwa [p3_eq, p4_eq]
State after:
no goals

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
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ ⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ≠ ⟨⟨p4, p4_ne⟩, p4_mem_α⟩
Tactic:
simp[hne, Person', Topic']
State after:
no goals