obtain ⟨k, hkr, l, hlr, lnek, lkc⟩ := hins
case mpr
α : 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
hins : Adj (mp (minsert M h)) v w
⊢ Adj (mp M) v w
case mpr.intro.intro.intro.intro.intro
α : 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 ((minsert M h).t + 1)
l : ℕ
hlr : l ∈ range ((minsert M h).t + 1)
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ Adj (mp M) v w