nth_rw 2 [ht] at ub
case intro.mk
α : 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
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1
⊢ False
case intro.mk
α : 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
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
⊢ False