rw [← insert_t M h] at this
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : M.t + 1 ∈ range (M.t + 1 + 1)
⊢ ¬Adj (mp (minsert M h)) v w
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
⊢ ¬Adj (mp (minsert M h)) v w