awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
n a : ℕ
h₁ : a.blt n = true
h₂ : IsNat n.minFac n
⊢ FactorsHelper n a [n]

Tactic:
FactorsHelper.nil.cons _ ⟨mul_one _⟩ h₁ h₂

Premises used: Mathlib.Meta.Simproc.FactorsHelper.cons, Mathlib.Meta.NormNum.IsNat.mk, Mathlib.Meta.Simproc.FactorsHelper.nil, mul_one
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
n m a : ℕ
l : List ℕ
h : IsNat (a * m) n
H : FactorsHelper m a l
⊢ FactorsHelper n a (a :: l)

Tactic:
fun pa =>
  H.cons_of_le _ h le_rfl (Nat.prime_def_minFac.1 pa).2 pa

Premises used: Mathlib.Meta.Simproc.FactorsHelper.cons_of_le, le_rfl, And.right, Iff.mp, Nat.prime_def_minFac, Mathlib.Meta.Simproc.FactorsHelper
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
a : ℕ
⊢ FactorsHelper a a [a]

Tactic:
FactorsHelper.nil.cons_self _ ⟨mul_one _⟩

Premises used: Mathlib.Meta.Simproc.FactorsHelper.cons_self, Mathlib.Meta.NormNum.IsNat.mk, Mathlib.Meta.Simproc.FactorsHelper.nil, mul_one
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
n : ℕ
l : List ℕ
H : FactorsHelper n 2 l
⊢ n.primeFactorsList = l

Tactic:
let ⟨h₁, h₂, h₃⟩ := H Nat.prime_two
  have := List.isChain_iff_pairwise.1 (@List.IsChain.tail _ _ (_ :: _) h₁)
  ((Nat.primeFactorsList_unique h₃ h₂).eq_of_pairwise'
     this (Nat.primeFactorsList_sorted _).pairwise).symm

Premises used: Nat.primeFactorsList_sorted, List.SortedLE.pairwise, List.Perm.eq_of_pairwise', Nat.primeFactorsList_unique, Nat.prime_two, List.IsChain.tail, Iff.mp, _private.0.Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq.match_1, List.isChain_iff_pairwise, Eq.symm, Eq, Nat.primeFactorsList
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__discr : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__discr_1 : PLift (a ≤ b)
hab : a ≤ b
h_bn : b < n
m : ℕ := n / b
em : Q(ℕ)
ehm : Q(IsNat (OfNat.ofNat «$em») «$em»)
h_ba_eq : b = a
⊢ a * m = n

Tactic:
simp [m, b, ← h_ba_eq, Nat.mul_div_cancel' (minFac_dvd _)]

Premises used: Nat.minFac_dvd, Nat.mul_div_cancel'
-- Module: Mathlib.Tactic.Simproc.Factors
Goal:
en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__discr : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__discr_1 : PLift (a ≤ b)
hab : a ≤ b
h_bn : ¬b < n
hbn_eq : b = n
hba : ¬b = a
⊢ a < n

Tactic:
lia
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
hnm : n.blt m = true
⊢ Icc m n = ∅

Tactic:
simpa using hnm
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using hmn
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
rw : Icc m n = insert m (Icc (m + 1) n)
rw₁ rw₂ : Icc m n = Icc m n
⊢ Icc m n = insert m s

Tactic:
rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]

Premises used: Finset.insert_Icc_add_one_left_eq_Icc
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc m n = s
rw : Ico m (n + 1) = Icc m n
rw₁ rw₂ : Icc m n = Icc m n
⊢ Ico m (n + 1) = s

Tactic:
rw [← hs, Ico_add_one_right_eq_Icc]

Premises used: Finset.Ico_add_one_right_eq_Icc
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m : ℕ
⊢ Ico m 0 = ∅

Tactic:
simp
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
rw : Ioc m n = Icc (m + 1) n
rw₁ rw₂ : Ioc m n = Ioc m n
⊢ Ioc m n = s

Tactic:
rw [← hs, Icc_add_one_left_eq_Ioc]

Premises used: Finset.Icc_add_one_left_eq_Ioc
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
rw : Ioo m n = Icc (m + 1) (n - 1)
rw₁ rw₂ : Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)
⊢ Ioo m n = s

Tactic:
rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]

Premises used: Finset.Icc_add_one_sub_one_eq_Ioo
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Iic n = s

Tactic:
hs

Premises used: Finset.Icc, Finset.Iic
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
rw : Ico ⊥ (n + 1) = s
rw₁ : Icc ⊥ n = s
rw₂ : Icc 0 n = s
rw₃ rw₄ : s = s
⊢ Iio (n + 1) = s

