split_ifs with h_1 h_2 h_3
case h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ ((v ∈ if k = M.t + 1 then C else MultiPart.P M k) ∧ w ∈ if l = M.t + 1 then C else MultiPart.P M l) ∨
    (v ∈ if l = M.t + 1 then C else MultiPart.P M l) ∧ w ∈ if k = M.t + 1 then C else MultiPart.P M k
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ v ∈ C ∧ w ∈ C ∨ v ∈ C ∧ w ∈ C

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ v ∈ C ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ C

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ v ∈ MultiPart.P M k ∧ w ∈ C ∨ v ∈ C ∧ w ∈ MultiPart.P M k

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : ¬l = M.t + 1
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k