refine ⟨i,hi,j,hj,?_⟩
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)