ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ctx : Nat.Linear.Context<VAR>c₁ c₂ : Nat.Linear.PolyCnstr<VAR>h₁ : Nat.Linear.PolyCnstr.denote ctx c₁<VAR>h₂ : Nat.Linear.PolyCnstr.denote ctx c₂<GOAL>Nat.Linear.PolyCnstr.denote ctx (c₁.combine c₂)
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<VAR>k : Nat<GOAL>p.isNum? = some k → Nat.Linear.Poly.denote ctx p = k
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<VAR>h : p.isZero = true<GOAL>Nat.Linear.Poly.denote ctx p = 0
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<VAR>h : p.isNonZero = true<GOAL>Nat.Linear.Poly.denote ctx p > 0
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.PolyCnstr<GOAL>c.isUnsat = true → Nat.Linear.PolyCnstr.denote ctx c = False
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.PolyCnstr<GOAL>c.isValid = true → Nat.Linear.PolyCnstr.denote ctx c = True
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.ExprCnstr<VAR>h : c.toNormPoly.isUnsat = true<GOAL>Nat.Linear.ExprCnstr.denote ctx c = False
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.ExprCnstr<VAR>h : c.toNormPoly.isValid = true<GOAL>Nat.Linear.ExprCnstr.denote ctx c = True
<VAR>ctx : Nat.Linear.Context<VAR>c : Nat.Linear.PolyCnstr<VAR>cs : Nat.Linear.Certificate<VAR>h : Nat.Linear.PolyCnstr.denote ctx (Nat.Linear.Certificate.combineHyps c cs) → False<GOAL>Nat.Linear.PolyCnstr.denote ctx c → Nat.Linear.Certificate.denote ctx cs
<VAR>ctx : Nat.Linear.Context<VAR>cs : Nat.Linear.Certificate<VAR>h : Nat.Linear.PolyCnstr.denote ctx cs.combine → False<GOAL>Nat.Linear.Certificate.denote ctx cs
<VAR>ctx : Nat.Linear.Context<VAR>cs : Nat.Linear.Certificate<VAR>h : cs.combine.isUnsat = true<GOAL>Nat.Linear.Certificate.denote ctx cs
<VAR>ctx : Nat.Linear.Context<VAR>k : Nat<VAR>v : Nat.Linear.Var<GOAL>Nat.Linear.Expr.denote ctx (Nat.Linear.monomialToExpr k v) = k * Nat.Linear.Var.denote ctx v
<VAR>ctx : Nat.Linear.Context<VAR>e : Nat.Linear.Expr<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Expr.denote ctx (Nat.Linear.Poly.toExpr.go e p) = Nat.Linear.Expr.denote ctx e + Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>p : Nat.Linear.Poly<GOAL>Nat.Linear.Expr.denote ctx p.toExpr = Nat.Linear.Poly.denote ctx p
<VAR>ctx : Nat.Linear.Context<VAR>c d : Nat.Linear.ExprCnstr<VAR>h : (c.toNormPoly == d.toPoly) = true<GOAL>Nat.Linear.ExprCnstr.denote ctx c = Nat.Linear.ExprCnstr.denote ctx d
<VAR>ctx : Nat.Linear.Context<VAR>e e' : Nat.Linear.Expr<VAR>h : (e.toNormPoly == e'.toPoly) = true<GOAL>Nat.Linear.Expr.denote ctx e = Nat.Linear.Expr.denote ctx e'
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a :: l ≠ []
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a :: l ≠ l
<GOAL>∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂
<GOAL>∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂
<VAR>α : Type u_1<VAR>a : α<VAR>l l' : List α<GOAL>a :: l = a :: l' ↔ l = l'
<VAR>α : Type u_1<VAR>a b : α<VAR>l l' : List α<GOAL>a :: l = b :: l' ↔ a = b ∧ l = l'
<VAR>α : Type u_1<VAR>l : List α<GOAL>l ≠ [] → ∃ b L, l = b :: L
<GOAL>∀ {α : Type u_1} {l : List α}, l.length = 0 → l = []
<GOAL>∀ {α : Type u_1} {l : List α} {n : Nat}, l.length = n + 1 → l ≠ []
<GOAL>∀ {α : Type u_1} {l : List α}, l.length = 0 ↔ l = []
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → 0 < l.length
<VAR>α : Type u_1<VAR>l : List α<GOAL>0 < l.length → ∃ a, a ∈ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>0 < l.length ↔ ∃ a, a ∈ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>0 < l.length → ∃ h t, l = h :: t
<VAR>α : Type u_1<VAR>l : List α<GOAL>0 < l.length ↔ ∃ h t, l = h :: t
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>l.length = n + 1 → ∃ h t, l = h :: t
<VAR>α : Type u_1<VAR>l : List α<GOAL>0 < l.length ↔ l ≠ []
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.length = 1 ↔ ∃ a, l = [a]
<GOAL>∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a
<VAR>α : Type u_1<VAR>i : Nat<VAR>a : α<VAR>as : List α<VAR>h : i + 1 < (a :: as).length<GOAL>(a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<VAR>i : Fin as.length<GOAL>(a :: as).get i.succ = as.get i
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>l.length ≤ n → l.get? n = none
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l.get? n = some (l.get ⟨n, h⟩)
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, l.get? n = some a ↔ ∃ h, l.get ⟨n, h⟩ = a
<GOAL>∀ {α : Type u_1} {l : List α} {n : Nat}, l.get? n = none ↔ l.length ≤ n
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<GOAL>l.get? i = l[i]?
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Fin l.length<GOAL>l.get i = l[↑i]
<VAR>α : Type u_1<VAR>n : Nat<GOAL>[][n]? = none
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l)[0]? = some a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<GOAL>(a :: l)[n + 1]? = l[n]?
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>l.length ≤ n → l[n]? = none
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l[n]? = some l[n]
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>l[n]? = some a ↔ ∃ h, l[n] = a
<GOAL>∀ {α : Type u_1} {l : List α} {n : Nat}, l[n]? = none ↔ l.length ≤ n
<GOAL>∀ {α : Type u_1} {l : List α} {n : Nat}, l.length ≤ n → l[n]? = none
<VAR>α : Type u_1<VAR>Inhabited α<VAR>n : Nat<GOAL>[][n]! = default
<VAR>α : Type u_1<VAR>a : α<VAR>Inhabited α<VAR>l : List α<GOAL>(a :: l)[0]! = a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>Inhabited α<VAR>l : List α<GOAL>(a :: l)[n + 1]! = l[n]!
<GOAL>∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂
<VAR>α : Type u_1<VAR>Inhabited α<VAR>l : List α<VAR>n : Nat<GOAL>l.length ≤ n → l.get! n = default
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.get? 0 = l.head?
<VAR>α : Type u_1<VAR>l l' : List α<VAR>h : l = l'<VAR>i : Nat<VAR>w : i < l.length<GOAL>l[i] = l'[i]
<VAR>α : Type u_1<VAR>l l' : List α<VAR>h : l = l'<VAR>i : Fin l.length<GOAL>l.get i = l'.get ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>i : Nat<VAR>a : α<VAR>h : i < 1<GOAL>[a][i] = a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Fin 1<GOAL>[a].get n = a
<VAR>α : Type u_1<VAR>l : List α<VAR>h : 0 < l.length<GOAL>l[0] = l.head ⋯
<VAR>α : Type u_1<VAR>l : List α<VAR>h : 0 < l.length<GOAL>l.get ⟨0, h⟩ = l.head ⋯
<VAR>α : Type u_1<VAR>a : α<VAR>Inhabited α<VAR>l : List α<VAR>n : Nat<GOAL>l[n]? = some a → l[n]! = a
<VAR>α : Type u_1<VAR>a : α<VAR>Inhabited α<VAR>l : List α<VAR>n : Nat<GOAL>l.get? n = some a → l.get! n = a
<VAR>α : Type u_1<VAR>Inhabited α<VAR>l : List α<VAR>n : Nat<GOAL>l.get! n = l.getD n default
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : ∀ (n : Nat), l₁[n]? = l₂[n]?<GOAL>l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>hl : l₁.length = l₂.length<VAR>h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n] = l₂[n]<GOAL>l₁ = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>hl : l₁.length = l₂.length<VAR>h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩<GOAL>l₁ = l₂
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<VAR>i : Nat<GOAL>i = l.length → ∀ (w : i < (l ++ [a]).length), (l ++ [a])[i] = a
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>(l ++ [a])[l.length]? = some a
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>(l ++ [a]).get? l.length = some a
<VAR>α : Type u_1<VAR>a : α<GOAL>¬a ∈ []
<GOAL>∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ a :: l
<VAR>α : Type u_1<VAR>y : α<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → a ∈ y :: l
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<GOAL>∃ x, x ∈ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l = [] ↔ ∀ (a : α), ¬a ∈ l
<GOAL>∀ {α : Type u_1} {a b : α}, a ∈ [b] → a = b
<VAR>α : Type u_1<VAR>a b : α<GOAL>a ∈ [b] ↔ a = b
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<GOAL>(∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x
<VAR>α : Type u_1<VAR>p : α → Prop<GOAL>¬∃ x x_1, p x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>x : α<GOAL>x ∈ [] → p x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<VAR>l : List α<GOAL>(∃ x x_1, p x) ↔ p a ∨ ∃ x x_1, p x
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>a : α<GOAL>(∀ (x : α), x ∈ [a] → p x) ↔ p a
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∈ [] ↔ False
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∈ [a]
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>a ∈ b :: l → b ∈ l → a ∈ l
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<VAR>h' : a ∈ b :: l<GOAL>a = b ∨ a ≠ b ∧ a ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>l ≠ []
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>as : List α<GOAL>List.elem a as = true ↔ a ∈ as
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>as : List α<GOAL>List.elem a as = decide (a ∈ as)
<VAR>α : Type u_1<VAR>a y : α<VAR>l : List α<VAR>h₁ : a ≠ y<VAR>h₂ : a ∈ y :: l<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>¬a ∈ b :: l → a ≠ b
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>¬a ∈ b :: l → ¬a ∈ l
<VAR>α : Type u_1<VAR>a y : α<VAR>l : List α<GOAL>a ≠ y → ¬a ∈ l → ¬a ∈ y :: l
<VAR>α : Type u_1<VAR>a y : α<VAR>l : List α<GOAL>¬a ∈ y :: l → a ≠ y ∧ ¬a ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → ∃ n h, l[n] = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ n, l.get n = a
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l[n] ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l.get ⟨n, h⟩ ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ n h, l[n] = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ n, l.get n = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ n, l[n]? = some a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ n, l.get? n = some a
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<VAR>e : l[n]? = some a<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<VAR>e : l.get? n = some a<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ n, l[n]? = some a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ n, l.get? n = some a
<VAR>α : Type u_1<VAR>y a : α<VAR>BEq α<VAR>LawfulBEq α<VAR>l : List α<GOAL>decide (y ∈ a :: l) = (y == a || decide (y ∈ l))
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>l.any p = decide (∃ x, x ∈ l ∧ p x = true)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>l.all p = decide (∀ (x : α), x ∈ l → p x = true)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>l.any p = true ↔ ∃ x, x ∈ l ∧ p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>[].set n a = []
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>a : α<GOAL>(x :: xs).set 0 a = a :: xs
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>n : Nat<VAR>a : α<GOAL>(x :: xs).set (n + 1) a = x :: xs.set n a
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>a : α<VAR>h : i < (l.set i a).length<GOAL>(l.set i a)[i] = a
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>a : α<VAR>h : i < (l.set i a).length<GOAL>(l.set i a).get ⟨i, h⟩ = a
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>a : α<VAR>h : i < (l.set i a).length<GOAL>(l.set i a)[i]? = some a
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a)[j] = l[j]
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<VAR>h : i ≠ j<VAR>a : α<GOAL>(l.set i a)[j]? = l[j]?
<VAR>α : Type u_1<VAR>l : List α<VAR>m n : Nat<VAR>a : α<VAR>h : n < (l.set m a).length<GOAL>(l.set m a)[n] = if m = n then a else l[n]
<VAR>α : Type u_1<VAR>l : List α<VAR>m n : Nat<VAR>a : α<VAR>h : n < (l.set m a).length<GOAL>(l.set m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, ⋯⟩
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<VAR>a : α<GOAL>(l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : l.length ≤ n<VAR>a : α<GOAL>l.set n a = l
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.set n a = [] ↔ l = []
<VAR>α : Type u_1<VAR>a b : α<VAR>n m : Nat<VAR>l : List α<GOAL>n ≠ m → (l.set n a).set m b = (l.set m b).set n a
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<VAR>n : Nat<GOAL>(l.set n a).set n b = l.set n b
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<VAR>a : α<GOAL>a ∈ l.set n a
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a b : α<GOAL>a ∈ l.set n b → a ∈ l ∨ a = b
<VAR>α : Type u_1<VAR>LT α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>l : List α<GOAL>¬l < l
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z<VAR>l₁ l₂ l₃ : List α<VAR>h₁ : l₁ < l₂<VAR>h₂ : l₂ < l₃<GOAL>l₁ < l₃
<VAR>α : Type u_1<VAR>LT α<VAR>lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y<VAR>l₁ l₂ : List α<VAR>h₁ : ¬l₁ < l₂<VAR>h₂ : ¬l₂ < l₁<GOAL>l₁ = l₂
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>l : List α<VAR>f : β → α → m β<VAR>b : β<GOAL>List.foldlM f b l.reverse = List.foldrM (fun x y => f y x) b l
<VAR>m : Type u_1 → Type u_2<VAR>β : Type u_1<VAR>α : Type u_3<VAR>Monad m<VAR>LawfulMonad m<VAR>f : β → α → m β<VAR>b : β<VAR>l l' : List α<GOAL>List.foldlM f b (l ++ l') = do let init ← List.foldlM f b l List.foldlM f init l'
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>a : α<VAR>l : List α<VAR>f : α → β → m β<VAR>b : β<GOAL>List.foldrM f b (a :: l) = List.foldrM f b l >>= f a
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<GOAL>List.foldl f b l = List.foldlM f b l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>b : β<VAR>l : List α<GOAL>List.foldr f b l = List.foldrM f b l
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m β<VAR>b : β<VAR>l l' : List α<GOAL>List.foldrM f b (l ++ l') = do let init ← List.foldrM f b l' List.foldrM f init l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>l l' : List α<GOAL>List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>b : β<VAR>l l' : List α<GOAL>List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l
<VAR>α : Type u_1<VAR>l' : List α<VAR>l : List α<GOAL>List.foldr List.cons l' l = l ++ l'
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.foldr List.cons [] l = l
<VAR>β₁ : Type u_1<VAR>β₂ : Type u_2<VAR>α : Type u_3<VAR>f : β₁ → β₂<VAR>g : α → β₂ → α<VAR>l : List β₁<VAR>init : α<GOAL>List.foldl g init (List.map f l) = List.foldl (fun x y => g x (f y)) init l
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : Type u_3<VAR>f : α₁ → α₂<VAR>g : α₂ → β → β<VAR>l : List α₁<VAR>init : β<GOAL>List.foldr g init (List.map f l) = List.foldr (fun x y => g (f x) y) init l
<VAR>α β : Type u<VAR>g : α → β<VAR>f : α → α → α<VAR>f' : β → β → β<VAR>a : α<VAR>l : List α<VAR>h : ∀ (x y : α), f' (g x) (g y) = g (f x y)<GOAL>List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)
<VAR>α β : Type u<VAR>g : α → β<VAR>f : α → α → α<VAR>f' : β → β → β<VAR>a : α<VAR>l : List α<VAR>h : ∀ (x y : α), f' (g x) (g y) = g (f x y)<GOAL>List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.getD n a = l[n]?.getD a
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.getD n a = (l.get? n).getD a
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.getLast h = l.get ⟨l.length - 1, ⋯⟩
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h₁ : a :: l ≠ []<VAR>h₂ : l ≠ []<GOAL>(a :: l).getLast h₁ = l.getLast h₂
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : a :: l ≠ []<GOAL>(a :: l).getLast h = l.getLastD a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l.getLastD a = l.getLast?.getD a
<VAR>α : Type u_1<VAR>a : α<VAR>h : [a] ≠ []<GOAL>[a].getLast h = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>Inhabited α<GOAL>(a :: l).getLast! = l.getLastD a
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.getLast h ∈ l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>l.getLastD a ∈ a :: l
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>n : Nat<VAR>h : n = xs.length<GOAL>(x :: xs)[n] = (x :: xs).getLast ⋯
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>n : Nat<VAR>h : n = xs.length<GOAL>(x :: xs).get ⟨n, ⋯⟩ = (x :: xs).getLast ⋯
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l).getLast? = some (l.getLastD a)
<VAR>α : Type u_1<VAR>a : α<GOAL>[a].getLast? = some a
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.getLast? = some (l.getLast h)
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.getLast? = l.get? (l.length - 1)
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(l ++ [a]).getLast? = some a
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>(l ++ [b]).getLastD a = b
<VAR>α : Type u_1<VAR>a : α<VAR>Inhabited α<VAR>l : List α<GOAL>l.head? = some a → l.head! = a
<VAR>α : Type u_1<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.head? = some (l.head h)
<VAR>α : Type u_1<VAR>l l' : List α<GOAL>l.tailD l' = l.tail?.getD l'
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map id l = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.map (fun a => a) l = l
<VAR>α : Type u_1<VAR>f : α → α<VAR>h : ∀ (x : α), f x = x<VAR>l : List α<GOAL>List.map f l = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>List.map f [a] = [f a]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>as : List α<VAR>f : α → β<GOAL>(List.map f as).length = as.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>n : Nat<GOAL>(List.map f l)[n]? = Option.map f l[n]?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>n : Nat<GOAL>(List.map f l).get? n = Option.map f (l.get? n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>n : Nat<VAR>h : n < (List.map f l).length<GOAL>(List.map f l)[n] = f l[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>n : Fin (List.map f l).length<GOAL>(List.map f l).get n = f (l.get ⟨↑n, ⋯⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>f : α → β<VAR>l : List α<GOAL>b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ f a = b
<GOAL>∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {f : α_1 → α} {l : List α_1}, b ∈ List.map f l → ∃ a, a ∈ l ∧ f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>l : List α<VAR>f : α → β<VAR>h : a ∈ l<GOAL>f a ∈ List.map f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f g : α → β<GOAL>List.map f l = List.map g l ↔ ∀ (a : α), a ∈ l → f a = g a
<GOAL>∀ {α : Type u_1} {l : List α} {α_1 : Type u_2} {f g : α → α_1}, (∀ (a : α), a ∈ l → f a = g a) → List.map f l = List.map g l
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1}, List.map f = List.map g ↔ f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l = [] ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>h : List.map f l = []<GOAL>l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>l₂ : List β<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (List.map f) l.tail? = some l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>l₂ : List β<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f a = b ∧ List.map f l₁ = l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l = List.foldr (fun a bs => f a :: bs) [] l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>(List.map f l).set n (f a) = List.map f (l.set n a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>w : List.map f l ≠ []<GOAL>(List.map f l).head w = f (l.head ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).head? = Option.map f l.head?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>a : α<GOAL>(List.map f l).headD (f a) = f (l.headD a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).tail? = Option.map (List.map f) l.tail?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l l' : List α<GOAL>(List.map f l).tailD (List.map f l') = List.map f (l.tailD l')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>h : List.map f l ≠ []<GOAL>(List.map f l).getLast h = f (l.getLast ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).getLast? = Option.map f l.getLast?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>a : α<GOAL>(List.map f l).getLastD (f a) = f (l.getLastD a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l₁ l₂ : List α<GOAL>List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>g : β → γ<VAR>f : α → β<VAR>l : List α<GOAL>List.map g (List.map f l) = List.map (g ∘ f) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<VAR>P : β → Prop<GOAL>(∀ (i : β), i ∈ List.map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : p a = true<GOAL>List.filter p (a :: l) = a :: List.filter p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : ¬p a = true<GOAL>List.filter p (a :: l) = List.filter p l
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>p : α → Bool<GOAL>List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>(List.filter p l).length ≤ l.length
<GOAL>∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ (a : α), a ∈ l → p a = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).length = l.length ↔ ∀ (a : α), a ∈ l → p a = true
<GOAL>∀ {α : Type u_1} {x : α} {p : α → Bool} {as : List α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = [] ↔ ∀ (a : α), a ∈ l → ¬p a = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} (q : α → Bool) (l : List α), List.filter p (List.filter q l) = List.filter (fun a => decide (p a = true ∧ q a = true)) l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>p : α → Bool<VAR>f : β → α<VAR>l : List β<GOAL>List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : α → Bool<VAR>as : List α<GOAL>List.map f (List.filter p as) = List.foldr (fun a bs => bif p a then f a :: bs else bs) [] as
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<GOAL>List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>(∀ (x : α), x ∈ l → p x = q x) → List.filter p l = List.filter q l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>a : α<VAR>l : List α<VAR>h : f a = none<GOAL>List.filterMap f (a :: l) = List.filterMap f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>a : α<VAR>l : List α<VAR>b : β<VAR>h : f a = some b<GOAL>List.filterMap f (a :: l) = b :: List.filterMap f l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>List.filterMap (some ∘ f) = List.map f
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.filterMap some l = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l : List α<GOAL>List.map some (List.filterMap f l) = List.filter (fun b => b.isSome) (List.map f l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l : List α<GOAL>(List.filterMap f l).length ≤ l.length
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, (List.filterMap f l).length = l.length ↔ ∀ (a : α), a ∈ l → (f a).isSome = true
<VAR>α : Type u_1<VAR>p : α → Bool<GOAL>List.filterMap (Option.guard fun x => p x = true) = List.filter p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>g : β → Option γ<VAR>l : List α<GOAL>List.filterMap g (List.filterMap f l) = List.filterMap (fun x => (f x).bind g) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → Option β<VAR>g : β → γ<VAR>l : List α<GOAL>List.map g (List.filterMap f l) = List.filterMap (fun x => Option.map g (f x)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → Option γ<VAR>l : List α<GOAL>List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l