rw [insert_P, insert_P] at lkc
case mpr.intro.intro.intro.intro.intro.refine'_3.inr
α : 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 ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
case mpr.intro.intro.intro.intro.intro.refine'_3.inr
α : 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 ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
lkc : (v ∈ if l ≠ M.t + 1 then MultiPart.P M l else C) ∧ w ∈ if k ≠ M.t + 1 then MultiPart.P M k else C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k