Tactic:
rw [Iio_eq_Ico, Ico_add_one_right_eq_Icc, bot_eq_zero, hs]

Premises used: Finset.Iio_eq_Ico, Finset.Ico_add_one_right_eq_Icc, bot_eq_zero
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iio 0) ∅

Tactic:
simp
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
hnm : n < m
⊢ Icc m n = ∅

Tactic:
simpa using hnm
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using hmn
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
rw : Icc m n = insert m (Icc (m + 1) n)
rw₁ rw₂ : Icc m n = Icc m n
⊢ Icc m n = insert m s

Tactic:
rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]

Premises used: Finset.insert_Icc_add_one_left_eq_Icc
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
rw : Ico m n = Icc m (n - 1)
rw₁ rw₂ : Ico m n = Ico m n
⊢ Ico m n = s

Tactic:
rw [← hs, Icc_sub_one_right_eq_Ico]

Premises used: Finset.Icc_sub_one_right_eq_Ico
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
rw : Ioc m n = Icc (m + 1) n
rw₁ rw₂ : Ioc m n = Ioc m n
⊢ Ioc m n = s

Tactic:
rw [← hs, Icc_add_one_left_eq_Ioc]

Premises used: Finset.Icc_add_one_left_eq_Ioc
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
rw : Ioo m n = Icc (m + 1) (n - 1)
rw₁ rw₂ : Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)
⊢ Ioo m n = s

Tactic:
rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]

Premises used: Finset.Icc_add_one_sub_one_eq_Ioo
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Icc 1 0) ∅

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Icc 1 1) {1}

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Icc 1 2) {1, 2}

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ico 1 1) ∅

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ico 1 2) {1}

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ico 1 3) {1, 2}

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioc 1 1) ∅

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioc 1 2) {2}

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioc 1 3) {2, 3}

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioo 1 2) ∅

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioo 1 3) {2}

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Ioo 1 4) {2, 3}

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iic 0) {0}

Tactic:
simp only [Iic_ofNat]

Premises used: Finset.Iic_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iic 1) {0, 1}

Tactic:
simp only [Iic_ofNat]

Premises used: Finset.Iic_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iic 2) {0, 1, 2}

Tactic:
simp only [Iic_ofNat]

Premises used: Finset.Iic_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iio 0) ∅

Tactic:
simp only [Iio_ofNat]

Premises used: Finset.Iio_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iio 1) {0}

Tactic:
simp only [Iio_ofNat]

Premises used: Finset.Iio_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℕ) (Iio 2) {0, 1}

Tactic:
simp only [Iio_ofNat]

Premises used: Finset.Iio_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Icc 1 0) ∅

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Icc 1 1) {1}

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Icc 1 2) {1, 2}

Tactic:
simp only [Icc_ofNat_ofNat]

Premises used: Finset.Icc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ico 1 1) ∅

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ico 1 2) {1}

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ico 1 3) {1, 2}

Tactic:
simp only [Ico_ofNat_ofNat]

Premises used: Finset.Ico_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioc 1 1) ∅

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioc 1 2) {2}

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioc 1 3) {2, 3}

Tactic:
simp only [Ioc_ofNat_ofNat]

Premises used: Finset.Ioc_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioo 1 2) ∅

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioo 1 3) {2}

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.FinsetInterval
Goal:
⊢ Eq (α := Finset ℤ) (Ioo 1 4) {2, 3}

Tactic:
simp only [Ioo_ofNat_ofNat]

Premises used: Finset.Ioo_ofNat_ofNat
-- Module: Mathlib.Tactic.Simproc.VecPerm
Goal:
α : Type u_1
m : ℕ
v : Fin m → α
⊢ v = FinVec.etaExpand v

Tactic:
(FinVec.etaExpand_eq _).symm

Premises used: FinVec.etaExpand_eq, Eq.symm
-- Module: Mathlib.Tactic.Translate.GuessName
Goal:
x : String
s : List String
⊢ Prod.Lex (fun (a₁ a₂ : Nat) ↦ a₁ < a₂) (fun (a₁ a₂ : Nat) ↦ a₁ < a₂)
    (s.length + List.length (α := String) [], s.length)
    (List.length (α := String) [] + (x :: s).length, List.length (α := String) [])

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.GuessName
Goal:
pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h : (pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun (a₁ a₂ : Nat) ↦ a₁ < a₂) (fun (a₁ a₂ : Nat) ↦ a₁ < a₂)
    ((List.drop 1 (s' ++ [pre]) ++ l).length + List.length (α := String) [], (List.drop 1 (s' ++ [pre]) ++ l).length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.GuessName
Goal:
pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun (a₁ a₂ : Nat) ↦ a₁ < a₂) (fun (a₁ a₂ : Nat) ↦ a₁ < a₂)
    (l.length + List.length (α := String) [], l.length) ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.GuessName
