ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n m k : Nat<VAR>mp : 0 < m<VAR>h : n * m = k * m<GOAL>n = k
<VAR>n : Nat<VAR>p : 0 < n<VAR>m k : Nat<GOAL>n * m = n * k ↔ m = k
<VAR>m : Nat<VAR>p : 0 < m<VAR>n k : Nat<GOAL>n * m = k * m ↔ n = k
<VAR>n m : Nat<VAR>h : n * m ≠ 0<GOAL>m ≠ 0
<VAR>n : Nat<VAR>m : Nat<VAR>h : 0 < n<GOAL>m ≤ n * m
<VAR>m : Nat<VAR>n : Nat<VAR>h : 0 < m<GOAL>n ≤ n * m
<VAR>a c b d : Nat<VAR>hac : a < c<VAR>hbd : b ≤ d<VAR>hd : 0 < d<GOAL>a * b < c * d
<VAR>a c b d : Nat<VAR>hac : a < c<VAR>hbd : b ≤ d<VAR>hb : 0 < b<GOAL>a * b < c * d
<VAR>a c b d : Nat<VAR>hac : a ≤ c<VAR>hbd : b < d<VAR>hc : 0 < c<GOAL>a * b < c * d
<VAR>a c b d : Nat<VAR>hac : a ≤ c<VAR>hbd : b < d<VAR>ha : 0 < a<GOAL>a * b < c * d
<VAR>a b c d : Nat<VAR>hac : a < c<VAR>hbd : b < d<GOAL>a * b < c * d
<VAR>a b : Nat<GOAL>a.succ * b.succ = a * b + a + b + 1
<VAR>a b : Nat<GOAL>(a + 1) * (b + 1) = a * b + a + b + 1
<VAR>m k n : Nat<GOAL>k * m ≤ m + n ↔ (k - 1) * m ≤ n
<VAR>a b : Nat<GOAL>a * a - b * b = (a + b) * (a - b)
<VAR>a b : Nat<VAR>h : 0 < a * b<GOAL>0 < b
<VAR>a b : Nat<VAR>h : 0 < a * b<GOAL>0 < a
<VAR>a b : Nat<VAR>h : 0 < a<GOAL>0 < a * b ↔ 0 < b
<VAR>a b : Nat<VAR>h : 0 < b<GOAL>0 < a * b ↔ 0 < a
<VAR>n : Nat<GOAL>n % 2 = 0 ∨ n % 2 = 1
<VAR>a b : Nat<VAR>h : a % b < a<GOAL>b ≤ a
<VAR>z x y : Nat<GOAL>x * z % (y * z) = x % y * z
<VAR>x k n : Nat<VAR>h₁ : n * k ≤ x<GOAL>(x - n * k) % n = x % n
<VAR>a n : Nat<GOAL>a % n % n = a % n
<VAR>a b n : Nat<GOAL>a * b % n = a % n * (b % n) % n
<VAR>m n k : Nat<GOAL>(m % n + k) % n = (m + k) % n
<VAR>m n k : Nat<GOAL>(m + n % k) % k = (m + n) % k
<VAR>a b n : Nat<GOAL>(a + b) % n = (a % n + b % n) % n
<VAR>m n : Nat<GOAL>m ^ n.succ = m * m ^ n
<VAR>m n : Nat<GOAL>m ^ (n + 1) = m * m ^ n
<VAR>m n : Nat<GOAL>m.pow n = m ^ n
<VAR>n : Nat<GOAL>1 <<< n = 2 ^ n
<VAR>n : Nat<VAR>H : 0 < n<GOAL>0 ^ n = 0
<VAR>a : Nat<GOAL>a ^ 2 = a * a
<VAR>a m n : Nat<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>a m n : Nat<GOAL>a ^ (m + n) = a ^ n * a ^ m
<VAR>a m n : Nat<GOAL>a ^ (m * n) = (a ^ m) ^ n
<VAR>a m n : Nat<GOAL>a ^ (m * n) = (a ^ n) ^ m
<VAR>a m n : Nat<GOAL>(a ^ m) ^ n = (a ^ n) ^ m
<VAR>a b n : Nat<GOAL>(a * b) ^ n = a ^ n * b ^ n
<VAR>n : Nat<VAR>h : n ≠ 0<GOAL>1 < 2 ^ n
<VAR>n : Nat<GOAL>1 < 2 ^ n ↔ n ≠ 0
<VAR>n : Nat<GOAL>1 ≤ 2 ^ n
<VAR>a n : Nat<VAR>h : 0 < a<GOAL>0 < a ^ n
<VAR>a n : Nat<VAR>h : 1 < a<GOAL>a ^ n < a ^ (n + 1)
<VAR>a n m : Nat<VAR>h : 1 < a<VAR>w : n < m<GOAL>a ^ n < a ^ m
<VAR>a n m : Nat<VAR>h : 1 < a<VAR>w : n ≤ m<GOAL>a ^ n ≤ a ^ m
<VAR>a n m : Nat<VAR>h : 1 < a<GOAL>a ^ n ≤ a ^ m ↔ n ≤ m
<VAR>a n m : Nat<VAR>h : 1 < a<GOAL>a ^ n < a ^ m ↔ n < m
<VAR>n k : Nat<VAR>h : n ≠ 0<GOAL>k ≤ n.log2 ↔ 2 ^ k ≤ n
<VAR>n k : Nat<VAR>h : n ≠ 0<GOAL>n.log2 < k ↔ n < 2 ^ k
<VAR>n : Nat<VAR>h : n ≠ 0<GOAL>2 ^ n.log2 ≤ n
<VAR>n : Nat<GOAL>n < 2 ^ (n.log2 + 1)
<VAR>a b c : Nat<VAR>H1 : b ∣ a<VAR>H2 : a / b = c<GOAL>a = b * c
<VAR>a b c : Nat<VAR>H : 0 < b<VAR>H' : b ∣ a<GOAL>a / b = c ↔ a = b * c
<VAR>a b c : Nat<VAR>H : 0 < b<VAR>H' : b ∣ a<GOAL>a / b = c ↔ a = c * b
<VAR>k l x : Nat<GOAL>0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
<VAR>x k l : Nat<VAR>w : 1 < x<GOAL>x ^ k ∣ x ^ l ↔ k ≤ l
<VAR>b k l : Nat<GOAL>(b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l
<VAR>m n : Nat<VAR>a : Nat<VAR>h : m ≤ n<GOAL>a ^ m ∣ a ^ n
<VAR>a : Nat<VAR>m n : Nat<VAR>h : m ≤ n<GOAL>a ^ (n - m) * a ^ m = a ^ n
<VAR>p m n k : Nat<VAR>hmn : m ≤ n<VAR>hdiv : p ^ n ∣ k<GOAL>p ^ m ∣ k
<VAR>p k m : Nat<VAR>hk : 1 ≤ k<VAR>hpk : p ^ k ∣ m<GOAL>p ∣ m
<VAR>x m n : Nat<VAR>h : n ≤ m<VAR>hx : 0 < x<GOAL>x ^ m / x ^ n = x ^ (m - n)
<VAR>m n : Nat<GOAL>m <<< (n + 1) = (2 * m) <<< n
<VAR>m n : Nat<GOAL>m <<< (n + 1) = 2 * m <<< n
<VAR>m n : Nat<GOAL>m >>> (n + 1) = (m / 2) >>> n
<VAR>m n k : Nat<GOAL>m <<< (n + k) = m <<< n <<< k
<VAR>m n k : Nat<GOAL>m <<< n <<< k = m <<< (n + k)
<VAR>x n : Nat<GOAL>x <<< n >>> n = x
<VAR>m : Nat<VAR>m_pos : m > 0<VAR>x y : Nat<GOAL>(m * x + y) / m = x + y / m
<VAR>m x y : Nat<GOAL>(m * x + y) % m = y % m
<VAR>m n : Nat<GOAL>m % n / n = 0
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>s : α<VAR>init : s = state 0<VAR>ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)<GOAL>(BitVec.iunfoldr f s).fst = state w
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>value : BitVec w<VAR>a : α<VAR>init : state 0 = a<VAR>step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsb ↑i)<GOAL>BitVec.iunfoldr f a = (state w, BitVec.truncate w value)
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)<GOAL>(∀ (i : Fin w), (BitVec.iunfoldr f (state 0)).snd.getLsb ↑i = (f i (state ↑i)).snd) ∧ (BitVec.iunfoldr f (state 0)).fst = state w
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>i : Fin w<VAR>ind : ∀ (i : Fin w), (f i (state ↑i)).fst = state (↑i + 1)<GOAL>(BitVec.iunfoldr f (state 0)).snd.getLsb ↑i = (f i (state ↑i)).snd
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>value : BitVec w<VAR>a : α<VAR>init : state 0 = a<VAR>step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsb ↑i)<GOAL>BitVec.iunfoldr f a = (state w, value)
<VAR>w : Nat<VAR>α : Type u_1<VAR>f : Fin w → α → α × Bool<VAR>state : Nat → α<VAR>value : BitVec w<VAR>a : α<VAR>init : state 0 = a<VAR>step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsb ↑i)<GOAL>(BitVec.iunfoldr f a).snd = value
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.toNat < 2 ^ w
<VAR>n : Nat<VAR>x : BitVec n<GOAL>x.toNat < 2 ^ n
<VAR>n i : Nat<GOAL>OfNat.ofNat i = BitVec.ofNat n i
<VAR>w x : Nat<GOAL>↑x = BitVec.ofNat w x
<VAR>x : BitVec 0<GOAL>x = BitVec.nil
<VAR>n m : Nat<VAR>h : n = m<VAR>x : Nat<GOAL>BitVec.cast h (BitVec.ofNat n x) = BitVec.ofNat m x
<VAR>n m k : Nat<VAR>h₁ : n = m<VAR>h₂ : m = k<VAR>x : BitVec n<GOAL>BitVec.cast h₂ (BitVec.cast h₁ x) = BitVec.cast ⋯ x
<VAR>n : Nat<VAR>h : n = n<VAR>x : BitVec n<GOAL>BitVec.cast h x = x
<VAR>w : Nat<VAR>msbs : BitVec w<VAR>lsb : Bool<GOAL>msbs ++ BitVec.ofBool lsb = msbs.concat lsb
<VAR>w : Nat<VAR>msb : Bool<VAR>lsbs : BitVec w<GOAL>BitVec.ofBool msb ++ lsbs = BitVec.cast ⋯ (BitVec.cons msb lsbs)
<VAR>w v : Nat<VAR>x : BitVec w<VAR>y : BitVec v<GOAL>x.append y = x ++ y
<VAR>w : Nat<VAR>x : BitVec w<VAR>n : Nat<GOAL>x.shiftLeft n = x <<< n
<VAR>w : Nat<VAR>x : BitVec w<VAR>n : Nat<GOAL>x.ushiftRight n = x >>> n
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.not = ~~~x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.and y = x &&& y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.or y = x ||| y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.xor y = x ^^^ y
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x.neg = -x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.add y = x + y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.sub y = x - y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.mul y = x * y
<VAR>n : Nat<GOAL>BitVec.zero n = 0#n
<VAR>α : Type u<VAR>n : Nat<VAR>v : α<GOAL>(mkArray n v).size = n
<VAR>α : Type u<VAR>a : Array α<VAR>i : Fin a.size<VAR>v : α<GOAL>(a.set i v).size = a.size
<VAR>α : Type u<VAR>a : Array α<VAR>v : α<GOAL>(a.push v).size = a.size + 1
<VAR>α : Type u_1<VAR>a b : List α<VAR>h₁ : a.length = b.length<VAR>h₂ : ∀ (i : Nat) (hi₁ : i < a.length) (hi₂ : i < b.length), a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩<GOAL>a = b
<VAR>α : Type u_1<VAR>a b : Array α<VAR>h₁ : a.size = b.size<VAR>h₂ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), getElem a i hi₁ = getElem b i hi₂<GOAL>a = b
<VAR>α : Type u_1<VAR>n : Nat<VAR>a b : Array α<VAR>hsz₁ : a.size = n<VAR>hsz₂ : b.size = n<VAR>h : ∀ (i : Nat) (hi : i < n), a.getLit i hsz₁ hi = b.getLit i hsz₂ hi<GOAL>a = b
<VAR>α : Type u_1<VAR>a : Array α<VAR>i j : Fin a.size<GOAL>(a.swap i j).size = a.size
<VAR>α : Type u_1<VAR>a : Array α<GOAL>a.pop.size = a.size - 1
<VAR>i j : Nat<VAR>h : i < j<GOAL>j - 1 - (i + 1) < j - i
<VAR>α : Type u_1<VAR>a : Array α<VAR>i : Fin a.size<GOAL>(a.feraseIdx i).size = a.size - 1
<VAR>α : Type u_1<VAR>as bs : Array α<VAR>h : as.data = bs.data<GOAL>as = bs
<VAR>α : Type u_1<VAR>as : List α<VAR>acc : Array α<GOAL>(as.toArrayAux acc).data = acc.data ++ as
<VAR>α : Type u_1<VAR>as : List α<GOAL>(List.toArray as).data = as
<VAR>α : Type u_1<VAR>as : Array α<VAR>n : Nat<VAR>hsz : as.size = n<VAR>i : Nat<VAR>hi : i ≤ as.size<GOAL>as.toListLitAux n hsz i hi (List.drop i as.data) = as.data
<VAR>α : Type u_1<VAR>n : Nat<VAR>as : Array α<VAR>i : Nat<VAR>h₁ : as.size = n<VAR>h₂ : i < n<GOAL>as.getLit i h₁ h₂ = getElem as.data i ⋯
<VAR>α : Type u_1<VAR>as : Array α<VAR>n : Nat<VAR>hsz : as.size = n<GOAL>as = as.toArrayLit n hsz
<VAR>c : Char<GOAL>(String.utf8EncodeChar c).length = c.utf8Size
<VAR>s : String<GOAL>s.toUTF8.size = s.utf8ByteSize
<VAR>i : String.Iterator<VAR>h : i.hasNext = true<GOAL>sizeOf i.next < sizeOf i
<VAR>i : String.Iterator<VAR>h : ¬i.atEnd = true<GOAL>sizeOf i.next < sizeOf i
<VAR>b c : Bool<GOAL>false.atLeastTwo b c = (b && c)
<VAR>a c : Bool<GOAL>a.atLeastTwo false c = (a && c)
<VAR>a b : Bool<GOAL>a.atLeastTwo b false = (a && b)
<VAR>b c : Bool<GOAL>true.atLeastTwo b c = (b || c)
<VAR>a c : Bool<GOAL>a.atLeastTwo true c = (a || c)
<VAR>a b : Bool<GOAL>a.atLeastTwo b true = (a || b)
<VAR>x i : Nat<VAR>x_lt_succ : x < 2 ^ (i + 1)<GOAL>x.testBit i = decide (x ≥ 2 ^ i)
<VAR>x i : Nat<GOAL>x % 2 ^ (i + 1) = 2 ^ i * (x.testBit i).toNat + x % 2 ^ i
<VAR>x y i : Nat<VAR>c : Bool<GOAL>x % 2 ^ i + (y % 2 ^ i + c.toNat) < 2 ^ (i + 1)
<GOAL>∀ {w : Nat} {x y : BitVec w} {c : Bool}, BitVec.carry 0 x y c = c
<VAR>w : Nat<VAR>i : Nat<VAR>x y : BitVec w<VAR>c : Bool<GOAL>BitVec.carry (i + 1) x y c = (x.getLsb i).atLeastTwo (y.getLsb i) (BitVec.carry i x y c)
<VAR>w i : Nat<VAR>i_lt : i < w<VAR>x y : BitVec w<VAR>c : Bool<GOAL>(x + y + BitVec.zeroExtend w (BitVec.ofBool c)).getLsb i = (x.getLsb i).xor ((y.getLsb i).xor (BitVec.carry i x y c))
<VAR>w i : Nat<VAR>i_lt : i < w<VAR>x y : BitVec w<GOAL>(x + y).getLsb i = (x.getLsb i).xor ((y.getLsb i).xor (BitVec.carry i x y false))
<VAR>w : Nat<VAR>x y : BitVec w<VAR>c : Bool<GOAL>x.adc y c = (BitVec.carry w x y c, x + y + BitVec.zeroExtend w (BitVec.ofBool c))
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x + y = (x.adc y false).snd
<VAR>w : Nat<VAR>x : BitVec w<GOAL>x + ~~~x = BitVec.allOnes w
<VAR>w : Nat<VAR>x : BitVec w<GOAL>BitVec.allOnes w - x = ~~~x
<VAR>w : Nat<VAR>x : BitVec w<VAR>i : Fin w<GOAL>(BitVec.iunfoldr (fun i c => (c, !x.getLsb ↑i)) ()).snd.getLsb ↑i = !x.getLsb ↑i
<VAR>w : Nat<VAR>x : BitVec w<GOAL>(BitVec.iunfoldr (fun i c => (c, !x.getLsb ↑i)) ()).snd + x = -1
<VAR>w : Nat<VAR>x : BitVec w<GOAL>(BitVec.iunfoldr (fun i c => (c, !x.getLsb ↑i)) ()).snd = ~~~x
<VAR>w : Nat<VAR>x : BitVec w<GOAL>-x = ((BitVec.iunfoldr (fun i c => (c, !x.getLsb ↑i)) ()).snd.adc (1#w) false).snd
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.ult y = !BitVec.carry w x (~~~y) true
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.ule y = !y.ult x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.ule y = BitVec.carry w y (~~~x) true
<VAR>w : Nat<VAR>x y : BitVec w<VAR>h : x.msb = y.msb<GOAL>x.slt y = x.ult y
<VAR>w : Nat<VAR>x y : BitVec w<VAR>h : x.msb ≠ y.msb<GOAL>x.ult y = y.msb
<VAR>w : Nat<VAR>x y : BitVec w<VAR>h : x.msb ≠ y.msb<GOAL>x.slt y = !x.ult y
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.slt y = (x.msb != y.msb).xor (x.ult y)
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.slt y = (x.msb == y.msb).xor (BitVec.carry w x (~~~y) true)
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.sle y = !y.slt x
<VAR>w : Nat<VAR>x y : BitVec w<GOAL>x.sle y = !(x.msb == y.msb).xor (BitVec.carry w y (~~~x) true)
<VAR>α : Sort u<VAR>self : Lean.Data.AC.Context α<GOAL>Std.Associative self.op
<VAR>e : List Nat<VAR>h : e ≠ []<GOAL>Lean.Data.AC.mergeIdem e ≠ []
<VAR>x : Nat<VAR>xs : List Nat<GOAL>Lean.Data.AC.mergeIdem (x :: x :: xs) = Lean.Data.AC.mergeIdem (x :: xs)
<VAR>x y : Nat<VAR>ys : List Nat<VAR>h : x ≠ y<GOAL>Lean.Data.AC.mergeIdem (x :: y :: ys) = x :: Lean.Data.AC.mergeIdem (y :: ys)
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Lean.Data.AC.ContextInformation.isIdem ctx = true<VAR>e : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.mergeIdem e) = Lean.Data.AC.evalList α ctx e
<VAR>x : Nat<VAR>xs : List Nat<GOAL>Lean.Data.AC.insert x xs ≠ []
<VAR>ys : List Nat<VAR>xs : List Nat<VAR>h : xs ≠ []<GOAL>Lean.Data.AC.sort.loop xs ys ≠ []
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Std.Commutative ctx.op<VAR>x : Nat<VAR>xs : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.insert x xs) = Lean.Data.AC.evalList α ctx (x :: xs)
<VAR>α : Sort u_1<VAR>a b c : List Nat<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Std.Commutative ctx.op<VAR>h₂ : Lean.Data.AC.evalList α ctx a = Lean.Data.AC.evalList α ctx b<VAR>h₃ : a ≠ []<VAR>h₄ : b ≠ []<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop a c) = Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop b c)
<VAR>α : Sort u_1<VAR>y : Nat<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Std.Commutative ctx.op<VAR>xs ys : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop xs (y :: ys)) = Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort.loop (y :: xs) ys)
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Std.Commutative ctx.op<VAR>x : Nat<VAR>xs : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort (x :: xs)) = Lean.Data.AC.evalList α ctx (x :: Lean.Data.AC.sort xs)
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>h : Lean.Data.AC.ContextInformation.isComm ctx = true<VAR>e : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort e) = Lean.Data.AC.evalList α ctx e
<VAR>e : Lean.Data.AC.Expr<GOAL>e.toList ≠ []
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>x : Nat<GOAL>Lean.Data.AC.ContextInformation.isNeutral ctx x = true → Std.LawfulIdentity (Lean.Data.AC.EvalInformation.evalOp ctx) (Lean.Data.AC.EvalInformation.evalVar ctx x)
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>e : List Nat<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.removeNeutrals ctx e) = Lean.Data.AC.evalList α ctx e
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>l r : List Nat<VAR>h₁ : l ≠ []<VAR>h₂ : r ≠ []<GOAL>Lean.Data.AC.evalList α ctx (l.append r) = ctx.op (Lean.Data.AC.evalList α ctx l) (Lean.Data.AC.evalList α ctx r)
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>e : Lean.Data.AC.Expr<GOAL>Lean.Data.AC.evalList α ctx e.toList = Lean.Data.AC.eval α ctx e
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>e : Lean.Data.AC.Expr<GOAL>Lean.Data.AC.evalList α ctx (Lean.Data.AC.norm ctx e) = Lean.Data.AC.eval α ctx e
<VAR>α : Sort u_1<VAR>ctx : Lean.Data.AC.Context α<VAR>a b : Lean.Data.AC.Expr<VAR>h : (Lean.Data.AC.norm ctx a == Lean.Data.AC.norm ctx b) = true<GOAL>Lean.Data.AC.eval α ctx a = Lean.Data.AC.eval α ctx b
<VAR>name : Lake.Name<VAR>self : Lake.NPackage name<GOAL>self.name = name
<VAR>c : Char<GOAL>c.utf8Size ≤ 4
<VAR>p₁ p₂ : String.Pos<GOAL>(p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)
<VAR>p : String.Pos<VAR>c : Char<GOAL>(p + c).byteIdx = p.byteIdx + c.utf8Size
<VAR>s : String<VAR>i : String.Pos<GOAL>i.byteIdx < (s.next i).byteIdx
<VAR>cs : List Char<VAR>i p : String.Pos<GOAL>p ≠ 0 → (String.utf8PrevAux cs i p).byteIdx < p.byteIdx
<VAR>s : String<VAR>i : String.Pos<VAR>h : i ≠ 0<GOAL>(s.prev i).byteIdx < i.byteIdx
<VAR>i : String.Iterator<GOAL>sizeOf i = i.s.utf8ByteSize - i.i.byteIdx
<VAR>c' : Char<VAR>cs : List Char<VAR>i p : String.Pos<GOAL>i > p → String.utf8SetAux c' cs i p = cs
<VAR>s : String<VAR>i : String.Pos<VAR>c : Char<VAR>b₁ b₂ : Nat<VAR>h : (s.next i).byteIdx + b₁ = s.endPos.byteIdx + b₂<GOAL>((s.set i c).next i).byteIdx + b₁ = (s.set i c).endPos.byteIdx + b₂
<VAR>i : String.Pos<VAR>c : Char<VAR>cs : List Char<VAR>a : String.Pos<VAR>b₁ b₂ : Nat<GOAL>(String.utf8GetAux cs a i).utf8Size + b₁ = String.utf8ByteSize.go cs + b₂ → (String.utf8GetAux (String.utf8SetAux c cs a i) a i).utf8Size + b₁ = String.utf8ByteSize.go (String.utf8SetAux c cs a i) + b₂
<VAR>s : String<VAR>i : String.Pos<VAR>c : Char<VAR>h : ¬s.atEnd i = true<GOAL>(s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx < s.endPos.byteIdx - i.byteIdx
<VAR>s : Substring<VAR>i : String.Pos<VAR>h : i.byteIdx < s.bsize<GOAL>i.byteIdx < (s.next i).byteIdx
<VAR>s₁ s₂ : String<VAR>h : s₁.data = s₂.data<GOAL>s₁ = s₂
<VAR>s₁ s₂ : String<GOAL>s₁ = s₂ ↔ s₁.data = s₂.data
<VAR>c : Char<GOAL>(String.singleton c).length = 1
<VAR>s : String<VAR>c : Char<GOAL>(s.push c).length = s.length + 1
<VAR>s : String<VAR>c : Char<VAR>n : Nat<GOAL>(s.pushn c n).length = s.length + n
<VAR>s t : String<GOAL>(s ++ t).length = s.length + t.length
<VAR>s : String<VAR>c : Char<GOAL>(s.push c).data = s.data ++ c :: List.nil
<VAR>s t : String<GOAL>(s ++ t).data = s.data ++ t.data
<VAR>s t : String<GOAL>s < t ↔ s.data < t.data
<VAR>n : Nat<GOAL>{ byteIdx := n }.byteIdx = n
<VAR>p : String.Pos<GOAL>{ byteIdx := p.byteIdx } = p
<VAR>i₁ i₂ : String.Pos<VAR>h : i₁.byteIdx = i₂.byteIdx<GOAL>i₁ = i₂
<VAR>i₁ i₂ : String.Pos<GOAL>i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx
<VAR>p₁ p₂ : String.Pos<GOAL>(p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx
<VAR>p₁ p₂ : String.Pos<GOAL>p₁ + p₂ = { byteIdx := p₁.byteIdx + p₂.byteIdx }
<VAR>p₁ p₂ : String.Pos<GOAL>(p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx
<VAR>p₁ p₂ : String.Pos<GOAL>p₁ - p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }
<VAR>p : String.Pos<VAR>c : Char<GOAL>p + c = { byteIdx := p.byteIdx + c.utf8Size }
<VAR>c : Char<GOAL>(0 + c).byteIdx = c.utf8Size
<VAR>c : Char<GOAL>0 + c = { byteIdx := c.utf8Size }
<VAR>p : String.Pos<VAR>c₁ c₂ : Char<GOAL>p + c₁ + c₂ = p + c₂ + c₁
<VAR>i₁ i₂ : String.Pos<VAR>h : i₁ < i₂<GOAL>i₁ ≠ i₂
<VAR>i₁ i₂ : String.Pos<VAR>h : i₁ < i₂<GOAL>i₂ ≠ i₁
<VAR>p : String.Pos<VAR>s : String<GOAL>(p + s).byteIdx = p.byteIdx + s.utf8ByteSize
<VAR>p : String.Pos<VAR>s : String<GOAL>p + s = { byteIdx := p.byteIdx + s.utf8ByteSize }
<VAR>s : String<GOAL>(0 + s).byteIdx = s.utf8ByteSize
<VAR>s : String<GOAL>0 + s = { byteIdx := s.utf8ByteSize }
<VAR>i₁ i₂ : String.Pos<GOAL>i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx
<VAR>i₁ i₂ : Nat<GOAL>{ byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂
<VAR>i₁ i₂ : String.Pos<GOAL>i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx
<VAR>i₁ i₂ : Nat<GOAL>{ byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂
<VAR>s : String<VAR>p : String.Pos<GOAL>s.get! p = s.get p
<VAR>s : String<VAR>p : String.Pos<GOAL>p < s.next p
<VAR>s : String<VAR>p : String.Pos<VAR>h : ¬s.atEnd p = true<GOAL>s.get' p h = s.get p
<VAR>s : String<VAR>p : String.Pos<VAR>h : ¬s.atEnd p = true<GOAL>s.next' p h = s.next p
<VAR>c : Char<GOAL>String.singleton c = { data := c :: List.nil }
<VAR>c : Char<GOAL>(String.singleton c).data = c :: List.nil
<VAR>s₁ s₂ s₃ : String<GOAL>s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)
<VAR>s : Substring<GOAL>s.prev 0 = 0
<VAR>s : Substring<VAR>n : Nat<GOAL>s.prevn n 0 = 0
<VAR>α : Type<VAR>self : Lake.ModuleFacet α<GOAL>Lake.ModuleData self.name = α
<VAR>k k' : Lake.BuildKey<GOAL>k.quickCmp k' = Ordering.eq → k = k'
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>v : Nat.Linear.Var<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.insertSorted k v p) = Nat.Linear.Poly.denote ctx p + k * Nat.Linear.Var.denote ctx v
<VAR>ctx : Nat.Linear.Context<VAR>p r : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.sort.go p r) = Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx r
<VAR>ctx : Nat.Linear.Context<VAR>m : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx m.sort = Nat.Linear.Poly.denote ctx m
<VAR>ctx : Nat.Linear.Context<VAR>p q : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (p ++ q) = Nat.Linear.Poly.denote ctx p + Nat.Linear.Poly.denote ctx q
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>v : Nat.Linear.Var<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx ((k, v) :: p) = k * Nat.Linear.Var.denote ctx v + Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>p q : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (List.reverseAux p q) = Nat.Linear.Poly.denote ctx (p ++ q)
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (List.reverse p) = Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx p.fuse = Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.mul k p) = k * Nat.Linear.Poly.denote ctx p
<VAR>x y : Nat<VAR>h₁ : ¬x.blt y = true<VAR>h₂ : ¬y.blt x = true<GOAL>x = y
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>m₁ m₂ r₁ r₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)<GOAL>Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>m₁ m₂ r₁ r₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_eq ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)<GOAL>Nat.Linear.Poly.denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_eq ctx (m₁, m₂)<GOAL>Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂)<GOAL>Nat.Linear.Poly.denote_eq ctx (m₁, m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote_eq ctx (m₁.cancel m₂) = Nat.Linear.Poly.denote_eq ctx (m₁, m₂)
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>m₁ m₂ r₁ r₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)<GOAL>Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>m₁ m₂ r₁ r₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_le ctx (Nat.Linear.Poly.cancelAux fuel m₁ m₂ r₁ r₂)<GOAL>Nat.Linear.Poly.denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_le ctx (m₁, m₂)<GOAL>Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<VAR>h : Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂)<GOAL>Nat.Linear.Poly.denote_le ctx (m₁, m₂)
<VAR>ctx : Nat.Linear.Context<VAR>m₁ m₂ : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote_le ctx (m₁.cancel m₂) = Nat.Linear.Poly.denote_le ctx (m₁, m₂)
<VAR>ctx : Nat.Linear.Context<VAR>fuel : Nat<VAR>p₁ p₂ : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.combineAux fuel p₁ p₂) = Nat.Linear.Poly.denote ctx p₁ + Nat.Linear.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>p₁ p₂ : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (p₁.combine p₂) = Nat.Linear.Poly.denote ctx p₁ + Nat.Linear.Poly.denote ctx p₂
<VAR>ctx : Nat.Linear.Context<VAR>e : Nat.Linear.Expr<GOAL>Nat.Linear.Poly.denote ctx e.toPoly = Nat.Linear.Expr.denote ctx e
<VAR>ctx : Nat.Linear.Context<VAR>a b : Nat.Linear.Expr<VAR>h : a.toNormPoly = b.toNormPoly<GOAL>Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b
<VAR>ctx : Nat.Linear.Context<VAR>a b c d : Nat.Linear.Expr<VAR>h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)<GOAL>(Nat.Linear.Expr.denote ctx a = Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c = Nat.Linear.Expr.denote ctx d)
<VAR>ctx : Nat.Linear.Context<VAR>a b c d : Nat.Linear.Expr<VAR>h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)<GOAL>(Nat.Linear.Expr.denote ctx a ≤ Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c ≤ Nat.Linear.Expr.denote ctx d)
<VAR>ctx : Nat.Linear.Context<VAR>a b c d : Nat.Linear.Expr<VAR>h : a.inc.toNormPoly.cancel b.toNormPoly = (c.inc.toPoly, d.toPoly)<GOAL>(Nat.Linear.Expr.denote ctx a < Nat.Linear.Expr.denote ctx b) = (Nat.Linear.Expr.denote ctx c < Nat.Linear.Expr.denote ctx d)
<VAR>c : Nat.Linear.ExprCnstr<GOAL>c.toPoly.norm = c.toNormPoly
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.ExprCnstr<GOAL>Nat.Linear.PolyCnstr.denote ctx c.toPoly = Nat.Linear.ExprCnstr.denote ctx c
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.ExprCnstr<GOAL>Nat.Linear.PolyCnstr.denote ctx c.toNormPoly = Nat.Linear.ExprCnstr.denote ctx c
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Poly.denote ctx (Nat.Linear.Poly.mul.go k p) = k * Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>c : Nat.Linear.PolyCnstr<GOAL>Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.PolyCnstr.mul (k + 1) c) = Nat.Linear.PolyCnstr.denote ctx c