awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
h : Ne (α := ℝ) (↑d : ℝ) 0
⊢ Ne (α := ℝ) (↑sd : ℝ) 0

Tactic:
rw [← mul_self_ne_zero, ← Nat.cast_mul, hd]

Premises used: Nat.cast_mul, mul_self_ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ Ne (α := ℝ) (↑d : ℝ) 0

Tactic:
Invertible.ne_zero _

Premises used: Invertible.ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ Ne (α := ℝ) (↑d : ℝ) 0

Tactic:
exact Invertible.ne_zero _

Premises used: Invertible.ne_zero
-- Module: Mathlib.Tactic.NormNum.RealSqrt
Goal:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv : Invertible (α := ℝ) (↑d : ℝ)
⊢ √(HMul.hMul (α := ℝ) (↑n : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : ℝ) _)) =
    HMul.hMul (α := ℝ) (↑sn : ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑sd : ℝ) _)

Tactic:
simp [← hn, ← hd, Real.sqrt_mul (mul_self_nonneg ↑sn)]

Premises used: mul_self_nonneg, Real.sqrt_mul
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
n : ℕ
⊢ (n + 2).AtLeastTwo

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
n : ℕ
⊢ IsNat n n

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
⊢ IsNat.{u_1} (α := α) n.rawCast n

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsNat.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
a : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.ofNat a) : α) (↑a : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑n : α) (↑(Int.ofNat n) : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℤ
⊢ IsInt.{u_1} (α := α) n.rawCast n

Tactic:
⟨rfl⟩

Premises used: Mathlib.Meta.NormNum.IsInt.mk, rfl
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(Int.negOfNat n) : α) (-(↑n : α))

Tactic:
simp [Int.negOfNat_eq, Int.cast_neg]

Premises used: Int.cast_neg, Int.negOfNat_eq
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℕ
a a' : α
h : IsInt a (Int.ofNat n)
e : (↑n : α) = a'
⊢ a = a'

Tactic:
h.to_isNat.to_eq e

Premises used: Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsNat.to_eq
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Semiring α
num : ℕ
inv : Invertible (α := α) (↑1 : α)
this : Invertible (α := α) 1
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑1 : α) _) = (↑num : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
a denom : ℕ
inv : Invertible (α := α) (↑denom : α)
⊢ HMul.hMul (α := α) (↑(Int.ofNat a) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑a : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ HMul.hMul (α := α) 1 (↑1 : α) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ HMul.hMul (α := α) (↑1 : α) 1 = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Semiring α
n : ℕ
⊢ (↑n : α) = HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑1 : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
num denom : ℕ
inv : Invertible (α := α) (↑denom : α)
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _) =
    HMul.hMul (α := α) (↑(Int.ofNat num) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑denom : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
num : ℤ
inv : Invertible (α := α) (↑1 : α)
this : Invertible (α := α) 1
⊢ HMul.hMul (α := α) (↑num : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑1 : α) _) = (↑num : α)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℤ
⊢ HMul.hMul (α := α) 1 (↑1 : α) = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℤ
⊢ HMul.hMul (α := α) (↑1 : α) 1 = 1

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : Ring α
n : ℤ
⊢ (↑n : α) = HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑1 : α) _)

Tactic:
simp
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u
n d : ℕ
inst : DivisionSemiring α
inv : Invertible (α := α) (↑d : α)
⊢ HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _) = NNRat.rawCast n d

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u
n : ℤ
d : ℕ
inst : DivisionRing α
inv : Invertible (α := α) (↑d : α)
⊢ HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _) = Rat.rawCast n d

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : DivisionRing α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ HMul.hMul (α := α) (↑(Int.negOfNat n) : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _) =
    -HDiv.hDiv (α := α) (↑n : α) (↑d : α)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : DivisionSemiring α
n d : ℕ
inv : Invertible (α := α) (↑d : α)
⊢ HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _) =
    HDiv.hDiv (α := α) (↑n : α) (↑d : α)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : DivisionSemiring α
