ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_1} {p : α_1 → Prop} {f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM (fun a => p (f a)) x → SatisfiesM p (f <$> x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>q : α → Prop<GOAL>∀ {α_1 : Type u_1} {p : α_1 → Prop} {a : α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM q x → (∀ {b : α}, q b → p a) → SatisfiesM p (Functor.mapConst a x)
<VAR>m : Type u_1 → Type u_2<GOAL>∀ {α : Type u_1} {p : α → Prop} {a : α} [inst : Applicative m] [inst_1 : LawfulApplicative m], p a → SatisfiesM p (pure a)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop} {q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ f → SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ f → SatisfiesM p₂ x → SatisfiesM (fun c => ∃ f a, p₁ f ∧ p₂ a ∧ c = f a) (Seq.seq f fun x_1 => x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p₂ : α → Prop<GOAL>∀ {α_1 : Type u_1} {q : α_1 → Prop} {f : m (α → α_1)} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) f → SatisfiesM p₂ x → SatisfiesM q (Seq.seq f fun x_1 => x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<GOAL>∀ {α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ f → SatisfiesM (fun a => ∀ {f : α → α_1}, p₁ f → q (f a)) x → SatisfiesM q (Seq.seq f fun x_1 => x)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p₁ : α → Prop<GOAL>∀ {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : α → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q a_1) → SatisfiesM q (SeqLeft.seqLeft x fun x => y)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_1<VAR>p₁ : α → Prop<GOAL>∀ {a : Type u_1} {p₂ : a → Prop} {y : m a} {q : a → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q b) → SatisfiesM q (SeqRight.seqRight x fun x => y)
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>p : α → Prop<VAR>x : m α<VAR>q : β → Prop<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM p x<VAR>hf : ∀ (a : α), p a → SatisfiesM q (f a)<GOAL>SatisfiesM q (x >>= f)
<VAR>m : Type u_1 → Type u_2<VAR>α β : Type u_1<VAR>q : β → Prop<VAR>x : m α<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → m β<VAR>hx : SatisfiesM (fun a => SatisfiesM q (f a)) x<GOAL>SatisfiesM q (x >>= f)
<GOAL>∀ {type : Type u_1} {p : type → Prop} {x : Id type}, SatisfiesM p x ↔ p x
<GOAL>∀ {α : Type u_1} {p : α → Prop} {x : Option α}, SatisfiesM p x ↔ ∀ (a : α), x = some a → p a
<VAR>ε : Type u_1<GOAL>∀ {α : Type u_2} {p : α → Prop} {x : Except ε α}, SatisfiesM p x ↔ ∀ (a : α), x = Except.ok a → p a
<VAR>m : Type u_1 → Type u_2<VAR>ρ : Type u_1<GOAL>∀ {α : Type u_1} {p : α → Prop} {x : ReaderT ρ m α} [inst : Monad m], SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM p (x s)
<VAR>m : Type → Type<VAR>ω σ : Type<GOAL>∀ {α : Type} {p : α → Prop} {x : StateRefT' ω σ m α} [inst : Monad m], SatisfiesM p x ↔ ∀ (s : ST.Ref ω σ), SatisfiesM p (x s)
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>p : α → Prop<VAR>x : StateT ρ m α<VAR>Monad m<VAR>LawfulMonad m<GOAL>SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
<VAR>m : Type u_1 → Type u_2<VAR>α ρ : Type u_1<VAR>p : α → Prop<VAR>x : ExceptT ρ m α<VAR>Monad m<VAR>LawfulMonad m<GOAL>SatisfiesM p x ↔ SatisfiesM (fun x => ∀ (a : α), x = Except.ok a → p a) x
<VAR>o₁ o₂ : Ordering<GOAL>o₁.swap = o₂.swap ↔ o₁ = o₂
<VAR>o₁ o₂ : Ordering<GOAL>(o₁.then o₂).swap = o₁.swap.then o₂.swap
<VAR>o₁ o₂ : Ordering<GOAL>o₁.then o₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt
<VAR>o₁ o₂ : Ordering<GOAL>o₁.then o₂ = Ordering.eq ↔ o₁ = Ordering.eq ∧ o₂ = Ordering.eq
<VAR>o₁ o₂ : Ordering<GOAL>o₁.then o₂ = Ordering.gt ↔ o₁ = Ordering.gt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.gt
<VAR>α : Sort u_1<VAR>le : α → α → Bool<VAR>self : Batteries.TotalBLE le<VAR>a b : α<GOAL>le a b = true ∨ le b a = true
<VAR>α : Sort u_1<VAR>cmp : α → α → Ordering<VAR>self : Batteries.OrientedCmp cmp<VAR>x y : α<GOAL>(cmp x y).swap = cmp y x
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Batteries.OrientedCmp cmp], cmp x y = Ordering.gt ↔ cmp y x = Ordering.lt
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Batteries.OrientedCmp cmp], cmp x y ≠ Ordering.gt ↔ cmp y x ≠ Ordering.lt
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α} [inst : Batteries.OrientedCmp cmp], cmp x y = Ordering.eq ↔ cmp y x = Ordering.eq
<GOAL>∀ {α : Sort u_1} {cmp : α → α → Ordering} {x : α} [inst : Batteries.OrientedCmp cmp], cmp x x = Ordering.eq
<VAR>α : Sort u_1<VAR>cmp : α → α → Ordering<VAR>self : Batteries.TransCmp cmp<VAR>x y z : α<GOAL>cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp x_1 z ≠ Ordering.lt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.lt → cmp y x_1 ≠ Ordering.lt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.gt → cmp y x_1 ≠ Ordering.gt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y ≠ Ordering.gt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z ≠ Ordering.gt → cmp x_1 z = Ordering.lt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.lt → cmp y z = Ordering.lt → cmp x_1 z = Ordering.lt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.gt → cmp y z = Ordering.gt → cmp x_1 z = Ordering.gt
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y z : x}, cmp x_1 y = Ordering.eq → cmp x_1 z = cmp y z
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {x_1 y : x}, cmp x_1 y = Ordering.eq → cmp x_1 = cmp y
<GOAL>∀ {x : Sort u_1} {cmp : x → x → Ordering} [inst : Batteries.TransCmp cmp] {y z x : x}, cmp y z = Ordering.eq → cmp x y = cmp x z
<VAR>α : Type u_1<VAR>BEq α<VAR>cmp : α → α → Ordering<VAR>self : Batteries.BEqCmp cmp<VAR>x y : α<GOAL>cmp x y = Ordering.eq ↔ (x == y) = true
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>BEq α<VAR>LawfulBEq α<VAR>Batteries.BEqCmp cmp<GOAL>cmp x y = Ordering.eq ↔ x = y
<VAR>α : Type u_1<VAR>LT α<VAR>cmp : α → α → Ordering<VAR>self : Batteries.LTCmp cmp<VAR>x y : α<GOAL>cmp x y = Ordering.lt ↔ x < y
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>LT α<VAR>Batteries.LTCmp cmp<GOAL>cmp x y = Ordering.gt ↔ y < x
<VAR>α : Type u_1<VAR>LE α<VAR>cmp : α → α → Ordering<VAR>self : Batteries.LECmp cmp<VAR>x y : α<GOAL>cmp x y ≠ Ordering.gt ↔ x ≤ y
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x y : α<VAR>LE α<VAR>Batteries.LECmp cmp<GOAL>cmp x y ≠ Ordering.lt ↔ y ≤ x
<VAR>α : Type u_1<VAR>x y : α<VAR>LT α<VAR>Decidable (x < y)<VAR>DecidableEq α<GOAL>compareOfLessAndEq x y = Ordering.lt ↔ x < y
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y<GOAL>Batteries.TransCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>LE α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>not_lt : ∀ {x y : α}, ¬x < y → y ≤ x<VAR>le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y<GOAL>Batteries.TransCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>BEq α<VAR>LawfulBEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<GOAL>Batteries.BEqCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y<GOAL>Batteries.LTCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>LE α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>not_lt : ∀ {x y : α}, ¬x < y → y ≤ x<VAR>le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y<GOAL>Batteries.LTCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>LE α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x<VAR>le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y<GOAL>Batteries.LECmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel LT.lt<VAR>DecidableEq α<VAR>BEq α<VAR>LawfulBEq α<VAR>LE α<VAR>lt_irrefl : ∀ (x : α), ¬x < x<VAR>lt_trans : ∀ {x y z : α}, x < y → y < z → x < z<VAR>not_lt : ∀ {x y : α}, ¬x < y ↔ y ≤ x<VAR>le_antisymm : ∀ {x y : α}, x ≤ y → y ≤ x → x = y<GOAL>Batteries.LawfulCmp fun x x_1 => compareOfLessAndEq x x_1
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>LT α<VAR>DecidableEq α<VAR>BEq α<VAR>LawfulBEq α<VAR>Batteries.BEqCmp cmp<VAR>Batteries.LTCmp cmp<VAR>x y : α<VAR>Decidable (x < y)<GOAL>cmp x y = compareOfLessAndEq x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ord α<VAR>Ord β<GOAL>compare = compareLex (compareOn fun x => x.fst) (compareOn fun x => x.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ord α<VAR>Ord β<VAR>Batteries.OrientedOrd α<VAR>Batteries.OrientedOrd β<GOAL>Batteries.OrientedOrd (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ord α<VAR>Ord β<VAR>Batteries.TransOrd α<VAR>Batteries.TransOrd β<GOAL>Batteries.TransOrd (α × β)
<VAR>α : Type u_1<VAR>ord : Ord α<VAR>inst : Batteries.OrientedOrd α<GOAL>Batteries.OrientedOrd α
<VAR>α : Type u_1<VAR>ord : Ord α<VAR>inst : Batteries.TransOrd α<GOAL>Batteries.TransOrd α
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>ord : Ord β<VAR>Batteries.OrientedOrd β<VAR>f : α → β<GOAL>Batteries.OrientedOrd α
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>ord : Ord β<VAR>Batteries.TransOrd β<VAR>f : α → β<GOAL>Batteries.TransOrd α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>oα : Ord α<VAR>oβ : Ord β<VAR>Batteries.OrientedOrd α<VAR>Batteries.OrientedOrd β<GOAL>Batteries.OrientedOrd (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>oα : Ord α<VAR>oβ : Ord β<VAR>Batteries.TransOrd α<VAR>Batteries.TransOrd β<GOAL>Batteries.TransOrd (α × β)
<VAR>α : Type u_1<VAR>ord₁ ord₂ : Ord α<VAR>Batteries.OrientedOrd α<VAR>Batteries.OrientedOrd α<GOAL>Batteries.OrientedOrd α
<VAR>α : Type u_1<VAR>ord₁ ord₂ : Ord α<VAR>Batteries.TransOrd α<VAR>Batteries.TransOrd α<GOAL>Batteries.TransOrd α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Sum.inl x).isLeft = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Sum.inr x).isLeft = false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Sum.inl x).isRight = false
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Sum.inr x).isRight = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>h : (Sum.inl x).isLeft = true<GOAL>(Sum.inl x).getLeft h = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<VAR>h : (Sum.inr x).isRight = true<GOAL>(Sum.inr x).getRight h = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Sum.inl x).getLeft? = some x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Sum.inr x).getLeft? = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Sum.inl x).getRight? = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Sum.inr x).getRight? = some x
<VAR>α : Type u_1<VAR>γ : Sort u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>x : α<GOAL>Sum.elim f g (Sum.inl x) = f x
<VAR>α : Type u_1<VAR>γ : Sort u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>x : β<GOAL>Sum.elim f g (Sum.inr x) = g x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>f : α → α'<VAR>g : β → β'<VAR>x : α<GOAL>Sum.map f g (Sum.inl x) = Sum.inl (f x)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>f : α → α'<VAR>g : β → β'<VAR>x : β<GOAL>Sum.map f g (Sum.inr x) = Sum.inr (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Sum.inl x).swap = Sum.inr x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Sum.inr x).swap = Sum.inl x
<GOAL>∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {a : α} {c : γ}, Sum.LiftRel r s (Sum.inl a) (Sum.inl c) ↔ r a c
<GOAL>∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {a : α} {d : δ}, ¬Sum.LiftRel r s (Sum.inl a) (Sum.inr d)
<GOAL>∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {b : β} {c : γ}, ¬Sum.LiftRel r s (Sum.inr b) (Sum.inl c)
<GOAL>∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {b : β} {d : δ}, Sum.LiftRel r s (Sum.inr b) (Sum.inr d) ↔ s b d
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {a₁ a₂ : α}, Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂) ↔ r a₁ a₂
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {b₁ b₂ : β}, Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂) ↔ s b₁ b₂
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {b : β} {a : α}, ¬Sum.Lex r s (Sum.inr b) (Sum.inl a)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>L' : List α<VAR>hL' : ∀ ⦃x : α⦄, x ∈ L' → p x<GOAL>List.pmap f L' hL' = List.map (fun x => match x with | ⟨x, hx⟩ => f x hx) (List.pmap Subtype.mk L' hL')
<VAR>α : Type u<VAR>l : List α<GOAL>l.eraseIdx 0 = l.tail
<VAR>α : Type u<VAR>l : List α<VAR>i : Nat<GOAL>l.eraseIdx i = List.take i l ++ List.drop (i + 1) l
<VAR>α : Type u<VAR>l : List α<VAR>k : Nat<GOAL>(l.eraseIdx k).Sublist l
<VAR>α : Type u<VAR>l : List α<VAR>k : Nat<GOAL>l.eraseIdx k ⊆ l
<VAR>α : Type u<VAR>l : List α<VAR>k : Nat<GOAL>l.eraseIdx k = l ↔ l.length ≤ k
<VAR>α : Type u<VAR>l : List α<VAR>k : Nat<VAR>hk : k < l.length<VAR>l' : List α<GOAL>(l ++ l').eraseIdx k = l.eraseIdx k ++ l'
<VAR>α : Type u<VAR>l : List α<VAR>k : Nat<VAR>hk : l.length ≤ k<VAR>l' : List α<GOAL>(l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l <+: l'<VAR>k : Nat<GOAL>l.eraseIdx k <+: l'.eraseIdx k
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l[↑i] = x
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l.get i = x
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l[i]? = some x
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l.get? i = some x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α ⊕ β → Prop<GOAL>(∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (Sum.inl a)) ∧ ∀ (b : β), p (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α ⊕ β → Prop<GOAL>(∃ x, p x) ↔ (∃ a, p (Sum.inl a)) ∨ ∃ b, p (Sum.inr b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : α ⊕ β → Sort u_3<VAR>p : ((ab : α ⊕ β) → γ ab) → Prop<GOAL>(∀ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔ ∀ (fa : (val : α) → γ (Sum.inl val)) (fb : (val : β) → γ (Sum.inr val)), p fun t => Sum.rec fa fb t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<VAR>h : x.isLeft = true<GOAL>Sum.inl (x.getLeft h) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<VAR>h : x.isRight = true<GOAL>Sum.inr (x.getRight h) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<VAR>h : x.isLeft = true<GOAL>x = Sum.inl (x.getLeft h)
<GOAL>∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α ⊕ β} (h : x.isLeft = true), x.getLeft h = a ↔ x = Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<VAR>h : x.isRight = true<GOAL>x = Sum.inr (x.getRight h)
<GOAL>∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α ⊕ β} (h : x.isRight = true), x.getRight h = b ↔ x = Sum.inr b
<GOAL>∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α ⊕ β}, x.getLeft? = some a ↔ x = Sum.inl a
<GOAL>∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α ⊕ β}, x.getRight? = some b ↔ x = Sum.inr b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>(!decide (x.isLeft = x.isRight)) = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.isLeft = false ↔ x.isRight = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>¬x.isLeft = true ↔ x.isRight = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>(!decide (x.isRight = x.isLeft)) = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.isRight = false ↔ x.isLeft = true
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>¬x.isRight = true ↔ x.isLeft = true
<GOAL>∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isLeft = true ↔ ∃ y, x = Sum.inl y
<GOAL>∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isRight = true ↔ ∃ y, x = Sum.inr y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : α<GOAL>Sum.inl a = Sum.inl b ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a b : β<GOAL>Sum.inr a = Sum.inr b ↔ a = b
<GOAL>∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β}, Sum.inl a ≠ Sum.inr b
<GOAL>∀ {β : Type u_1} {b : β} {α : Type u_2} {a : α}, Sum.inr b ≠ Sum.inl a
<VAR>α : Type u_1<VAR>γ : Sort u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<GOAL>Sum.elim f g ∘ Sum.inl = f
<VAR>α : Type u_1<VAR>γ : Sort u_2<VAR>β : Type u_3<VAR>f : α → γ<VAR>g : β → γ<GOAL>Sum.elim f g ∘ Sum.inr = g
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Sum.elim Sum.inl Sum.inr = id
<VAR>γ : Sort u_1<VAR>δ : Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : γ → δ<VAR>g : α → γ<VAR>h : β → γ<GOAL>f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Sort u_3<VAR>f : α ⊕ β → γ<GOAL>Sum.elim (f ∘ Sum.inl) (f ∘ Sum.inr) = f
<VAR>α' : Type u_1<VAR>α'' : Type u_2<VAR>β' : Type u_3<VAR>β'' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f' : α' → α''<VAR>g' : β' → β''<VAR>f : α → α'<VAR>g : β → β'<VAR>x : α ⊕ β<GOAL>Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x
<VAR>α' : Type u_1<VAR>α'' : Type u_2<VAR>β' : Type u_3<VAR>β'' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>f' : α' → α''<VAR>g' : β' → β''<VAR>f : α → α'<VAR>g : β → β'<GOAL>Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Sum.map id id = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ε : Sort u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>f₁ : α → β<VAR>f₂ : β → ε<VAR>g₁ : γ → δ<VAR>g₂ : δ → ε<VAR>x : α ⊕ γ<GOAL>Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ε : Sort u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>f₁ : α → β<VAR>f₂ : β → ε<VAR>g₁ : γ → δ<VAR>g₂ : δ → ε<GOAL>Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α ⊕ γ<GOAL>(Sum.map f g x).isLeft = x.isLeft
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α ⊕ γ<GOAL>(Sum.map f g x).isRight = x.isRight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α ⊕ γ<GOAL>(Sum.map f g x).getLeft? = Option.map f x.getLeft?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β<VAR>g : γ → δ<VAR>x : α ⊕ γ<GOAL>(Sum.map f g x).getRight? = Option.map g x.getRight?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.swap.swap = x
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Sum.swap ∘ Sum.swap = id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.swap.isLeft = x.isRight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.swap.isRight = x.isLeft
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.swap.getLeft? = x.getRight?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α ⊕ β<GOAL>x.swap.getRight? = x.getLeft?
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s₁ s₂ : β → β_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, (∀ (a : α) (b : α_1), r₁ a b → r₂ a b) → (∀ (a : β) (b : β_1), s₁ a b → s₂ a b) → Sum.LiftRel r₁ s₁ x y → Sum.LiftRel r₂ s₂ x y
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {r₁ r₂ : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s : β → β_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, (∀ (a : α) (b : α_1), r₁ a b → r₂ a b) → Sum.LiftRel r₁ s x y → Sum.LiftRel r₂ s x y
<GOAL>∀ {β : Type u_1} {β_1 : Type u_2} {s₁ s₂ : β → β_1 → Prop} {α : Type u_3} {α_1 : Type u_4} {r : α → α_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, (∀ (a : β) (b : β_1), s₁ a b → s₂ a b) → Sum.LiftRel r s₁ x y → Sum.LiftRel r s₂ x y
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {r : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s : β → β_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, Sum.LiftRel r s x y → Sum.LiftRel s r x.swap y.swap
<GOAL>∀ {β : Type u_1} {β_1 : Type u_2} {s : β → β_1 → Prop} {α : Type u_3} {α_1 : Type u_4} {r : α → α_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, Sum.LiftRel s r x.swap y.swap ↔ Sum.LiftRel r s x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>a b : α ⊕ β<VAR>h : Sum.LiftRel r s a b<GOAL>Sum.Lex r s a b
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop}, Subrelation (Sum.LiftRel r s) (Sum.Lex r s)
<GOAL>∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {β : Type u_2} {s₁ s₂ : β → β → Prop} {x y : α ⊕ β}, (∀ (a b : α), r₁ a b → r₂ a b) → (∀ (a b : β), s₁ a b → s₂ a b) → Sum.Lex r₁ s₁ x y → Sum.Lex r₂ s₂ x y
<GOAL>∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {x y : α ⊕ β}, (∀ (a b : α), r₁ a b → r₂ a b) → Sum.Lex r₁ s x y → Sum.Lex r₂ s x y
<GOAL>∀ {β : Type u_1} {s₁ s₂ : β → β → Prop} {α : Type u_2} {r : α → α → Prop} {x y : α ⊕ β}, (∀ (a b : β), s₁ a b → s₂ a b) → Sum.Lex r s₁ x y → Sum.Lex r s₂ x y
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {a : α} {β : Type u_2} {s : β → β → Prop}, Acc r a → Acc (Sum.Lex r s) (Sum.inl a)
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop}, (∀ (a : α), Acc (Sum.Lex r s) (Sum.inl a)) → ∀ {b : β}, Acc s b → Acc (Sum.Lex r s) (Sum.inr b)
<GOAL>∀ {α : Type u_1} {r : α → α → Prop} {α_1 : Type u_2} {s : α_1 → α_1 → Prop}, WellFounded r → WellFounded s → WellFounded (Sum.Lex r s)
<VAR>γ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>c : γ<GOAL>Sum.elim (Function.const α c) (Function.const β c) = Function.const (α ⊕ β) c
<VAR>γ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>c : γ<GOAL>(Sum.elim (fun x => c) fun x => c) = fun x => c
<VAR>α : Type u<VAR>self : Batteries.DList α<VAR>l : List α<GOAL>self.apply l = self.apply [] ++ l
<VAR>x y : UInt8<GOAL>x.toNat = y.toNat → x = y
<VAR>x y : UInt8<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>x : UInt8<GOAL>↑x.val = x.toNat
<VAR>n : Nat<GOAL>(OfNat.ofNat n).val = OfNat.ofNat n
<VAR>n : Nat<GOAL>(OfNat.ofNat n).toNat = n % UInt8.size
<VAR>x : UInt8<GOAL>x.toNat < 2 ^ 8
<VAR>x : UInt8<GOAL>x.toUInt16.toNat = x.toNat
<VAR>x : UInt8<GOAL>x.toUInt32.toNat = x.toNat
<VAR>x : UInt8<GOAL>x.toUInt64.toNat = x.toNat
<VAR>x y : UInt8<GOAL>(x + y).toNat = (x.toNat + y.toNat) % UInt8.size
<VAR>x y : UInt8<GOAL>(x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size
<VAR>x y : UInt8<GOAL>(x * y).toNat = x.toNat * y.toNat % UInt8.size
<VAR>x y : UInt8<GOAL>(x / y).toNat = x.toNat / y.toNat
<VAR>x y : UInt8<GOAL>(x % y).toNat = x.toNat % y.toNat
<VAR>x : UInt8<VAR>n : Nat<GOAL>(x.modn n).toNat = x.toNat % n
<VAR>x y : UInt8<GOAL>x = y ↔ x ≤ y ∧ y ≤ x
<VAR>x y : UInt8<VAR>h1 : x ≤ y<VAR>h2 : y ≤ x<GOAL>x = y
<VAR>x y : UInt16<GOAL>x.toNat = y.toNat → x = y
<VAR>x y : UInt16<GOAL>x = y ↔ x.toNat = y.toNat
<VAR>x : UInt16<GOAL>↑x.val = x.toNat
<VAR>n : Nat<GOAL>(OfNat.ofNat n).toNat = n % UInt16.size
<VAR>x : UInt16<GOAL>x.toNat < 2 ^ 16
<VAR>x : UInt16<GOAL>x.toUInt8.toNat = x.toNat % 2 ^ 8