-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (goal)
Goal:
α : Type u_1
inst : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun (a b : α) ↦ decide (a ≤ b)
this_1 :
  ∀ (i : Fin n),
    ∃ (j : Fin sli.length),
      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ = val i
i j : Fin n
pf : ∀ (j : Fin sli.length), (↑j : ℕ) < sli.length
hi : ∃ (j : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i
hj : ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j
h_eq :
  ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hi.choose (p := fun (j : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
          ℕ)
        ⋯ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
          ℕ)
        ⋯
this :
  ∀ (i j : Fin (li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).length) (_hij : i < j),
    decide ((li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun (a b : α) ↦ decide (a ≤ b)).get j) =
      true
neg :
  ∀
    (h :
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
          (↑(hi.choose (p := fun (j : Fin sli.length) ↦
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
            ℕ)
          ⋯ ≤
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
          (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
            ℕ)
          ⋯),
    (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ) ≤
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
        ℕ)
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hi.choose (p := fun (j : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
          ℕ)
        ⋯ ≤
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
        (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
          ℕ)
        ⋯ ↔
    (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ) ≤
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
        ℕ)
have neg₁ : ∀
  (h :
    (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
        ℕ) ≤
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
        ℕ)),
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
      (↑(hi.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
        ℕ)
      sorry ≤
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli
      (↑(hj.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
        ℕ)
      sorry
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