obtain ⟨j, hjr, hjm⟩ := inv_part ha
case e_s.a
α : 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
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
case e_s.a.intro.intro
α : 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
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)