Goal:
pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun (a₁ a₂ : Nat) ↦ a₁ < a₂) (fun (a₁ a₂ : Nat) ↦ a₁ < a₂) (l.length + (s' ++ [pre]).length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
r_1 r : ArgReorder
n : Nat
cycle : { l : List Nat // 2 ≤ l.length }
⊢ cycle.val (p := fun (l : List Nat) ↦ 2 ≤ l.length) ≠ []

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
r : ArgReorder
x : Nat × ArgReorder
h : x ∈ r.argReorders
mk :
  ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
    x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
      sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
⊢ sizeOf x.snd < sizeOf r

Tactic:
cases r
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
x : Nat × ArgReorder
perm : Permutation
argReorders : Array (Nat × ArgReorder)
h : x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }

Tactic:
grind [→ Array.sizeOf_lt_of_mem]

Premises used: Array.sizeOf_lt_of_mem
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
r : ArgReorder
x : Nat × ArgReorder
h : x ∈ r.argReorders
mk mk₁ :
  ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
    x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
      sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
⊢ sizeOf x.snd < sizeOf r

Tactic:
decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]

Premises used: Array.sizeOf_lt_of_mem
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
r : ArgReorder
perm : List String :=
  List.map
    (fun (x : Subtype (Membership.mem r.perm)) ↦
      match (motive := Subtype (Membership.mem r.perm) → String) x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun (x_1 : Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length)))) ↦
              match (motive := Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length))) → String)
                x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length).attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h : x ∈ r.argReorders
mk :
  ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
    x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
      sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
⊢ sizeOf x.snd < sizeOf r

Tactic:
cases r
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
x : Nat × ArgReorder
perm_1 : Permutation
argReorders : Array (Nat × ArgReorder)
perm : List String :=
  List.map
    (fun (x : Subtype (Membership.mem { perm := perm_1, argReorders := argReorders : ArgReorder }.perm)) ↦
      match (motive :=
        Subtype (Membership.mem { perm := perm_1, argReorders := argReorders : ArgReorder }.perm) → String) x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun (x_1 : Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length)))) ↦
              match (motive := Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length))) → String)
                x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length).attach))
    (List.attach { perm := perm_1, argReorders := argReorders : ArgReorder }.perm)
h : x ∈ { perm := perm_1, argReorders := argReorders : ArgReorder }.argReorders
⊢ sizeOf x.snd < sizeOf { perm := perm_1, argReorders := argReorders : ArgReorder }

Tactic:
grind [→ Array.sizeOf_lt_of_mem]

Premises used: Array.sizeOf_lt_of_mem
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
r : ArgReorder
perm : List String :=
  List.map
    (fun (x : Subtype (Membership.mem r.perm)) ↦
      match (motive := Subtype (Membership.mem r.perm) → String) x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun (x_1 : Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length)))) ↦
              match (motive := Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length))) → String)
                x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length).attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h : x ∈ r.argReorders
mk mk₁ :
  ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
    x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
      sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
⊢ sizeOf x.snd < sizeOf r

Tactic:
decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]

