ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a0 a1 a2 a3 a4 a5 a6 a7 a8 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 8).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8
<VAR>a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 : Int<VAR>t : List Int<GOAL>(Lean.Omega.LinearCombo.coordinate 9).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<GOAL>(l₁ + l₂).const = l₁.const + l₂.const
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<GOAL>(l₁ + l₂).coeffs = l₁.coeffs + l₂.coeffs
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<GOAL>(l₁ - l₂).const = l₁.const - l₂.const
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<GOAL>(l₁ - l₂).coeffs = l₁.coeffs - l₂.coeffs
<VAR>l : Lean.Omega.LinearCombo<GOAL>(-l).const = -l.const
<VAR>l : Lean.Omega.LinearCombo<GOAL>(-l).coeffs = -l.coeffs
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<GOAL>l₁ - l₂ = l₁ + -l₂
<VAR>lc : Lean.Omega.LinearCombo<VAR>i : Int<GOAL>(i * lc).const = i * lc.const
<VAR>lc : Lean.Omega.LinearCombo<VAR>i : Int<GOAL>(i * lc).coeffs = i * lc.coeffs
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<GOAL>(l₁ + l₂).eval v = l₁.eval v + l₂.eval v
<VAR>lc : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<GOAL>(-lc).eval v = -lc.eval v
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<GOAL>(l₁ - l₂).eval v = l₁.eval v - l₂.eval v
<VAR>lc : Lean.Omega.LinearCombo<VAR>i : Int<VAR>v : Lean.Omega.Coeffs<GOAL>(i * lc).eval v = i * lc.eval v
<VAR>lc : Lean.Omega.LinearCombo<VAR>i : Int<VAR>v : Lean.Omega.Coeffs<GOAL>(i * lc).eval v = lc.eval v * i
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<VAR>w : l₁.coeffs.isZero<GOAL>(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<VAR>w : l₂.coeffs.isZero<GOAL>(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
<VAR>l₁ l₂ : Lean.Omega.LinearCombo<VAR>v : Lean.Omega.Coeffs<VAR>w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero<GOAL>(l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
<VAR>p : Prop<VAR>h : p = True<GOAL>p
<VAR>p : Prop<VAR>h : p = False<GOAL>¬p
<VAR>p : Prop<VAR>h : p<GOAL>p = True
<VAR>p : Prop<VAR>h : ¬p<GOAL>p = False
<VAR>p : Prop<VAR>h : p → False<GOAL>p = False
<VAR>p : Prop<VAR>Decidable p<VAR>h : decide p = true<GOAL>p = True
<VAR>p : Prop<GOAL>∀ {x : Decidable p}, decide p = false → p = False
<VAR>α : Sort u_1<VAR>a : α<GOAL>(a = a) = True
<VAR>p₁ p₂ : Sort u<VAR>q₁ q₂ : Sort v<VAR>h₁ : p₁ = p₂<VAR>h₂ : q₁ = q₂<GOAL>(p₁ → q₁) = (p₂ → q₂)
<VAR>p₁ p₂ q₁ q₂ : Prop<VAR>h₁ : p₁ ↔ p₂<VAR>h₂ : q₁ ↔ q₂<GOAL>(p₁ ↔ q₁) ↔ (p₂ ↔ q₂)
<VAR>p₁ p₂ q₁ : Prop<VAR>h₁ : p₁ = p₂<VAR>q₂ : p₂ → Prop<VAR>h₂ : ∀ (h : p₂), q₁ = q₂ h<GOAL>(p₁ → q₁) = ∀ (h : p₂), q₂ h
<VAR>p₁ p₂ q₁ q₂ : Prop<VAR>h₁ : p₁ = p₂<VAR>h₂ : p₂ → q₁ = q₂<GOAL>(p₁ → q₁) = (p₂ → q₂)
<VAR>α : Sort u<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a = q a<GOAL>(∀ (a : α), p a) = ∀ (a : α), q a
<VAR>p₁ p₂ : Prop<VAR>q₁ : p₁ → Prop<VAR>q₂ : p₂ → Prop<VAR>h₁ : p₁ = p₂<VAR>h₂ : ∀ (a : p₂), q₁ ⋯ = q₂ a<GOAL>(∀ (a : p₁), q₁ a) = ∀ (a : p₂), q₂ a
<VAR>α : Sort u<VAR>β : Sort v<VAR>a a' : α<VAR>b b' : α → β<VAR>h₁ : a = a'<VAR>h₂ : ∀ (x : α), b x = b' x<GOAL>(let x := a; b x) = let x := a'; b' x
<VAR>α : Sort u<VAR>β : Sort v<VAR>a a' : α<VAR>b : α → β<VAR>h : a = a'<GOAL>(let x := a; b x) = let x := a'; b x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>b b' : (a : α) → β a<VAR>a : α<VAR>h : ∀ (x : α), b x = b' x<GOAL>(let x := a; b x) = let x := a; b' x
<VAR>α : Sort u_1<VAR>b c : Prop<VAR>x y u v : α<VAR>s : Decidable b<VAR>Decidable c<VAR>h₁ : b = c<VAR>h₂ : c → x = u<VAR>h₃ : ¬c → y = v<GOAL>ite b x y = ite c u v
<VAR>p q : Prop<VAR>h₁ : p = q<VAR>h₂ : q<GOAL>p
<VAR>p q : Prop<VAR>h₁ : p = q<VAR>h₂ : ¬q<GOAL>¬p
<VAR>b c : Prop<VAR>α : Sort u_1<GOAL>∀ {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
<VAR>α : Sort u_1<VAR>a b : α<GOAL>(a ≠ b) = ¬a = b
<VAR>α : Sort u_1<VAR>a b : α<GOAL>ite True a b = a
<VAR>α : Sort u_1<VAR>a b : α<GOAL>ite False a b = b
<VAR>α : Sort u<VAR>t : True → α<VAR>e : ¬True → α<GOAL>dite True t e = t True.intro
<VAR>α : Sort u<VAR>t : False → α<VAR>e : ¬False → α<GOAL>dite False t e = e not_false
<VAR>α : Sort u<VAR>c : Prop<GOAL>∀ {x : Decidable c} (a b : α), c = True → ite c a b = a
<VAR>α : Sort u<VAR>c : Prop<GOAL>∀ {x : Decidable c} (a b : α), c = False → ite c a b = b
<VAR>α : Sort u<VAR>c : Prop<GOAL>∀ {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = True), dite c t e = t ⋯
<VAR>α : Sort u<VAR>c : Prop<GOAL>∀ {x : Decidable c} {t : c → α} {e : ¬c → α} (h : c = False), dite c t e = e ⋯
<VAR>α : Sort u<VAR>c : Prop<VAR>d : Decidable c<VAR>a : α<GOAL>ite c a a = a
<VAR>p : Prop<GOAL>(p ∧ True) = p
<VAR>p : Prop<GOAL>(True ∧ p) = p
<VAR>p : Prop<GOAL>(p ∧ False) = False
<VAR>p : Prop<GOAL>(False ∧ p) = False
<VAR>p : Prop<GOAL>(p ∧ p) = p
<VAR>a : Prop<GOAL>¬(a ∧ ¬a)
<VAR>a : Prop<GOAL>¬(¬a ∧ a)
<VAR>a b c : Prop<GOAL>a ∧ b → c ↔ a → b → c
<VAR>a b : Prop<GOAL>¬(a ∧ b) ↔ a → ¬b
<VAR>p : Prop<GOAL>(p ∨ p) = p
<VAR>p : Prop<GOAL>(p ∨ True) = True
<VAR>p : Prop<GOAL>(True ∨ p) = True
<VAR>p : Prop<GOAL>(p ∨ False) = p
<VAR>p : Prop<GOAL>(False ∨ p) = p
<VAR>p : Prop<GOAL>(p ↔ p) = True
<VAR>p : Prop<GOAL>(p ↔ True) = p
<VAR>p : Prop<GOAL>(True ↔ p) = p
<VAR>p : Prop<GOAL>(p ↔ False) = ¬p
<VAR>p : Prop<GOAL>(False ↔ p) = ¬p
<VAR>a : Prop<GOAL>¬(¬a ↔ a)
<VAR>a b c : Prop<VAR>h : a → (b ↔ c)<GOAL>a ∧ b ↔ a ∧ c
<VAR>c a b : Prop<VAR>h : c → (a ↔ b)<GOAL>a ∧ c ↔ b ∧ c
<VAR>a b c : Prop<GOAL>(a ∧ b) ∧ c ↔ a ∧ b ∧ c
<VAR>a b : Prop<GOAL>a ∧ a ∧ b ↔ a ∧ b
<VAR>a b : Prop<GOAL>(a ∧ b) ∧ b ↔ a ∧ b
<VAR>a b c : Prop<GOAL>(a ∧ b ↔ a ∧ c) ↔ a → (b ↔ c)
<VAR>a c b : Prop<GOAL>(a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)
<VAR>a b : Prop<VAR>h : a → b<GOAL>a ∧ b ↔ a
<VAR>b a : Prop<VAR>h : b → a<GOAL>a ∧ b ↔ b
<VAR>a b : Prop<GOAL>(a ∧ b ↔ a) ↔ a → b
<VAR>a b : Prop<GOAL>(a ∧ b ↔ b) ↔ b → a
<VAR>p q : Prop<GOAL>(p ↔ p ∧ q) ↔ p → q
<VAR>p q : Prop<GOAL>(p ↔ q ∧ p) ↔ p → q
<VAR>a c b d : Prop<VAR>f : a → c<VAR>g : b → d<VAR>h : a ∨ b<GOAL>c ∨ d
<VAR>a b c : Prop<VAR>f : a → b<GOAL>a ∨ c → b ∨ c
<VAR>b c a : Prop<VAR>f : b → c<GOAL>a ∨ b → a ∨ c
<VAR>a b c : Prop<GOAL>(a ∨ b) ∨ c ↔ a ∨ b ∨ c
<VAR>a b : Prop<GOAL>a ∨ a ∨ b ↔ a ∨ b
<VAR>a b : Prop<GOAL>(a ∨ b) ∨ b ↔ a ∨ b
<VAR>a b : Prop<VAR>ha : a → b<GOAL>a ∨ b ↔ b
<VAR>b a : Prop<VAR>hb : b → a<GOAL>a ∨ b ↔ a
<VAR>a b : Prop<GOAL>(a ∨ b ↔ a) ↔ b → a
<VAR>a b : Prop<GOAL>(a ∨ b ↔ b) ↔ a → b
<VAR>a b : Prop<GOAL>(a ↔ a ∨ b) ↔ b → a
<VAR>a b : Prop<GOAL>(b ↔ a ∨ b) ↔ a → b
<VAR>a b : Bool<GOAL>((a || b) = true) = (a = true ∨ b = true)
<VAR>a b : Bool<GOAL>((a && b) = true) = (a = true ∧ b = true)
<VAR>a b c : Bool<GOAL>(a && b && c) = (a && (b && c))
<VAR>a b c : Bool<GOAL>(a || b || c) = (a || (b || c))
<VAR>b : Bool<GOAL>(!b == true) = (b == false)
<VAR>b : Bool<GOAL>(!b == false) = (b == true)
<VAR>b : Bool<GOAL>((!b) = true) = (b = false)
<VAR>b : Bool<GOAL>((!b) = false) = (b = true)
<VAR>a b : Bool<GOAL>((a == b) = true) = (a = b)
<VAR>a b : Bool<GOAL>((!a == b) = true) = ¬a = b
<VAR>b : Bool<GOAL>(¬b = true) = (b = false)
<VAR>b : Bool<GOAL>(¬b = false) = (b = true)
<VAR>p : Prop<VAR>Decidable p<GOAL>(decide p = true) = p
<VAR>p : Prop<VAR>g : Decidable p<VAR>h : Decidable ¬p<GOAL>(decide ¬p) = !decide p
<VAR>p : Prop<VAR>h : Decidable p<GOAL>((!decide p) = true) = ¬p
<VAR>α : Sort u_1<VAR>a b : α<GOAL>HEq a b = (a = b)
<VAR>α : Type u_1<VAR>a b : α<GOAL>(bif true then a else b) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>(bif false then a else b) = b
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<GOAL>(a == a) = true
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>(a == a) = true
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<GOAL>(a != a) = false
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>(a != a) = false
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a != b) = true ↔ a ≠ b
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a == b) = false ↔ a ≠ b
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<GOAL>(a != b) = false ↔ a = b
<VAR>a : Nat<GOAL>(a ≤ 0) = (a = 0)
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ List.toArray l ↔ a ∈ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.drop 1 l = l.tail
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1}, (List.zipWith f l l').tail = List.zipWith f l.tail l'.tail
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] ⊆ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l ⊆ l
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<VAR>h₁ : l₁ ⊆ l₂<VAR>h₂ : l₂ ⊆ l₃<GOAL>l₁ ⊆ l₃
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l ⊆ a :: l
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ⊆ l₂ → l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁ ⊆ l₂ → l₁ ⊆ a :: l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>a : α<VAR>s : l₁ ⊆ l₂<GOAL>a :: l₁ ⊆ a :: l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ ⊆ l₁ ++ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₂ ⊆ l₁ ++ l₂
<VAR>α : Type u_1<VAR>l l₁ : List α<VAR>l₂ : List α<GOAL>l ⊆ l₁ → l ⊆ l₁ ++ l₂
<VAR>α : Type u_1<VAR>l l₂ : List α<VAR>l₁ : List α<GOAL>l ⊆ l₂ → l ⊆ l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {a : α} {l m : List α}, a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m
<VAR>α : Type u_1<VAR>l : List α<GOAL>l ⊆ [] ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → β<VAR>H : l₁ ⊆ l₂<GOAL>List.map f l₁ ⊆ List.map f l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] <+ l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <+ l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l <+ a :: l
<GOAL>∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a :: l₁ <+ l₂ → l₁ <+ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+ l₁ ++ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₂ <+ l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {l l₁ l₂ : List α}, l <+ l₁ → l <+ l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {l l₂ l₁ : List α}, l <+ l₂ → l <+ l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ (l : List α), l ++ l₁ <+ l ++ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ (l : List α), l₁ ++ l <+ l₂ ++ l
<GOAL>∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁ <+ l₂ → r₁ <+ r₂ → l₁ ++ r₁ <+ l₂ ++ r₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → l₁ ⊆ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.length ≤ l₂.length
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <+ [] ↔ l = []
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → l₁.length = l₂.length → l₁ = l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+ l₂ → l₂.length ≤ l₁.length → l₁ = l₂
<VAR>α : Type u_1<VAR>m n : Nat<VAR>a : α<GOAL>List.replicate m a <+ List.replicate n a ↔ m ≤ n
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>l₁ l₂ : List α<GOAL>l₁.isSublist l₂ = true ↔ l₁ <+ l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tail = l.tailD []
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(a :: l).next? = some (a, l)
<GOAL>∀ {α : Type u_1} {l : List α} {n : Fin l.length} {x : α}, l.get n = x ↔ l.get? ↑n = some x
<VAR>i : Nat<GOAL>∀ {α : Type u_1} {xs : List α} {j : Nat}, i < xs.length → xs.Nodup → xs[i]? = xs[j]? → i = j
<VAR>i : Nat<GOAL>∀ {α : Type u_1} {xs : List α} {j : Nat}, i < xs.length → xs.Nodup → xs.get? i = xs.get? j → i = j
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>(List.drop n l).tail = List.drop (n + 1) l
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<GOAL>List.modifyNth f n [] = []
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>l : List α<GOAL>List.modifyNth f 0 (a :: l) = f a :: l
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>l : List α<VAR>n : Nat<GOAL>List.modifyNth f (n + 1) (a :: l) = a :: List.modifyNth f n l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.modifyNthTail id n l = l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>l.eraseIdx n = List.modifyNthTail List.tail n l
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>m : Nat<GOAL>(List.modifyNth f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>m : Nat<GOAL>(List.modifyNth f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m
<VAR>α : Type u_1<VAR>f : List α → List α<VAR>H : ∀ (l : List α), (f l).length = l.length<VAR>n : Nat<VAR>l : List α<GOAL>(List.modifyNthTail f n l).length = l.length
<VAR>α : Type u_1<VAR>f : List α → List α<VAR>n : Nat<VAR>l₁ l₂ : List α<GOAL>List.modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂
<VAR>α : Type u_1<VAR>f : List α → List α<VAR>n : Nat<VAR>l : List α<VAR>h : n ≤ l.length<GOAL>∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ List.modifyNthTail f n l = l₁ ++ f l₂
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>(List.modifyNth f n l).length = l.length
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>(List.modifyNth f n l)[n]? = f <$> l[n]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>(List.modifyNth f n l).get? n = f <$> l.get? n
<VAR>α : Type u_1<VAR>f : α → α<VAR>m n : Nat<VAR>l : List α<VAR>h : m ≠ n<GOAL>(List.modifyNth f m l)[n]? = l[n]?
<VAR>α : Type u_1<VAR>f : α → α<VAR>m n : Nat<VAR>l : List α<VAR>h : m ≠ n<GOAL>(List.modifyNth f m l).get? n = l.get? n
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ List.modifyNth f n l = l₁ ++ f a :: l₂
<VAR>α : Type u_1<VAR>f : List α → List α<VAR>H : f [] = []<VAR>n : Nat<VAR>l : List α<GOAL>List.modifyNthTail f n l = List.take n l ++ f (List.drop n l)
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>List.modifyNth f n l = List.take n l ++ List.modifyHead f (List.drop n l)
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>List.modifyNth f n l = List.take n l ++ f l[n] :: List.drop (n + 1) l
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<GOAL>l.set n a = List.modifyNth (fun x => a) n l
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>l.set n a = List.take n l ++ a :: List.drop (n + 1) l
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<GOAL>List.modifyNth f n l = ((fun a => l.set n (f a)) <$> l.get? n).getD l
<VAR>α : Type u_1<VAR>f : α → α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>List.modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))
<VAR>α : Type u_1<VAR>n : Nat<VAR>a' : α<VAR>l : List α<VAR>h : n < l.length<GOAL>∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂
<VAR>α : Type u_1<VAR>n : Nat<VAR>a' : α<VAR>l : List α<VAR>h : n < l.length<GOAL>∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<GOAL>(l.set n a).get? n = (fun x => a) <$> l.get? n
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<VAR>l : List α<VAR>h : m ≠ n<GOAL>(l.set m a).get? n = l.get? n
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<VAR>l : List α<GOAL>(l.set m a)[n]? = if m = n then (fun x => a) <$> l[n]? else l[n]?
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<VAR>l : List α<VAR>h : m < l.length<GOAL>(l.set m a).get? n = if m = n then some a else l.get? n
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>l : List α<VAR>h : n < m<GOAL>List.drop m (l.set n a) = List.drop m l
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>l : List α<VAR>h : m < n<GOAL>List.take m (l.set n a) = List.take m l
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<GOAL>i < l.length → (l.eraseIdx i).length = l.length - 1
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tail.length = l.length - 1
<GOAL>∀ {α : Type u_1} {p : α → Bool}, List.eraseP p [] = []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<GOAL>List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>p : α → Bool<VAR>h : p a = true<GOAL>List.eraseP p (a :: l) = l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>p : α → Bool<VAR>h : ¬p a = true<GOAL>List.eraseP p (a :: l) = a :: List.eraseP p l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → ¬p a = true<GOAL>List.eraseP p l = l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>a : α<VAR>al : a ∈ l<VAR>pa : p a = true<GOAL>∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.eraseP p l = l ∨ ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂
<GOAL>∀ {α : Type u_1} {a : α} {l : List α} {p : α → Bool}, a ∈ l → p a = true → (List.eraseP p l).length = l.length.pred
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>pa : p a = true<VAR>l₁ : List α<VAR>l₂ : List α<GOAL>a ∈ l₁ → List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ : List α<VAR>l₂ : List α<GOAL>(∀ (b : α), b ∈ l₁ → ¬p b = true) → List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.eraseP p l <+ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.eraseP p l ⊆ l
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁ <+ l₂ → List.eraseP p l₁ <+ List.eraseP p l₂
<VAR>α : Type u_1<VAR>a : α<VAR>p : α → Bool<VAR>l : List α<GOAL>a ∈ List.eraseP p l → a ∈ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>pa : ¬p a = true<GOAL>a ∈ List.eraseP p l ↔ a ∈ l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>p : α → Bool<VAR>f : β → α<VAR>l : List β<GOAL>List.eraseP p (List.map f l) = List.map f (List.eraseP (p ∘ f) l)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.extractP p l = (List.find? p l, List.eraseP p l)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>acc : Array α<VAR>xs : List α<GOAL>l = acc.data ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs)
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>l : List α<GOAL>l.erase a = List.eraseP (fun x => x == a) l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<GOAL>l.erase a = List.eraseP (fun x => a == x) l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(l.erase a).length = l.length.pred
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>LawfulBEq α<VAR>l₁ : List α<VAR>l₂ : List α<VAR>h : a ∈ l₁<GOAL>(l₁ ++ l₂).erase a = l₁.erase a ++ l₂
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l₁ : List α<VAR>l₂ : List α<VAR>h : ¬a ∈ l₁<GOAL>(l₁ ++ l₂).erase a = l₁ ++ l₂.erase a
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>l : List α<GOAL>l.erase a <+ l
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>l : List α<GOAL>l.erase a ⊆ l
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+ l₂<GOAL>l₁.erase a <+ l₂.erase a
<VAR>α : Type u_1<VAR>BEq α<VAR>a b : α<VAR>l : List α<VAR>h : a ∈ l.erase b<GOAL>a ∈ l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>ab : a ≠ b<GOAL>a ∈ l.erase b ↔ a ∈ l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>l : List α<GOAL>(l.erase a).erase b = (l.erase b).erase a
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.filter p l <+ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → Option β<VAR>s : l₁ <+ l₂<GOAL>List.filterMap f l₁ <+ List.filterMap f l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<GOAL>List.filter p l₁ <+ List.filter p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<GOAL>List.findIdx p [] = 0
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : Nat<GOAL>List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>b : α<VAR>l : List α<GOAL>List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>y : α<VAR>xs : List α<VAR>w : xs.get? (List.findIdx p xs) = some y<GOAL>p y = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>xs : List α<VAR>w : List.findIdx p xs < xs.length<GOAL>p (xs.get ⟨List.findIdx p xs, w⟩) = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>xs : List α<VAR>h : ∃ x, x ∈ xs ∧ p x = true<GOAL>List.findIdx p xs < xs.length
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>xs : List α<VAR>h : ∃ x, x ∈ xs ∧ p x = true<GOAL>xs.get? (List.findIdx p xs) = some (xs.get ⟨List.findIdx p xs, ⋯⟩)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>i : Nat<GOAL>List.findIdx? p [] i = none
<GOAL>∀ {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} {i : Nat}, List.findIdx? p (x :: xs) i = if p x = true then some i else List.findIdx? p xs (i + 1)
<VAR>α : Type u_1<VAR>xs : List α<VAR>p : α → Bool<VAR>i : Nat<GOAL>List.findIdx? p xs (i + 1) = Option.map (fun i => i + 1) (List.findIdx? p xs i)
<VAR>α : Type u_1<VAR>i : Nat<VAR>xs : List α<VAR>p : α → Bool<GOAL>List.findIdx? p xs = some i ↔ List.map p (List.take (i + 1) xs) = List.replicate i false ++ [true]
<VAR>α : Type u_1<VAR>i : Nat<VAR>xs : List α<VAR>p : α → Bool<VAR>w : List.findIdx? p xs = some i<GOAL>match xs.get? i with
<VAR>α : Type u_1<VAR>xs : List α<VAR>p : α → Bool<VAR>w : List.findIdx? p xs = none<VAR>i : Nat<GOAL>match xs.get? i with
<VAR>α : Type u_1<VAR>xs ys : List α<VAR>p : α → Bool<GOAL>List.findIdx? p (xs ++ ys) = HOrElse.hOrElse (List.findIdx? p xs) fun x => Option.map (fun i => i + xs.length) (List.findIdx? p ys)
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {p : α → Bool}, List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, l₁ <+ l₂ → List.Pairwise R l₂ → List.Pairwise R l₁
<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_2} {f : α → α_1} {R : α_1 → α_1 → Prop} {l : List α}, List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<GOAL>List.Pairwise R (l₁ ++ l₂) ↔ List.Pairwise R l₁ ∧ List.Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l.reverse ↔ List.Pairwise (fun a b => R b a) l
<VAR>α : Type u_1<VAR>R S : α → α → Prop<VAR>H : ∀ {a b : α}, R a b → S a b<VAR>l : List α<GOAL>List.Pairwise R l → List.Pairwise S l
<GOAL>∀ {α : Type u_1} {p : α → Option α}, List.replaceF p [] = []
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>a : α<VAR>l : List α<GOAL>List.replaceF p (a :: l) = match p a with | none => a :: List.replaceF p l | some a' => a' :: l
<VAR>α : Type u_1<VAR>a' a : α<VAR>l : List α<VAR>p : α → Option α<VAR>h : p a = some a'<GOAL>List.replaceF p (a :: l) = a' :: l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>p : α → Option α<VAR>h : p a = none<GOAL>List.replaceF p (a :: l) = a :: List.replaceF p l
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a = none<GOAL>List.replaceF p l = l
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<VAR>a a' : α<VAR>al : a ∈ l<VAR>pa : p a = some a'<GOAL>∃ a a' l₁ l₂, (∀ (b : α), b ∈ l₁ → p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>l : List α<GOAL>List.replaceF p l = l ∨ ∃ a a' l₁ l₂, (∀ (b : α), b ∈ l₁ → p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂
<GOAL>∀ {α : Type u_1} {f : α → Option α} {l : List α}, (List.replaceF f l).length = l.length
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ → l₂.Disjoint l₁
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ l₂.Disjoint l₁
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₁ → ¬a ∈ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₂ → ¬a ∈ l₁
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → a ≠ b
<GOAL>∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ ⊆ l → l.Disjoint l₂ → l₁.Disjoint l₂