ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type → Type u_1<VAR>α : Type u_2<VAR>Monad m<VAR>LawfulMonad m<VAR>p : α → m Bool<VAR>as : Array α<VAR>start stop : Nat<VAR>q : Fin as.size → Prop<VAR>hp : ∀ (i : Fin as.size), start ≤ ↑i → ↑i < stop → SatisfiesM (fun x => x = true ↔ q i) (p as[i])<GOAL>SatisfiesM (fun res => res = true ↔ ∃ i, start ≤ ↑i ∧ ↑i < stop ∧ q i) (Array.anyM p as start stop)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>init : β<VAR>h0 : motive as.size init<VAR>f : α → β → m β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)<GOAL>SatisfiesM (motive 0) (Array.foldrM f init as as.size)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>motive : Nat → β → Prop<VAR>f : α → β → m β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)<VAR>i : Nat<VAR>b : β<VAR>hi : i ≤ as.size<VAR>H : motive i b<GOAL>SatisfiesM (motive 0) (Array.foldrM.fold f as 0 i hi b)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>f : Fin as.size → α → m β<VAR>motive : Nat → Prop<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f i as[i])<VAR>bs : Array β<VAR>i j : Nat<VAR>h : i + j = as.size<VAR>h₁ : j = bs.size<VAR>h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p ⟨i, h⟩ bs[i]<VAR>hm : motive j<GOAL>SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p ⟨i_1, h⟩ arr[i_1]) (Array.mapIdxM.map as f i j h bs)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>as : Array α<VAR>f : Fin as.size → α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f i as[i])<GOAL>SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (as.mapIdxM f)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>Monad m<VAR>LawfulMonad m<VAR>a : Array α<VAR>i : Nat<VAR>f : α → m α<GOAL>SatisfiesM (fun x => x.size = a.size) (a.modifyM i f)
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<GOAL>(a :: as).tail = as
<VAR>α : Type u_1<VAR>p : α → Option α<VAR>acc : Array α<VAR>xs : List α<GOAL>List.replaceFTR.go p xs acc = acc.data ++ List.replaceF p xs
<VAR>α : Type u_1<VAR>f : α → α<GOAL>List.modifyHead f [] = []
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>f : α → α<GOAL>List.modifyHead f (a :: l) = f a :: l
<GOAL>∀ {α : Type u_1} {f : α → α} {acc : Array α} (l : List α) (n : Nat), List.modifyNthTR.go f l n acc = acc.data ++ List.modifyNth f n l
<GOAL>@List.modifyNth = @List.modifyNthTR
<GOAL>∀ {α : Type u_1} {a : α} {acc : Array α} (n : Nat) (l : List α), List.insertNthTR.go a n l acc = acc.data ++ List.insertNth n a l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>l.headD a = l.head?.getD a
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>List.takeD 0 l a = []
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>a : α<GOAL>List.takeD (n + 1) l a = l.head?.getD a :: List.takeD n l.tail a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>List.takeD n [] a = List.replicate n a
<GOAL>∀ {α : Type u_1} {dflt : α} {acc : Array α} (n : Nat) (l : List α), List.takeDTR.go dflt n l acc = acc.data ++ List.takeD n l dflt
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α} {a : α} {acc : Array α} (l : List α_1), List.scanlTR.go f l a acc = acc.data ++ List.scanl f a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.Forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ List.Forall₂ R l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Bool<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>List.all₂ r l₁ l₂ = true ↔ List.Forall₂ (fun x x_1 => r x x_1 = true) l₁ l₂
<VAR>α : Type u_1<VAR>L : List (List α)<GOAL>L.any List.isEmpty = true → L.sections = []
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>acc : Array α<VAR>xs : List α<GOAL>l = acc.data ++ xs → List.erasePTR.go p l xs acc = acc.data ++ List.eraseP p xs
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : Fin n → α<VAR>i j : Nat<VAR>h : i + j = n<VAR>h' : j ≤ n<GOAL>List.ofFnTR.go f j h' (List.ofFn.go f i j h) = List.ofFn f
<GOAL>@List.takeWhile₂ = @List.takeWhile₂TR
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>R : α → β → Bool<VAR>as : List α<VAR>bs : List β<VAR>acca : List α<VAR>accb : List β<GOAL>List.takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ (List.takeWhile₂ R as bs).fst, accb.reverse ++ (List.takeWhile₂ R as bs).snd)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>a : α<VAR>l : List α<GOAL>List.Pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ List.Pairwise R l
<VAR>step : Nat := 1<VAR>s n m : Nat<GOAL>List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.dropSlice n 0 l = l
<VAR>α : Type u_1<VAR>l : List α<VAR>m : Nat<VAR>acc : Array α<VAR>xs : List α<VAR>n : Nat<GOAL>l = acc.data ++ xs → List.dropSliceTR.go l m xs n acc = acc.data ++ List.dropSlice n (m + 1) xs
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>acc : Array γ<VAR>as : List α<VAR>bs : List β<GOAL>List.zipWithLeft'TR.go f as bs acc = match List.zipWithLeft' f as bs with | (l, r) => (acc.toList ++ l, r)
<VAR>α : Type u_3<VAR>β : Type u_2<VAR>γ : Type u_1<VAR>f : α → Option β → γ<VAR>acc : Array γ<VAR>as : List α<VAR>bs : List β<GOAL>List.zipWithLeftTR.go f as bs acc = acc.toList ++ List.zipWithLeft f as bs
<VAR>α : Type u_1<VAR>acc : Array α<VAR>as : List (Option α)<VAR>as' : List α<GOAL>List.fillNonesTR.go as as' acc = acc.data ++ as.fillNones as'
<VAR>α : Type u_1<VAR>acc : Array (List α)<VAR>ns : List Nat<VAR>xs : List α<GOAL>List.takeListTR.go ns xs acc = match xs.takeList ns with | (l, r) => (acc.toList ++ l, r)
<VAR>p q : Rat<GOAL>p.num = q.num → p.den = q.den → p = q
<VAR>r : Int<GOAL>{ num := r, den := 1, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<GOAL>Rat.maybeNormalize num den g den_nz reduced = { num := num.div ↑g, den := den / g, den_nz := den_nz, reduced := reduced }
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den ≠ 0<VAR>e : g = num.natAbs.gcd den<GOAL>(num / ↑g).natAbs.Coprime (den / g)
<VAR>num : Int<VAR>den : Nat<VAR>den_nz : den ≠ 0<GOAL>Rat.normalize num den den_nz = { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }
<VAR>d : Nat<VAR>nz : d ≠ 0<GOAL>Rat.normalize 0 d nz = 0
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<VAR>c : num.natAbs.Coprime den<GOAL>{ num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz
<VAR>r : Rat<GOAL>Rat.normalize r.num r.den ⋯ = r
<VAR>d : Nat<VAR>n : Int<VAR>a : Nat<VAR>d0 : d ≠ 0<VAR>a0 : a ≠ 0<GOAL>Rat.normalize (↑a * n) (a * d) ⋯ = Rat.normalize n d d0
<VAR>d : Nat<VAR>n : Int<VAR>a : Nat<VAR>d0 : d ≠ 0<VAR>a0 : a ≠ 0<GOAL>Rat.normalize (n * ↑a) (d * a) ⋯ = Rat.normalize n d d0
<VAR>d₁ d₂ : Nat<VAR>n₁ n₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>Rat.normalize n₁ d₁ z₁ = Rat.normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<GOAL>Rat.maybeNormalize num den g den_nz reduced = Rat.normalize num den ⋯
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<GOAL>Rat.normalize n d d0 = 0 ↔ n = 0
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<GOAL>∃ d, d ≠ 0 ∧ num = (Rat.normalize num den nz).num * ↑d ∧ den = (Rat.normalize num den nz).den * d
<VAR>n : Int<VAR>d : Nat<VAR>z : d ≠ 0<VAR>n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>h : Rat.normalize n d z = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
<VAR>num : Int<VAR>den : Nat<VAR>den_nz : den ≠ 0<GOAL>Rat.normalize num den den_nz = mkRat num den
<VAR>d : Nat<VAR>n n' : Int<VAR>d' : Nat<VAR>z' : d' ≠ 0<VAR>c : n'.natAbs.Coprime d'<VAR>z : d ≠ 0<VAR>h : mkRat n d = { num := n', den := d', den_nz := z', reduced := c }<GOAL>∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
<VAR>n : Int<VAR>d : Nat<GOAL>mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0
<VAR>d : Nat<VAR>n : Int<VAR>d0 : d ≠ 0<GOAL>mkRat n d ≠ 0 ↔ n ≠ 0
<VAR>n : Nat<GOAL>Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n
<VAR>n : Int<GOAL>(Rat.ofInt n).num = n
<VAR>n : Int<GOAL>(Rat.ofInt n).den = 1
<VAR>n : Nat<GOAL>Rat.num (OfNat.ofNat n) = OfNat.ofNat n
<VAR>n : Nat<GOAL>Rat.den (OfNat.ofNat n) = 1
<VAR>a b : Rat<GOAL>a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>Rat.normalize n₁ d₁ z₁ + Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂)
<VAR>a : Rat<GOAL>(-a).num = -a.num
<VAR>n : Int<VAR>d : Nat<VAR>z : d ≠ 0<GOAL>-Rat.normalize n d z = Rat.normalize (-n) d z
<VAR>a b : Rat<GOAL>a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯
<VAR>a b : Rat<GOAL>a - b = a + -b
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ - n₂ /. d₂ = (n₁ * d₂ - n₂ * d₁) /. (d₁ * d₂)
<VAR>a b : Rat<GOAL>a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>Rat.normalize n₁ d₁ z₁ * Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * n₂) (d₁ * d₂) ⋯
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Int<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)
<VAR>a : Rat<GOAL>a.inv = ↑a.den /. a.num
<VAR>a b : Rat<GOAL>a / b = a * b.inv
<VAR>m e : Nat<GOAL>Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)
<VAR>m e : Nat<GOAL>Rat.ofScientific m false e = ↑(m * 10 ^ e)
<VAR>m : Nat<VAR>s : Bool<VAR>e : Nat<GOAL>Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)
<VAR>a b : Int<GOAL>↑a = ↑b ↔ a = b
<VAR>a : Int<GOAL>↑(-a) = -↑a
<VAR>α : Type u_1<VAR>l : List α<GOAL>l ~ l
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ = l₂ → l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ ~ l₂<GOAL>l₂ ~ l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ ~ l₂ ↔ l₂ ~ l₁
<VAR>α : Type u_1<VAR>x y : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>y :: x :: l₁ ~ x :: y :: l₂
<VAR>α : Type u_1<VAR>motive : (l₁ l₂ : List α) → l₁ ~ l₂ → Prop<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>nil : motive [] [] ⋯<VAR>cons : ∀ (x : α) {l₁ l₂ : List α} (h : l₁ ~ l₂), motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) ⋯<VAR>swap' : ∀ (x y : α) {l₁ l₂ : List α} (h : l₁ ~ l₂), motive l₁ l₂ h → motive (y :: x :: l₁) (x :: y :: l₂) ⋯<VAR>trans : ∀ {l₁ l₂ l₃ : List α} (h₁ : l₁ ~ l₂) (h₂ : l₂ ~ l₃), motive l₁ l₂ h₁ → motive l₂ l₃ h₂ → motive l₁ l₃ ⋯<GOAL>motive l₁ l₂ p
<VAR>α : Type u_1<GOAL>Equivalence List.Perm
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>t₁ : List α<VAR>p : l₁ ~ l₂<GOAL>l₁ ++ t₁ ~ l₂ ++ t₁
<VAR>α : Type u_1<VAR>t₁ t₂ : List α<VAR>l : List α<GOAL>t₁ ~ t₂ → l ++ t₁ ~ l ++ t₂
<VAR>α : Type u_1<VAR>l₁ l₂ t₁ t₂ : List α<VAR>p₁ : l₁ ~ l₂<VAR>p₂ : t₁ ~ t₂<GOAL>l₁ ++ t₁ ~ l₂ ++ t₂
<VAR>α : Type u_1<VAR>a : α<VAR>h₁ h₂ t₁ t₂ : List α<VAR>p₁ : h₁ ~ h₂<VAR>p₂ : t₁ ~ t₂<GOAL>h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l ++ [a] ~ a :: l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ ++ l₂ ~ l₂ ++ l₁
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>l.concat a ~ a :: l
<VAR>α : Type u_1<VAR>l : List α<VAR>p : l ~ []<GOAL>l = []
<VAR>α : Type u_1<VAR>l : List α<VAR>p : [] ~ l<GOAL>[] = l
<VAR>α : Type u_1<VAR>l₁ : List α<GOAL>l₁ ~ [] ↔ l₁ = []
<VAR>α : Type u_1<VAR>l₁ : List α<GOAL>[] ~ l₁ ↔ l₁ = []
<VAR>α : Type u_1<VAR>x : α<VAR>l : List α<GOAL>¬[] ~ x :: l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse ~ l
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>p : l ~ l₁ ++ l₂<GOAL>a :: l ~ l₁ ++ a :: l₂
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>l ~ List.replicate n a ↔ l = List.replicate n a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>List.replicate n a ~ l ↔ List.replicate n a = l
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l ~ [a] ↔ l = [a]
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>[a] ~ l ↔ [a] = l
<VAR>α : Type u_1<VAR>a b : α<GOAL>[a] ~ [b] ↔ a = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>l ~ a :: l.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>List.filterMap f l₁ ~ List.filterMap f l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>List.map f l₁ ~ List.map f l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l₁ l₂ : List α<GOAL>l₁ ~ l₂ → ∀ {H₁ : ∀ (a : α), a ∈ l₁ → p a} {H₂ : ∀ (a : α), a ∈ l₂ → p a}, List.pmap f l₁ H₁ ~ List.pmap f l₂ H₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.filter p l ++ List.filter (fun x => !p x) l ~ l
<VAR>α : Type u_1<VAR>SizeOf α<VAR>l₁ l₂ : List α<VAR>h : l₁ ~ l₂<GOAL>sizeOf l₁ = sizeOf l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>[] <+~ l
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>l <+~ l₁ ↔ l <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<VAR>p : l₁ ~ l₂<GOAL>l₁ <+~ l ↔ l₂ <+~ l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<GOAL>l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l : List α<GOAL>l <+~ l
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<VAR>s₁₂ : l₁ <+~ l₂<VAR>s₂₃ : l₂ <+~ l₃<GOAL>l₁ <+~ l₃
<VAR>α : Type u_1<VAR>l l' : List α<VAR>x : α<VAR>h : l <+~ l'<GOAL>l <+~ x :: l'
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ → l₁.length ≤ l₂.length
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ → l₂.length ≤ l₁.length → l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h₁ : l₁ <+~ l₂<VAR>h₂ : l₂ <+~ l₁<GOAL>l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ → l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l l' : List α<VAR>h : l <+~ l'<GOAL>List.filter p l <+~ List.filter p l'
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ <+ l₂ → ∃ l, l₂ ~ l₁ ++ l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<GOAL>List.countP p l₁ = List.countP p l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ → List.countP p l₁ ≤ List.countP p l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>s : l₁ ~ l₂<VAR>p p' : α → Bool<VAR>hp : ∀ (x : α), x ∈ l₁ → p x = p' x<GOAL>List.countP p l₁ = List.countP p' l₂
<VAR>α : Type u_1<VAR>l : List α<VAR>p q : α → Bool<GOAL>List.countP p l = List.countP p (List.filter q l) + List.countP p (List.filter (fun a => !q a) l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>a : α<GOAL>List.count a l₁ = List.count a l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>s : l₁ <+~ l₂<VAR>a : α<GOAL>List.count a l₁ ≤ List.count a l₂
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>f : β → α → β<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<VAR>comm : ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : β), f (f z x) y = f (f z y) x<VAR>init : β<GOAL>List.foldl f init l₁ = List.foldl f init l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ r₁ r₂ : List α<GOAL>l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ~ a :: l₂ → l₁ ~ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>l : List α<GOAL>l ++ l₁ ~ l ++ l₂ ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>l : List α<GOAL>l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ <+~ a :: l₂ ↔ l₁ <+~ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h₁ : ¬a ∈ l₁<VAR>h₂ : a ∈ l₂<VAR>s : l₁ <+~ l₂<GOAL>a :: l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>l : List α<GOAL>l ++ l₁ <+~ l ++ l₂ ↔ l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>l : List α<GOAL>l₁ ++ l <+~ l₂ ++ l ↔ l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>s : l₁ <+~ l₂<VAR>h : l₁.length < l₂.length<GOAL>∃ a, a :: l₁ <+~ l₂
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₁ ⊆ l₂ → l₁ <+~ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<VAR>d : l.Nodup<VAR>s₁ : l₁ <+ l<VAR>s₂ : l₂ <+ l<GOAL>l₁ ~ l₂ ↔ l₁ = l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>l₁.erase a ~ l₂.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l <+~ a :: l.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>l.erase a <+~ l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>a : α<VAR>h : l₁ <+~ l₂<GOAL>l₁.erase a <+~ l₂.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>t : List α<VAR>h : l₁ ~ l₂<GOAL>l₁.diff t ~ l₂.diff t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>t₁ t₂ : List α<VAR>h : t₁ ~ t₂<GOAL>l.diff t₁ = l.diff t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ t₁ t₂ : List α<VAR>hl : l₁ ~ l₂<VAR>ht : t₁ ~ t₂<GOAL>l₁.diff t₁ ~ l₂.diff t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+~ l₂<VAR>t : List α<GOAL>l₁.diff t <+~ l₂.diff t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>l : List α<GOAL>(a :: l).erase b <+~ a :: l.erase b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁).diff l₂ ⊆ a :: l₁.diff l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ ~ l₂ ↔ ∀ (a : α), List.count a l₁ = List.count a l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂<GOAL>l₁ ++ l₂.diff l₁ ~ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → List.count x l₁ ≤ List.count x l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.isSubperm l₂ = true ↔ l₁ <+~ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>h : l₁ <+~ l₂<VAR>x : α<VAR>hx : List.count x l₁ < List.count x l₂<GOAL>x :: l₁ <+~ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<GOAL>l₁.isPerm l₂ = true ↔ l₁ ~ l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>p : l₁ ~ l₂<GOAL>List.insert a l₁ ~ List.insert a l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x y : α<VAR>l : List α<GOAL>List.insert x (List.insert y l) ~ List.insert y (List.insert x l)
<VAR>α : Type u_1<VAR>x : α<VAR>l : List α<VAR>n : Nat<VAR>h : n ≤ l.length<GOAL>List.insertNth n x l ~ x :: l
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>t₁ : List α<VAR>h : l₁ ~ l₂<GOAL>l₁ ∪ t₁ ~ l₂ ∪ t₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>t₁ t₂ : List α<VAR>h : t₁ ~ t₂<GOAL>l ∪ t₁ ~ l ∪ t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ t₁ t₂ : List α<VAR>p₁ : l₁ ~ l₂<VAR>p₂ : t₁ ~ t₂<GOAL>l₁ ∪ t₁ ~ l₂ ∪ t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>t₁ : List α<GOAL>l₁ ~ l₂ → l₁ ∩ t₁ ~ l₂ ∩ t₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>t₁ t₂ : List α<VAR>p : t₁ ~ t₂<GOAL>l ∩ t₁ = l ∩ t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ t₁ t₂ : List α<VAR>p₁ : l₁ ~ l₂<VAR>p₂ : t₁ ~ t₂<GOAL>l₁ ∩ t₁ ~ l₂ ∩ t₂
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>S : ∀ {x y : α}, R x y → R y x<VAR>l₁ l₂ : List α<VAR>_p : l₁ ~ l₂<GOAL>List.Pairwise R l₁ ↔ List.Pairwise R l₂
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l l' : List α<VAR>hR : List.Pairwise R l<VAR>hl : l ~ l'<VAR>hsymm : ∀ {x y : α}, R x y → R y x<GOAL>List.Pairwise R l'
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l l' : List α<VAR>hl : l ~ l'<VAR>hR : List.Pairwise R l<VAR>hsymm : ∀ {x y : α}, R x y → R y x<GOAL>List.Pairwise R l'
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁ ~ l₂ → (l₁.Nodup ↔ l₂.Nodup)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>f : α → List β<VAR>p : l₁ ~ l₂<GOAL>l₁.bind f ~ l₂.bind f
<VAR>α : Type u_1<VAR>l₁ l₂ : List (List α)<GOAL>List.Forall₂ (fun x x_1 => x ~ x_1) l₁ l₂ → l₁.join ~ l₂.join
<VAR>α : Type u_1<VAR>f : α → Bool<VAR>l₁ l₂ : List α<VAR>H : List.Pairwise (fun a b => f a = true → f b = true → False) l₁<VAR>p : l₁ ~ l₂<GOAL>List.eraseP f l₁ ~ List.eraseP f l₂
<VAR>α : Type u_1<VAR>s : α → α → Bool<VAR>l r : List α<GOAL>List.merge s l r ~ l ++ r
<VAR>α : Type u_1<VAR>l₁ l₂ r₁ r₂ : List α<VAR>s₁ s₂ : α → α → Bool<VAR>hl : l₁ ~ l₂<VAR>hr : r₁ ~ r₂<GOAL>List.merge s₁ l₁ r₁ ~ List.merge s₂ l₂ r₂
<VAR>self : IncidenceGeometry<VAR>α β : IncidenceGeometry.Circle<GOAL>IncidenceGeometry.circlesInter α β → ∃ a b, a ≠ b ∧ IncidenceGeometry.onCircle a α ∧ IncidenceGeometry.onCircle a β ∧ IncidenceGeometry.onCircle b α ∧ IncidenceGeometry.onCircle b β
<VAR>self : IncidenceGeometry<VAR>a b c : IncidenceGeometry.Point<VAR>L : IncidenceGeometry.Line<GOAL>IncidenceGeometry.between a b c → IncidenceGeometry.onLine a L → IncidenceGeometry.onLine c L → IncidenceGeometry.onLine b L
<VAR>self : IncidenceGeometry<VAR>a b : IncidenceGeometry.Point<VAR>L M : IncidenceGeometry.Line<GOAL>a ≠ b → IncidenceGeometry.onLine a L → IncidenceGeometry.onLine b L → IncidenceGeometry.onLine a M → IncidenceGeometry.onLine b M → L = M
<VAR>self : IncidenceGeometry<VAR>a b : IncidenceGeometry.Point<VAR>α β : IncidenceGeometry.Circle<GOAL>IncidenceGeometry.onCircle b α → IncidenceGeometry.onCircle a β → IncidenceGeometry.inCircle a α → IncidenceGeometry.inCircle b β → IncidenceGeometry.circlesInter α β
<VAR>self : IncidenceGeometry<VAR>a b c : IncidenceGeometry.Point<GOAL>IncidenceGeometry.between a b c → b ≠ c
<VAR>self : IncidenceGeometry<VAR>a : IncidenceGeometry.Point<VAR>α : IncidenceGeometry.Circle<GOAL>IncidenceGeometry.centerCircle a α → IncidenceGeometry.inCircle a α
<VAR>self : IncidenceGeometry<VAR>a b : IncidenceGeometry.Point<GOAL>∃ L, IncidenceGeometry.onLine a L ∧ IncidenceGeometry.onLine b L
<VAR>self : IncidenceGeometry<VAR>a b : IncidenceGeometry.Point<GOAL>a ≠ b → ∃ C, IncidenceGeometry.centerCircle a C ∧ IncidenceGeometry.onCircle b C
<VAR>ε : Type u<VAR>α : Type u_1<GOAL>Except.map id = id
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>β : Type u<VAR>a : α<VAR>s : σ<VAR>k : α → σ → m β<GOAL>(pure a).runK s k = k a s
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β : Type u<VAR>s : σ<VAR>k : σ → σ → m β<GOAL>get.runK s k = k s s
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β : Type u<VAR>s s' : σ<VAR>k : PUnit → σ → m β<GOAL>(set s').runK s k = k PUnit.unit s'
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β : Type u<VAR>f : σ → σ<VAR>s : σ<VAR>k : PUnit → σ → m β<GOAL>(modify f).runK s k = k PUnit.unit (f s)
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>β : Type u<VAR>Monad m<VAR>x : m α<VAR>s : σ<VAR>k : α → σ → m β<GOAL>(StateCpsT.lift x).runK s k = do let x ← x k x s
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>n : Type u → Type u_1<VAR>β : Type u<VAR>Monad m<VAR>MonadLiftT n m<VAR>x : n α<VAR>s : σ<VAR>k : α → σ → m β<GOAL>(monadLift x).runK s k = do let x ← monadLift x k x s
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>β γ : Type u<VAR>a : α<VAR>f : α → StateCpsT σ m β<VAR>s : σ<VAR>k : β → σ → m γ<GOAL>(pure a >>= f).runK s k = (f a).runK s k
<VAR>α σ : Type u<VAR>m : Type u → Type v<VAR>β γ : Type u<VAR>Monad m<VAR>x : m α<VAR>f : α → StateCpsT σ m β<VAR>s : σ<VAR>k : β → σ → m γ<GOAL>(StateCpsT.lift x >>= f).runK s k = do let a ← x (f a).runK s k
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β γ : Type u<VAR>f : σ → StateCpsT σ m β<VAR>s : σ<VAR>k : β → σ → m γ<GOAL>(get >>= f).runK s k = (f s).runK s k
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β γ : Type u<VAR>f : PUnit → StateCpsT σ m β<VAR>s s' : σ<VAR>k : β → σ → m γ<GOAL>(set s' >>= f).runK s k = (f PUnit.unit).runK s' k
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>β γ : Type u<VAR>f : σ → σ<VAR>g : PUnit → StateCpsT σ m β<VAR>s : σ<VAR>k : β → σ → m γ<GOAL>(modify f >>= g).runK s k = (g PUnit.unit).runK (f s) k