rw [mem_inter] at *
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∩ MultiPart.P M i
hb : b ∈ S ∩ MultiPart.P M i
ne : a ≠ b
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
⊢ False