n d : ℕ
h : Ne.{u_1 + 1} (α := α) (↑d : α) 0
this : Invertible (α := α) (↑d : α)
⊢ NNRat.rawCast n d = HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.NormNum.Result
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
d : ℕ
h : Ne.{u_1 + 1} (α := α) (↑d : α) 0
this : Invertible (α := α) (↑d : α)
⊢ Rat.rawCast n d = HMul.hMul (α := α) (↑n : α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑d : α) _)

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Tactic.Order.Preprocessing
Goal:
α : Type u
inst : Preorder α
x y : α
h : ¬x ≤ y
⊢ ¬x < y

Tactic:
(h ·.le)

Premises used: LT.lt.le, Not
-- Module: Mathlib.Tactic.Order.Preprocessing
Goal:
α : Type u
inst : Preorder α
x y : α
h1 : ¬x < y
h2 : x ≤ y
⊢ y ≤ x

Tactic:
not_lt_iff_le_imp_ge.mp h1 h2

Premises used: Iff.mp, not_lt_iff_le_imp_ge
-- Module: Mathlib.Tactic.Order.ToInt
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
h : val i ∈ sli
⊢ ∃ (j : Fin sli.length),
    getElem (valid := fun (xs : List α) (i : Fin sli.length) ↦ (↑i : ℕ) < xs.length) sli j ⋯ = val i

Tactic:
apply List.get_of_mem

Premises used: List.get_of_mem
-- Module: Mathlib.Tactic.Order.ToInt
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
h : val i ∈ li
⊢ val i ∈ sli

Tactic:
rw [List.Perm.mem_iff (List.mergeSort_perm _ _)]

Premises used: List.mergeSort_perm, List.Perm.mem_iff
-- Module: Mathlib.Tactic.Order.ToInt
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 ∈ li

Tactic:
simp [li]
-- Module: Mathlib.Tactic.Order.ToInt
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

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]
-- Module: Mathlib.Tactic.Order.ToInt
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
h :
  ∀ (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)
⊢ ∃ (tr : Fin n → ℤ), ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

Tactic:
use fun i ↦ (this i).choose

Premises used: Exists.choose
-- Module: Mathlib.Tactic.Order.ToInt
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 :
  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 ↔
    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)

Tactic:
simp only [Fin.getElem_fin, Int.ofNat_le]

Premises used: Fin.getElem_fin, Int.ofNat_le
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
          ℕ)
neg :
  ∀ (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)) :
        ℕ)

Tactic:
by_cases h_eq : val i = val j
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
        ℕ)

Tactic:
simp [h_eq]
-- Module: Mathlib.Tactic.Order.ToInt
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
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 : ℕ) ⋯ = val i)
    (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)) :
          ℕ)
⊢ 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)) :
        ℕ)

Tactic:
generalize_proofs _ hi hj
-- Module: Mathlib.Tactic.Order.ToInt
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 : ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j
⊢ ∃ (j_1 : Fin sli.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) sli (↑j_1 : ℕ) ⋯ = val j

Tactic:
rw [← hi.choose_spec, ← hj.choose_spec] at h_eq

Premises used: Exists.choose_spec
-- Module: Mathlib.Tactic.Order.ToInt
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
⊢ ¬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)) :
          ℕ)
        ⋯

Tactic:
rw [← hi.choose_spec, ← hj.choose_spec] at h_eq

Premises used: Exists.choose_spec
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
          ℕ)
        ⋯
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 : ℕ) ⋯ = 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

Tactic:
rw [← hi.choose_spec, ← hj.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
          ℕ)
        ⋯
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 : ℕ) ⋯ = 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)) :
        ℕ)
⊢ 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)) :
        ℕ)

Tactic:
conv_lhs => rw [← hi.choose_spec, ← hj.choose_spec]

Premises used: Exists.choose_spec
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
          ℕ)
        ⋯
a b c : α
⊢ (fun (a b : α) ↦ decide (a ≤ b)) a b = true →
    (fun (a b : α) ↦ decide (a ≤ b)) b c = true → (fun (a b : α) ↦ decide (a ≤ b)) a c = true

Tactic:
simpa using le_trans

Premises used: le_trans
-- Module: Mathlib.Tactic.Order.ToInt
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)) :
          ℕ)
        ⋯
⊢ ∀ (a b : α), ((fun (a b : α) ↦ decide (a ≤ b)) a b || (fun (a b : α) ↦ decide (a ≤ b)) b a) = true

Tactic:
simpa using le_total

Premises used: le_total