rw [insert_t]
case 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
⊢ j < (minsert M h).t + 1 ∧
    ∃ j_1,
      j_1 < (minsert M h).t + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
case 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
⊢ j < M.t + 1 + 1 ∧
    ∃ j_1,
      j_1 < M.t + 1 + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)