ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>K L : List α<VAR>f : ℕ → α → β<GOAL>List.mapIdx f (K ++ L) = List.mapIdx f K ++ List.mapIdx (fun i a => f (i + K.length) a) L
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<GOAL>(List.mapIdx f l).length = l.length
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<GOAL>List.mapIdx f l = [] ↔ l = []
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<VAR>i : ℕ<VAR>h : i < l.length<VAR>h' : i < (List.mapIdx f l).length := ⋯<GOAL>(List.mapIdx f l).nthLe i h' = f i (l.nthLe i h)
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<GOAL>List.mapIdx f l = List.ofFn fun i => f (↑i) (l.get i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → β<VAR>b : β<VAR>a : α<VAR>as : List α<VAR>start : ℕ<GOAL>List.foldrIdxSpec f b (a :: as) start = f start a (List.foldrIdxSpec f b as (start + 1))
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → β<VAR>b : β<VAR>as : List α<VAR>start : ℕ<GOAL>List.foldrIdx f b as start = List.foldrIdxSpec f b as start
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → β<VAR>b : β<VAR>as : List α<GOAL>List.foldrIdx f b as = List.foldr (Function.uncurry f) b as.enum
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>as : List α<GOAL>List.indexesValues (fun b => decide (p b)) as = List.filter ((fun b => decide (p b)) ∘ Prod.snd) as.enum
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>as : List α<GOAL>List.findIdxs (fun b => decide (p b)) as = List.map Prod.fst (List.indexesValues (fun b => decide (p b)) as)
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<GOAL>List.findIdx p xs = xs.length ↔ ∀ x ∈ xs, ¬p x = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<GOAL>List.findIdx p xs ≤ xs.length
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<GOAL>List.findIdx p xs < xs.length ↔ ∃ x ∈ xs, p x = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < List.findIdx p xs<GOAL>¬p (xs.get ⟨i, ⋯⟩) = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>i ≤ List.findIdx p xs
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<VAR>h2 : ∀ (j : ℕ) (hji : j ≤ i), ¬p (xs.get ⟨j, ⋯⟩) = true<GOAL>i < List.findIdx p xs
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>i : ℕ<VAR>h : i < xs.length<GOAL>List.findIdx p xs = i ↔ p (xs.get ⟨i, h⟩) = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p (xs.get ⟨j, ⋯⟩) = true
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → α<VAR>a : α<VAR>b : β<VAR>bs : List β<VAR>start : ℕ<GOAL>List.foldlIdxSpec f a (b :: bs) start = List.foldlIdxSpec f (f start a b) bs (start + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → α<VAR>a : α<VAR>bs : List β<VAR>start : ℕ<GOAL>List.foldlIdx f a bs start = List.foldlIdxSpec f a bs start
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β → α<VAR>a : α<VAR>bs : List β<GOAL>List.foldlIdx f a bs = List.foldl (fun a p => f p.1 a p.2) a bs.enum
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>β : Type u<VAR>f : ℕ → α → β → m β<VAR>b : β<VAR>as : List α<VAR>LawfulMonad m<GOAL>List.foldrIdxM f b as = List.foldrM (Function.uncurry f) b as.enum
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>β : Type u<VAR>f : ℕ → β → α → m β<VAR>b : β<VAR>as : List α<GOAL>List.foldlIdxM f b as = List.foldlM (fun b p => f p.1 b p.2) b as.enum
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>β : Type u<VAR>f : ℕ → α → m β<VAR>start : ℕ<VAR>a : α<VAR>as : List α<GOAL>List.mapIdxMAuxSpec f start (a :: as) = Seq.seq (List.cons <$> f start a) fun x => List.mapIdxMAuxSpec f (start + 1) as
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>β : Type u<VAR>f : ℕ → α → m β<VAR>arr : Array β<VAR>as : List α<GOAL>List.mapIdxM.go f as arr = (fun x => arr.toList ++ x) <$> List.mapIdxMAuxSpec f arr.size as
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>β : Type u<VAR>f : ℕ → α → m β<VAR>as : List α<GOAL>as.mapIdxM f = List.traverse (Function.uncurry f) as.enum
<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u_1<VAR>f : ℕ → α → m PUnit.{u + 1}<VAR>as : List α<VAR>arr : Array PUnit.{u + 1}<GOAL>List.mapIdxMAux' f arr.size as = SeqRight.seqRight (List.mapIdxM.go f as arr) fun x => pure PUnit.unit
<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u_1<VAR>f : ℕ → α → m PUnit.{u + 1}<VAR>as : List α<GOAL>List.mapIdxM' f as = SeqRight.seqRight (as.mapIdxM f) fun x => pure PUnit.unit
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>H : Symmetric R<VAR>H₁ : ∀ (x : α), x ∈ l → R x x<VAR>H₂ : List.Pairwise R l<VAR>x : α<GOAL>x ∈ l → ∀ ⦃y : α⦄, y ∈ l → R x y
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>hR : Symmetric R<VAR>hl : List.Pairwise R l<VAR>a : α<GOAL>a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<VAR>hl : List.Pairwise R l<VAR>hr : Symmetric R<GOAL>{x | x ∈ l}.Pairwise R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → α → Prop<VAR>f : β → α<VAR>l : List β<GOAL>List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → α → Prop<VAR>p : β → Prop<VAR>f : (b : β) → p b → α<VAR>l : List β<VAR>h : ∀ (x : β), x ∈ l → p x<GOAL>List.Pairwise R (List.pmap f l h) ↔ List.Pairwise (fun b₁ b₂ => ∀ (h₁ : p b₁) (h₂ : p b₂), R (f b₁ h₁) (f b₂ h₂)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : α → α → Prop<VAR>l : List α<VAR>hl : List.Pairwise R l<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>h : ∀ (x : α), x ∈ l → p x<VAR>S : β → β → Prop<VAR>hS : ∀ ⦃x : α⦄ (hx : p x) ⦃y : α⦄ (hy : p y), R x y → S (f x hx) (f y hy)<GOAL>List.Pairwise S (List.pmap f l h)
<VAR>α : Type u_1<VAR>l : List α<VAR>r : α → α → Prop<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b<GOAL>List.Pairwise r l
<VAR>α : Type u_1<VAR>l : List α<VAR>r : α → α → Prop<VAR>hr : Reflexive r<VAR>h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b<GOAL>List.Pairwise r l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l ↔ ∀ (i j : ℕ) (h₁ : j < l.length) (h₂ : i < j), R (l.nthLe i ⋯) (l.nthLe j h₁)
<VAR>α : Sort u<GOAL>Countable α ↔ Nonempty (α ↪ ℕ)
<VAR>α : Sort u<GOAL>Uncountable α ↔ IsEmpty (α ↪ ℕ)
<VAR>α : Sort u_1<VAR>Countable α<GOAL>Nonempty (α ↪ ℕ)
<VAR>α : Sort u<VAR>β : Sort v<VAR>Countable β<VAR>f : α ↪ β<GOAL>Countable α
<VAR>α : Sort u<VAR>β : Sort v<VAR>Uncountable α<VAR>f : α ↪ β<GOAL>Uncountable β
<VAR>α : Type u<VAR>π : α → Type w<VAR>a : α<VAR>Uncountable (π a)<GOAL>Uncountable (Sigma π)
<VAR>α : Type u<VAR>a : α<GOAL>[a].sublists' = [[], [a]]
<VAR>α : Type u<VAR>a : α<VAR>r₁ r₂ : List (List α)<GOAL>List.sublists'Aux a r₁ r₂ = (Array.foldl (fun r l => r.push (a :: l)) (List.toArray r₂) (List.toArray r₁) 0).toList
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists' = List.foldr (fun a r => List.sublists'Aux a r r) [[]] l
<VAR>α : Type u<VAR>a : α<VAR>r₁ r₂ : List (List α)<GOAL>List.sublists'Aux a r₁ r₂ = r₂ ++ List.map (List.cons a) r₁
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists' = l.sublists' ++ List.map (List.cons a) l.sublists'
<VAR>α : Type u<VAR>s t : List α<GOAL>s ∈ t.sublists' ↔ s.Sublist t
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists'.length = 2 ^ l.length
<VAR>α : Type u<VAR>a : α<GOAL>[a].sublists = [[], [a]]
<VAR>α : Type u<GOAL>List.sublistsAux = fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] (List.toArray r) 0).toList
<VAR>α : Type u<GOAL>List.sublistsAux = fun a r => r.bind fun l => [l, a :: l]
<VAR>α : Type u<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).sublists = do let x ← l₂.sublists List.map (fun x_1 => x_1 ++ x) l₁.sublists
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists = do let x ← l.sublists [x, a :: x]
<VAR>α : Type u<VAR>l : List α<VAR>a : α<GOAL>(l ++ [a]).sublists = l.sublists ++ List.map (fun x => x ++ [a]) l.sublists
<VAR>α : Type u<VAR>l : List α<GOAL>l.reverse.sublists = List.map List.reverse l.sublists'
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists = List.map List.reverse l.reverse.sublists'
<VAR>α : Type u<VAR>l : List α<GOAL>l.reverse.sublists' = List.map List.reverse l.sublists
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists' = List.map List.reverse l.reverse.sublists
<VAR>α : Type u<VAR>s t : List α<GOAL>s ∈ t.sublists ↔ s.Sublist t
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists.length = 2 ^ l.length
<VAR>α : Type u<VAR>l : List α<GOAL>(List.map pure l).Sublist l.sublists
<VAR>α : Type u<VAR>l : List α<GOAL>(List.map List.ret l).Sublist l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>l : List α<VAR>f : List α → β<VAR>g : β → γ<VAR>r : List β<VAR>s : List γ<GOAL>List.sublistsLenAux n l (g ∘ f) (List.map g r ++ s) = List.map g (List.sublistsLenAux n l f r) ++ s
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>n : ℕ<VAR>f : List α → β<VAR>r : List β<GOAL>List.sublistsLenAux n l f r = List.map f (List.sublistsLen n l) ++ r
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : List α → β<VAR>r : List β<GOAL>List.sublistsLenAux 0 l f r = f [] :: r
<VAR>α : Type u<VAR>l : List α<GOAL>List.sublistsLen 0 l = [[]]
<VAR>α : Type u<VAR>n : ℕ<GOAL>List.sublistsLen (n + 1) [] = []
<VAR>α : Type u<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>List.sublistsLen (n + 1) (a :: l) = List.sublistsLen (n + 1) l ++ List.map (List.cons a) (List.sublistsLen n l)
<VAR>α : Type u<VAR>l : List α<GOAL>List.sublistsLen 1 l = List.map (fun x => [x]) l.reverse
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<GOAL>(List.sublistsLen n l).length = l.length.choose n
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<GOAL>(List.sublistsLen n l).Sublist l.sublists'
<VAR>α : Type u<VAR>n : ℕ<VAR>l₁ l₂ : List α<VAR>h : l₁.Sublist l₂<GOAL>(List.sublistsLen n l₁).Sublist (List.sublistsLen n l₂)
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<GOAL>l' ∈ List.sublistsLen n l → l'.length = n
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l'.Sublist l<GOAL>l' ∈ List.sublistsLen l'.length l
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<GOAL>l' ∈ List.sublistsLen n l ↔ l'.Sublist l ∧ l'.length = n
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<VAR>h : l.length < n<GOAL>List.sublistsLen n l = []
<VAR>α : Type u<VAR>l : List α<GOAL>List.sublistsLen l.length l = [l]
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<GOAL>List.Pairwise R l → List.Pairwise (List.Lex (Function.swap R)) l.sublists'
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>l : List α<VAR>H : List.Pairwise R l<GOAL>List.Pairwise (fun l₁ l₂ => List.Lex R l₁.reverse l₂.reverse) l.sublists
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists.Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists'.Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<VAR>h : l.Nodup<GOAL>(List.sublistsLen n l).Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).sublists = List.map (List.map f) l.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).sublists' = List.map (List.map f) l.sublists'
<VAR>α : Type u<VAR>l : List α<GOAL>l.sublists.Perm l.sublists'
<VAR>α : Type u<VAR>a : α<VAR>l : List α<GOAL>(a :: l).sublists.Perm (l.sublists ++ List.map (List.cons a) l.sublists)
<VAR>α : Type u<VAR>l l₁ l₂ : List α<GOAL>(l₁, l₂) ∈ l.sublists.revzip → (l₁ ++ l₂).Perm l
<VAR>α : Type u<VAR>l l₁ l₂ : List α<GOAL>(l₁, l₂) ∈ l.sublists'.revzip → (l₁ ++ l₂).Perm l
<VAR>α : Type u<VAR>l : List α<GOAL>((List.range (l.length + 1)).bind fun n => List.sublistsLen n l).Perm l.sublists'
<VAR>α : Sort u<VAR>self : Countable α<GOAL>∃ f, Function.Injective f
<VAR>α : Sort u<GOAL>Countable α ↔ ∃ f, Function.Injective f
<VAR>α : Sort u<VAR>Countable α<GOAL>∃ f, Function.Injective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>Countable β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Countable α
<VAR>α : Sort u<VAR>β : Sort v<VAR>Countable α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Countable β
<VAR>α : Sort u<VAR>Nonempty α<VAR>Countable α<GOAL>∃ f, Function.Surjective f
<VAR>α : Sort u<VAR>Nonempty α<GOAL>Countable α ↔ ∃ f, Function.Surjective f
<VAR>β : Sort v<VAR>α : Sort u_1<VAR>Countable α<VAR>e : α ≃ β<GOAL>Countable β
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Countable α ↔ Countable β
<VAR>α : Sort u_1<VAR>self : Uncountable α<GOAL>¬Countable α
<VAR>α : Sort u_1<GOAL>Uncountable α ↔ ¬Countable α
<VAR>α : Sort u<GOAL>¬Uncountable α ↔ Countable α
<VAR>α : Sort u<GOAL>¬Countable α ↔ Uncountable α
<VAR>α : Sort u<VAR>Countable α<GOAL>¬Uncountable α
<VAR>α : Sort u<VAR>Uncountable α<GOAL>¬Countable α
<VAR>α : Sort u<VAR>β : Sort v<VAR>Uncountable α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Uncountable β
<VAR>α : Sort u<VAR>β : Sort v<VAR>Uncountable β<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Uncountable α
<VAR>α : Sort u<VAR>β : Sort v<VAR>Uncountable α<VAR>Countable β<VAR>f : α → β<GOAL>¬Function.Injective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>Countable α<VAR>Uncountable β<VAR>f : α → β<GOAL>¬Function.Surjective f
<VAR>α : Sort u<VAR>Nonempty α<GOAL>Uncountable α ↔ ∀ (f : ℕ → α), ¬Function.Surjective f
<VAR>β : Sort v<VAR>α : Sort u_1<VAR>Uncountable α<VAR>e : α ≃ β<GOAL>Uncountable β
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>Uncountable α ↔ Uncountable β
<VAR>α : Sort u<GOAL>Function.Injective Opposite.op
<VAR>α : Sort u<GOAL>Function.Injective Opposite.unop
<VAR>α : Sort u<VAR>x : αᵒᵖ<GOAL>Opposite.op (Opposite.unop x) = x
<VAR>α : Sort u<VAR>x : α<GOAL>Opposite.unop (Opposite.op x) = x
<VAR>α : Sort u<VAR>x y : α<GOAL>Opposite.op x = Opposite.op y ↔ x = y
<VAR>α : Sort u<VAR>x y : αᵒᵖ<GOAL>Opposite.unop x = Opposite.unop y ↔ x = y
<VAR>α : Sort u<GOAL>Function.Surjective Opposite.op
<VAR>α : Sort u<GOAL>Function.Surjective Opposite.unop
<VAR>α : Sort u<GOAL>⇑Opposite.equivToOpposite = Opposite.op
<VAR>α : Sort u<GOAL>⇑Opposite.equivToOpposite.symm = Opposite.unop
<VAR>α : Sort u<VAR>x : α<VAR>y : αᵒᵖ<GOAL>Opposite.op x = y ↔ x = Opposite.unop y
<VAR>α : Sort u<VAR>x : αᵒᵖ<VAR>y : α<GOAL>Opposite.unop x = y ↔ x = Opposite.op y
<VAR>α : Type u_1<VAR>q₁ q₂ : Semiquot α<GOAL>q₁ = q₂ ↔ q₁.s = q₂.s
<VAR>α : Type u_1<VAR>q₁ q₂ : Semiquot α<GOAL>q₁ = q₂ ↔ ∀ (a : α), a ∈ q₁ ↔ a ∈ q₂
<VAR>α : Type u_1<VAR>q : Semiquot α<GOAL>∃ a, a ∈ q
<VAR>α : Type u_1<VAR>q : Semiquot α<VAR>a : α<VAR>h : a ∈ q<GOAL>q = Semiquot.mk h
<VAR>α : Type u_1<VAR>q : Semiquot α<GOAL>q.s.Nonempty
<VAR>α : Type u_1<VAR>a b : α<GOAL>a ∈ Semiquot.pure b ↔ a = b
<VAR>α : Type u_1<VAR>q : Semiquot α<VAR>s : Set α<VAR>h : q.s ⊆ s<GOAL>Semiquot.blur s q = q.blur' h
<VAR>α : Type u_1<VAR>q : Semiquot α<VAR>s : Set α<VAR>h : q.s ⊆ s<VAR>a : α<GOAL>a ∈ q.blur' h ↔ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>f : α → β<VAR>h : ∀ a ∈ q, ∀ b ∈ q, f a = f b<VAR>a : α<VAR>aq : a ∈ q<GOAL>q.liftOn f h = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>q : Semiquot α<VAR>b : β<GOAL>b ∈ Semiquot.map f q ↔ ∃ a ∈ q, f a = b
<VAR>α β : Type u_1<GOAL>(fun x x_1 => x <$> x_1) = Semiquot.map
<VAR>α β : Type u_1<GOAL>(fun x x_1 => x >>= x_1) = Semiquot.bind
<VAR>α : Type u_1<VAR>a b : α<GOAL>a ∈ pure b ↔ a = b
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∈ pure a
<VAR>α : Type u_1<VAR>a b : α<GOAL>pure a = pure b ↔ a = b
<VAR>α : Type u_1<VAR>a : α<VAR>s : Semiquot α<GOAL>pure a ≤ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>q : Semiquot α<VAR>p : q.IsPure<GOAL>q.get p ∈ q
<VAR>α : Type u_1<VAR>q : Semiquot α<VAR>p : q.IsPure<GOAL>q = pure (q.get p)
<VAR>α : Type u_1<VAR>a : α<GOAL>(pure a).IsPure
<VAR>α : Type u_1<VAR>s : Semiquot α<GOAL>s.IsPure ↔ ∃ a, s = pure a
<VAR>α : Type u_1<VAR>s t : Semiquot α<VAR>st : s ≤ t<VAR>h : t.IsPure<GOAL>s.IsPure
<VAR>α : Type u_1<VAR>s t : Semiquot α<VAR>h : t.IsPure<GOAL>s ≤ t ↔ s = t
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>q : Semiquot α<GOAL>q.IsPure
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : α<GOAL>a ∈ Semiquot.univ
<VAR>α : Type u_1<VAR>I J : Inhabited α<GOAL>Semiquot.univ = Semiquot.univ
<VAR>α : Type u_1<VAR>Inhabited α<GOAL>Semiquot.univ.IsPure ↔ Subsingleton α
<VAR>α : Type u_1<VAR>OrderedAddCommMonoid α<VAR>A B : Set α<VAR>hA : BddAbove A<VAR>hB : BddAbove B<GOAL>BddAbove (A + B)
<VAR>α : Type u_1<VAR>OrderedCommMonoid α<VAR>A B : Set α<VAR>hA : BddAbove A<VAR>hB : BddAbove B<GOAL>BddAbove (A * B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>One γ<VAR>c : α<VAR>f : β → γ<GOAL>(Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>Zero γ<VAR>c : α<VAR>f : β → γ<GOAL>(Function.support fun x => f (c⁻¹ • x)) = c • Function.support f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>One γ<VAR>c : α<VAR>hc : c ≠ 0<VAR>f : β → γ<GOAL>(Function.mulSupport fun x => f (c⁻¹ • x)) = c • Function.mulSupport f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>GroupWithZero α<VAR>MulAction α β<VAR>Zero γ<VAR>c : α<VAR>hc : c ≠ 0<VAR>f : β → γ<GOAL>(Function.support fun x => f (c⁻¹ • x)) = c • Function.support f
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => n • x) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : n ^ j • g = 0<GOAL>g +ᵥ s = s
<VAR>G : Type u_1<VAR>CommGroup G<VAR>n : ℤ<VAR>s : Set G<VAR>hs : (fun x => x ^ n) ⁻¹' s = s<VAR>g : G<VAR>j : ℕ<VAR>hg : g ^ n ^ j = 1<GOAL>g • s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE β<VAR>Add β<VAR>One β<VAR>f : α → β<GOAL>∅.EquitableOn f
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, f '' s ⊆ Set.Icc b (b + 1)
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>Add β<VAR>One β<VAR>s : Set α<VAR>f : α → β<GOAL>¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedSemiring β<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>f : α → β<GOAL>s.EquitableOn f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedSemiring β<VAR>a : α<VAR>f : α → β<GOAL>{a}.EquitableOn f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>(↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>h : (↑s).EquitableOn f<VAR>ha : a ∈ s<GOAL>(∑ i ∈ s, f i) / s.card ≤ f a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>h : (↑s).EquitableOn f<VAR>ha : a ∈ s<GOAL>f a ≤ (∑ i ∈ s, f i) / s.card + 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>(↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / s.card ∨ f a = (∑ i ∈ s, f i) / s.card + 1
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<GOAL>o.toOption.isSome = true ↔ o.Dom
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<GOAL>o.toOption = none ↔ ¬o.Dom
<VAR>α : Type u_1<VAR>o p : Part α<GOAL>(o.Dom ↔ p.Dom) → (∀ (h₁ : o.Dom) (h₂ : p.Dom), o.get h₁ = p.get h₂) → o = p
<VAR>α : Type u_1<VAR>o : Part α<GOAL>{ Dom := o.Dom, get := fun h => o.get h } = o
<VAR>α : Type u_1<VAR>a : α<VAR>o : Part α<GOAL>(a ∈ o) = ∃ (h : o.Dom), o.get h = a
<VAR>α : Type u_1<VAR>o : Part α<GOAL>o.Dom ↔ ∃ y, y ∈ o
<VAR>α : Type u_1<VAR>o : Part α<VAR>h : o.Dom<GOAL>o.get h ∈ o
<VAR>α : Type u_1<VAR>p : Prop<VAR>o : p → α<VAR>a : α<GOAL>a ∈ { Dom := p, get := o } ↔ ∃ (h : p), o h = a
<VAR>α : Type u_1<VAR>o p : Part α<VAR>H : ∀ (a : α), a ∈ o ↔ a ∈ p<GOAL>o = p
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ Part.none
<VAR>α : Type u_1<VAR>a : α<GOAL>(Part.some a).Dom
<VAR>α : Type u_1<VAR>a b : α<VAR>o : Part α<GOAL>a ∈ o → b ∈ o → a = b
<VAR>α : Type u_1<GOAL>Relator.LeftUnique fun x x_1 => x ∈ x_1
<VAR>α : Type u_1<VAR>o : Part α<VAR>a : α<VAR>h : a ∈ o<VAR>h' : o.Dom<GOAL>o.get h' = a
<VAR>α : Type u_1<VAR>o : Part α<GOAL>{a | a ∈ o}.Subsingleton
<VAR>α : Type u_1<VAR>a : α<VAR>ha : (Part.some a).Dom<GOAL>(Part.some a).get ha = a
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∈ Part.some a
<VAR>α : Type u_1<VAR>a b : α<GOAL>b ∈ Part.some a ↔ b = a
<VAR>α : Type u_1<VAR>a : α<VAR>o : Part α<GOAL>o = Part.some a ↔ a ∈ o
<VAR>α : Type u_1<VAR>o : Part α<GOAL>o = Part.none ↔ ∀ (a : α), a ∉ o
<VAR>α : Type u_1<VAR>o : Part α<GOAL>o = Part.none ↔ ¬o.Dom
<VAR>α : Type u_1<GOAL>¬Part.none.Dom
<VAR>α : Type u_1<VAR>x : α<GOAL>Part.some x ≠ Part.none
<VAR>α : Type u_1<VAR>x : α<GOAL>Part.none ≠ Part.some x
<VAR>α : Type u_1<VAR>o : Part α<GOAL>o ≠ Part.none ↔ ∃ x, o = Part.some x
<VAR>α : Type u_1<VAR>o : Part α<GOAL>o = Part.none ∨ ∃ x, o = Part.some x
<VAR>α : Type u_1<GOAL>Function.Injective Part.some
<VAR>α : Type u_1<VAR>a b : α<GOAL>Part.some a = Part.some b ↔ a = b
<VAR>α : Type u_1<VAR>a : Part α<VAR>ha : a.Dom<GOAL>Part.some (a.get ha) = a
<VAR>α : Type u_1<VAR>a : Part α<VAR>ha : a.Dom<VAR>b : α<GOAL>a.get ha = b ↔ a = Part.some b
<VAR>α : Type u_1<VAR>a : Part α<VAR>ha : a.Dom<VAR>b : Part α<VAR>h : a = b<GOAL>a.get ha = b.get ⋯
<VAR>α : Type u_1<VAR>o : Part α<VAR>a : α<VAR>h : o.Dom<GOAL>o.get h = a ↔ a ∈ o
<VAR>α : Type u_1<VAR>o : Part α<VAR>a : α<VAR>h : o.Dom<GOAL>a = o.get h ↔ a ∈ o
<VAR>α : Type u_1<VAR>Decidable Part.none.Dom<GOAL>Part.none.toOption = none
<VAR>α : Type u_1<VAR>a : α<VAR>Decidable (Part.some a).Dom<GOAL>(Part.some a).toOption = some a
<VAR>α : Type u_1<VAR>a : Part α<VAR>h : a.Dom<VAR>Decidable a.Dom<VAR>d : α<GOAL>a.getOrElse d = a.get h
<VAR>α : Type u_1<VAR>a : Part α<VAR>h : ¬a.Dom<VAR>Decidable a.Dom<VAR>d : α<GOAL>a.getOrElse d = d
<VAR>α : Type u_1<VAR>d : α<VAR>Decidable Part.none.Dom<GOAL>Part.none.getOrElse d = d
<VAR>α : Type u_1<VAR>a d : α<VAR>Decidable (Part.some a).Dom<GOAL>(Part.some a).getOrElse d = a
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<VAR>a : α<GOAL>a ∈ o.toOption ↔ a ∈ o
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<VAR>a : α<GOAL>o.toOption = some a ↔ a ∈ o
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<VAR>h : o.Dom<GOAL>o.toOption = some (o.get h)
<VAR>α : Type u_1<VAR>a : Part α<VAR>Decidable a.Dom<GOAL>a.toOption = none ↔ ¬a.Dom
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>a : Part α<VAR>Decidable a.Dom<VAR>b : β<VAR>f : α → β<GOAL>a.toOption.elim b f = if h : a.Dom then f (a.get h) else b
<VAR>α : Type u_1<VAR>a : α<VAR>o : Option α<GOAL>a ∈ ↑o ↔ a ∈ o
<VAR>α : Type u_4<VAR>o : Option α<GOAL>(↑o).Dom ↔ o.isSome = true
<VAR>α : Type u_4<VAR>o : Option α<GOAL>↑o = { Dom := o.isSome = true, get := o.get }
<VAR>α : Type u_1<GOAL>↑none = Part.none
<VAR>α : Type u_1<VAR>a : α<GOAL>↑(some a) = Part.some a
<VAR>α : Type u_1<VAR>P : Part α → Prop<VAR>a : Part α<VAR>hnone : P Part.none<VAR>hsome : ∀ (a : α), P (Part.some a)<GOAL>P a
<VAR>α : Type u_1<VAR>o : Option α<GOAL>(↑o).toOption = o
<VAR>α : Type u_1<VAR>o : Part α<VAR>Decidable o.Dom<GOAL>↑o.toOption = o
<VAR>α : Type u_1<VAR>x y : Part α<VAR>z : Part α<VAR>hx : x ≤ z<VAR>hy : y ≤ z<GOAL>x ≤ y ∨ y ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Part α<GOAL>∀ (a : o.Dom), (Part.map f o).get a = (f ∘ o.get) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Part α<GOAL>(Part.map f o).Dom = o.Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Part α<VAR>a : α<GOAL>a ∈ o → f a ∈ Part.map f o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>o : Part α<VAR>b : β<GOAL>b ∈ Part.map f o ↔ ∃ a ∈ o, f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Part.map f Part.none = Part.none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>Part.map f (Part.some a) = Part.some (f a)
<VAR>α : Type u_1<VAR>p : Prop<VAR>f : p → Part α<VAR>a : α<VAR>h : p<GOAL>a ∈ f h → a ∈ Part.assert p f
<VAR>α : Type u_1<VAR>p : Prop<VAR>f : p → Part α<VAR>a : α<GOAL>a ∈ Part.assert p f ↔ ∃ (h : p), a ∈ f h
<VAR>α : Type u_1<VAR>p : Prop<VAR>f : p → Part α<VAR>h : p<GOAL>Part.assert p f = f h
<VAR>α : Type u_1<VAR>p : Prop<VAR>f : p → Part α<VAR>h : ¬p<GOAL>Part.assert p f = Part.none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Part α<VAR>g : α → Part β<VAR>a : α<VAR>b : β<GOAL>a ∈ f → b ∈ g a → b ∈ f.bind g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Part α<VAR>g : α → Part β<VAR>b : β<GOAL>b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>o : Part α<VAR>h : o.Dom<VAR>f : α → Part β<GOAL>o.bind f = f (o.get h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Part β<VAR>a : Part α<VAR>h : (a.bind f).Dom<GOAL>a.Dom