rw [this] at lkc
case mpr.intro.intro.intro.intro.intro.refine'_1.inl
α : 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 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False
case mpr.intro.intro.intro.intro.intro.refine'_1.inl
α : 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 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False