rw [← sin, card_biUnion] at hs2
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
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ 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 : ∑ u in range (M.t + 1), card (S ∩ MultiPart.P M u) = 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
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ 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 (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = 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
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)