awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd
have refine : Invertible (α := ℝ) (↑sd : ℝ)
Tactic: refine ⟨?_, ?out⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
refine : Invertible (α := ℝ) (↑sd : ℝ)
⊢ IsNNRat (√(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _))) sn sd
have out : √(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)) =
  HMul.hMul (α := ℝ) (↑sn : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑sd : ℝ) _)
Tactic: refine ⟨?_, ?out⟩
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ Invertible (α := ℝ) (↑sd : ℝ)
have h : Ne (α := ℝ) (↑sd : ℝ) 0
Tactic: apply invertibleOfNonzero
-- Lean 4 proof step from Mathlib.Tactic.NormNum.RealSqrt (goal)
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ Ne (α := ℝ) (↑sd : ℝ) 0
have h : Ne (α := ℝ) (↑d : ℝ) 0
Tactic: rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]
-- 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)
i : Fin n
⊢ ∃ (j : Fin sli.length),
    getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ = val i
have h : val i ∈ sli
Tactic: apply List.get_of_mem
-- 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)
i : Fin n
⊢ val i ∈ sli
have h : val i ∈ li
Tactic: rw [List.Perm.mem_iff (List.mergeSort_perm _ _)]
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (hypothesis)
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)
⊢ ∃ (tr : Fin n → ℤ), ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j
have this : ∀ (i : Fin n),
  ∃ (j : Fin sli.length),
    getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j sorry = val i
Tactic: have (i : Fin n) : ∃ j : Fin sli.length, sli[j] = val i := by
    apply List.get_of_mem
    rw [List.Perm.mem_iff (List.mergeSort_perm _ _)]
    simp [li]
-- 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 :
  ∀ (i : Fin n),
    ∃ (j : Fin sli.length),
      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ = val i
⊢ ∃ (tr : Fin n → ℤ), ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j
have h : ∀ (i j : Fin n),
  val i ≤ val j ↔
    LE.le (α := ℤ)
      ((fun (i : Fin n) ↦
          ((↑(↑(sorry.choose (p := fun (j : Fin sli.length) ↦
                      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j sorry =
                        val i)) :
                  ℕ) :
              ℤ) :
            ℤ))
        i)
      ((fun (i : Fin n) ↦
          ((↑(↑(sorry.choose (p := fun (j : Fin sli.length) ↦
                      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j sorry =
                        val i)) :
                  ℕ) :
              ℤ) :
            ℤ))
        j)
Tactic: use fun i ↦ (this i).choose
-- 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 :
  ∀ (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
⊢ val i ≤ val j ↔
    LE.le (α := ℤ)
      ((fun (i : Fin n) ↦
          ((↑(↑(⋯.choose (p := fun (j : Fin sli.length) ↦
                      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ =
                        val i)) :
                  ℕ) :
              ℤ) :
            ℤ))
        i)
      ((fun (i : Fin n) ↦
          ((↑(↑(⋯.choose (p := fun (j : Fin sli.length) ↦
                      getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ =
                        val i)) :
                  ℕ) :
              ℤ) :
            ℤ))
        j)
have h : val i ≤ val j ↔
  (↑(sorry.choose (p := fun (j : Fin sli.length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
      ℕ) ≤
    (↑(sorry.choose (p := fun (j_1 : Fin sli.length) ↦
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
      ℕ)
Tactic: simp only [Fin.getElem_fin, Int.ofNat_le]
-- 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 :
  ∀ (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
⊢ val i ≤ val j ↔
    (↑(⋯.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ) ≤
      (↑(⋯.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
        ℕ)
have pos : ∀ (h_eq : val i = val j),
  val i ≤ val j ↔
    (↑(sorry.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
        ℕ) ≤
      (↑(sorry.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
        ℕ)
Tactic: by_cases h_eq : val i = val j
-- 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 :
  ∀ (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
pos :
  ∀ (h_eq : val i = val j),
    val i ≤ val j ↔
      (↑(⋯.choose (p := fun (j : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
          ℕ) ≤
        (↑(⋯.choose (p := fun (j_1 : Fin sli.length) ↦
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
          ℕ)
⊢ val i ≤ val j ↔
    (↑(⋯.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ) ≤
      (↑(⋯.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_eq : ¬val i = val j),
  val i ≤ val j ↔
    (↑(sorry.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)) :
        ℕ) ≤
      (↑(sorry.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j)) :
        ℕ)
Tactic: by_cases h_eq : val i = val j
-- 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 :
  ∀ (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
h_eq : ¬val i = val j
⊢ val i ≤ val j ↔
    (↑(⋯.choose (p := fun (j : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) ⋯ = val i)) :
        ℕ) ≤
      (↑(⋯.choose (p := fun (j_1 : Fin sli.length) ↦
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j)) :
        ℕ)
have neg : ∀ (pf : ∀ (j : Fin sli.length), (↑j : ℕ) < sli.length)
  (hi : ∃ (j : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j : ℕ) sorry = val i)
  (hj :
    ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) sorry = val j),
  val i ≤ val j ↔
    (↑(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)) :
        ℕ)
Tactic: generalize_proofs _ hi hj
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (hypothesis)
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 :
  ∀ (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
h_eq : ¬val i = val j
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 hj₁ : ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j
⊢ val i ≤ 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 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 : ℕ) 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: rw [← hi.choose_spec, ← hj.choose_spec] at h_eq
Cleared hypotheses: h_eq, hj
-- 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 :
  ∀ (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)) :
          ℕ)
        ⋯
| val i ≤ val j
have rw : 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: rw [← hi.choose_spec, ← hj.choose_spec]
-- 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 :
  ∀ (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)) :
          ℕ)
        ⋯
⊢ val i ≤ 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 : 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 ↔
  (↑(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)) :
      ℕ)
Tactic: conv_lhs => rw [← hi.choose_spec, ← hj.choose_spec]
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (hypothesis)
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 :
  ∀ (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)) :
          ℕ)
        ⋯
⊢ 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 this₁ : List.Pairwise (fun (a b : α) ↦ decide (a ≤ b) = true) (li.mergeSort fun (a b : α) ↦ decide (a ≤ b))
Tactic: have := li.pairwise_mergeSort (le := fun a b ↦ decide (a ≤ b))
      (fun a b c ↦ by simpa using le_trans) (by simpa using le_total)
-- Lean 4 proof step from Mathlib.Tactic.Order.ToInt (hypothesis)
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 : List.Pairwise (fun (a b : α) ↦ decide (a ≤ b) = true) (li.mergeSort fun (a b : α) ↦ decide (a ≤ b))
⊢ 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 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
Tactic: rw [List.pairwise_iff_get] at this
Cleared hypotheses: this
-- 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
⊢ 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 :
    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),
  (↑(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)) :
      ℕ)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