rw [insert_P]
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ (v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else C) ∧ a ∈ MultiPart.P (minsert M h) j