Premises used: Array.sizeOf_lt_of_mem
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
n : Nat
map_1 : Vector (Option (Fin n)) n
map_2 : Vector (Option (Fin n)) n := map_1
perm_1 : List { l : List Nat // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
r : MProd (Option Permutation) (MProd (Vector (Option (Fin n)) n) (List { l : List Nat // 2 ≤ l.length }))
r_1 : MProd (Vector (Option (Fin n)) n) (List { l : List Nat // 2 ≤ l.length }) := r.snd
map_3 : Vector (Option (Fin n)) n := r_1.fst
perm_2 : List { l : List Nat // 2 ≤ l.length } := r_1.snd
j_1 : Fin n
j_2 : Fin n := j_1
j : Fin n
map : Vector (Option (Fin n)) n
perm : List { l : List Nat // 2 ≤ l.length }
y : PUnit
⊢ 2 ≤ [i, (↑j : Nat)].length

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
n : Nat
map_1 : Vector (Option (Fin n)) n
map_2 : Vector (Option (Fin n)) n := map_1
perm_1 : List { l : List Nat // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
r : MProd (Option Permutation) (MProd (Vector (Option (Fin n)) n) (List { l : List Nat // 2 ≤ l.length }))
r_1 : MProd (Vector (Option (Fin n)) n) (List { l : List Nat // 2 ≤ l.length }) := r.snd
map_3 : Vector (Option (Fin n)) n := r_1.fst
perm_2 : List { l : List Nat // 2 ≤ l.length } := r_1.snd
j_1 : Fin n
j_2 : Fin n := j_1
j_3 : Fin n
map_4 : Vector (Option (Fin n)) n
perm : List { l : List Nat // 2 ≤ l.length }
y : PUnit
cycle_1 : { l : List Nat // 2 ≤ l.length } := Subtype.mk (p := fun (l : List Nat) ↦ 2 ≤ l.length) [i, (↑j_3 : Nat)] ⋯
x : Unit
r_2 : MProd (Option Permutation) (MProd { l : List Nat // 2 ≤ l.length } (MProd (Fin n) (Vector (Option (Fin n)) n)))
r_3 : MProd { l : List Nat // 2 ≤ l.length } (MProd (Fin n) (Vector (Option (Fin n)) n)) := r_2.snd
cycle_2 : { l : List Nat // 2 ≤ l.length } := r_3.fst
x_1 : MProd (Fin n) (Vector (Option (Fin n)) n) := r_3.snd
j_4 : Fin n := x_1.fst
map_5 : Vector (Option (Fin n)) n := x_1.snd
j' : Fin n
map : Vector (Option (Fin n)) n := map_5.set! (↑j_4 : Nat) none
cycle : { l : List Nat // 2 ≤ l.length }
j_5 : Fin n
y_1 : PUnit
j : Fin n := j'
⊢ 2 ≤ (cycle.val (p := fun (l : List Nat) ↦ 2 ≤ l.length) ++ [(↑j : Nat)]).length

Tactic:
grind
-- Module: Mathlib.Tactic.Translate.Reorder
Goal:
reorder : ArgReorder
decl : ConstantInfo
map_1 : Vector (Option (Fin decl.levelParams.length)) decl.levelParams.length :=
  Vector.replicate decl.levelParams.length none
x : { l : List Nat // 2 ≤ l.length }
r : Vector (Option (Fin decl.levelParams.length)) decl.levelParams.length
map : Vector (Option (Fin decl.levelParams.length)) decl.levelParams.length := r
cycle : List Nat
property : 2 ≤ cycle.length
⊢ cycle ≠ []

Tactic:
grind
-- Module: Mathlib.Tactic.Zify
Goal:
a b : ℕ
⊢ a ≠ b ↔ Ne (α := ℤ) (↑a : ℤ) (↑b : ℤ)

Tactic:
not_congr Int.ofNat_inj.symm

Premises used: Int.ofNat_inj, Iff.symm, not_congr
-- Module: Mathlib.Tactic.Zify
Goal:
R : Type u_1
inst : AddGroupWithOne R
m n k : ℕ
h : m + k ≤ n
⊢ (↑(n - m) : R) = HSub.hSub (α := R) (↑n : R) (↑m : R)

Tactic:
Nat.cast_sub (m.le_add_right k |>.trans h)

Premises used: Nat.cast_sub, Nat.le_add_right, LE.le.trans
-- Module: Mathlib.Tactic.Zify
Goal:
R : Type u_1
inst : AddGroupWithOne R
m n : ℕ
h : m < n
⊢ (↑(n - m) : R) = HSub.hSub (α := R) (↑n : R) (↑m : R)

Tactic:
Nat.cast_sub h.le

Premises used: Nat.cast_sub, LT.lt.le
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
e_opt :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
⊢ Option.getD
      (Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m))
      y =
    (List.dlookup (β := fun (x : α) ↦ β) x m).getD y

Tactic:
congr 1
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
⊢ Eq.{v + 1} (α := Option β)
    (Option.map (α := (_ : α) × β) (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) []) :
      Option β)
    (List.dlookup (β := fun (x : α) ↦ β) x [] : Option β)

Tactic:
simp
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
p : (_ : α) × β
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
e_opt :
  ∀ (fst : α) (snd : β),
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
          (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
      List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) (p :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (p :: m)

Tactic:
rcases p with ⟨fst, snd⟩
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
pos :
  ∀ (heq : fst = x),
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
          (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
      List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
neg :
  ∀ (heq : ¬fst = x),
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
          (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
      List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)

Tactic:
by_cases heq : fst = x
-- Module: Mathlib.Testing.Plausible.Functions
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : fst = x
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)

Tactic:
simp [heq]