ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Finset.Icc a₁ b₁ ⊆ Finset.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Finset.Icc a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Finset.Icc a₁ b₁ ⊆ Finset.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ < a₁<VAR>hb : b₁ ≤ b₂<GOAL>Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ < b₂<GOAL>Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ico a a = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ioc a a = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Ioo a a = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hca : c ≤ a<GOAL>Finset.filter (fun x => x < c) (Finset.Ico a b) = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hbc : b ≤ c<GOAL>Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hcb : c ≤ b<GOAL>Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a c
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => c ≤ x<VAR>hca : c ≤ a<GOAL>Finset.filter (fun x => c ≤ x) (Finset.Ico a b) = Finset.Ico a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidablePred fun x => b ≤ x<GOAL>Finset.filter (fun x => b ≤ x) (Finset.Ico a b) = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => c ≤ x<VAR>hac : a ≤ c<GOAL>Finset.filter (fun x => c ≤ x) (Finset.Ico a b) = Finset.Ico c b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>h : b < c<GOAL>Finset.filter (fun x => x < c) (Finset.Icc a b) = Finset.Icc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>h : b < c<GOAL>Finset.filter (fun x => x < c) (Finset.Ioc a b) = Finset.Ioc a b
<VAR>α : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a c : α<VAR>DecidablePred fun x => x < c<VAR>h : a < c<GOAL>Finset.filter (fun x => x < c) (Finset.Iic a) = Finset.Iic a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype α<VAR>DecidablePred fun j => a < j ∧ j < b<GOAL>Finset.filter (fun j => a < j ∧ j < b) Finset.univ = Finset.Ioo a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype α<VAR>DecidablePred fun j => a < j ∧ j ≤ b<GOAL>Finset.filter (fun j => a < j ∧ j ≤ b) Finset.univ = Finset.Ioc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype α<VAR>DecidablePred fun j => a ≤ j ∧ j < b<GOAL>Finset.filter (fun j => a ≤ j ∧ j < b) Finset.univ = Finset.Ico a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>Fintype α<VAR>DecidablePred fun j => a ≤ j ∧ j ≤ b<GOAL>Finset.filter (fun j => a ≤ j ∧ j ≤ b) Finset.univ = Finset.Icc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<VAR>LocallyFiniteOrderTop α<GOAL>(Finset.Ici a).Nonempty
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<VAR>LocallyFiniteOrderTop α<GOAL>(Finset.Ioi a).Nonempty ↔ ¬IsMax a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Icc a b ⊆ Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Ico a b ⊆ Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Ioc a b ⊆ Finset.Ioi a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Ioo a b ⊆ Finset.Ioi a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Ioc a b ⊆ Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderTop α<GOAL>Finset.Ioo a b ⊆ Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<VAR>LocallyFiniteOrderBot α<GOAL>(Finset.Iic a).Nonempty
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<VAR>LocallyFiniteOrderBot α<GOAL>(Finset.Iio a).Nonempty ↔ ¬IsMin a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Icc a b ⊆ Finset.Iic b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Ioc a b ⊆ Finset.Iic b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Ico a b ⊆ Finset.Iio b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Ioo a b ⊆ Finset.Iio b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Ico a b ⊆ Finset.Iic b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>LocallyFiniteOrderBot α<GOAL>Finset.Ioo a b ⊆ Finset.Iic b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>Finset.Ioi a ⊆ Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>s : Set α<VAR>hs : BddBelow s<GOAL>s.Finite
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>s : Set α<GOAL>s.Infinite → ¬BddBelow s
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<VAR>Fintype α<VAR>DecidablePred fun x => a < x<GOAL>Finset.filter (fun x => a < x) Finset.univ = Finset.Ioi a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<VAR>Fintype α<VAR>DecidablePred fun x => a ≤ x<GOAL>Finset.filter (fun x => a ≤ x) Finset.univ = Finset.Ici a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>Finset.Iio a ⊆ Finset.Iic a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>s.Finite
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>s : Set α<GOAL>s.Infinite → ¬BddAbove s
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<VAR>Fintype α<VAR>DecidablePred fun x => x < a<GOAL>Finset.filter (fun x => x < a) Finset.univ = Finset.Iio a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<VAR>Fintype α<VAR>DecidablePred fun x => x ≤ a<GOAL>Finset.filter (fun x => x ≤ a) Finset.univ = Finset.Iic a
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>Disjoint (Finset.Ioi a) (Finset.Iio a)
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Finset.Icc a a = {a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.Icc a b = {c} ↔ a = c ∧ b = c
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Disjoint (Finset.Ico a b) (Finset.Ico b c)
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>(Finset.Icc a b).erase a = Finset.Ioc a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>(Finset.Icc a b).erase b = Finset.Ico a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>(Finset.Ico a b).erase a = Finset.Ioo a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>(Finset.Ioc a b).erase b = Finset.Ioo a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b : α<GOAL>Finset.Icc a b \ {a, b} = Finset.Ioo a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≤ b<GOAL>insert b (Finset.Ico a b) = Finset.Icc a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≤ b<GOAL>insert a (Finset.Ioc a b) = Finset.Icc a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a < b<GOAL>insert a (Finset.Ioo a b) = Finset.Ico a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a < b<GOAL>insert b (Finset.Ioo a b) = Finset.Ioc a b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≤ b<GOAL>Finset.Icc a b \ Finset.Ico a b = {b}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≤ b<GOAL>Finset.Icc a b \ Finset.Ioc a b = {a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≤ b<GOAL>Finset.Icc a b \ Finset.Ioo a b = {a, b}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a < b<GOAL>Finset.Ico a b \ Finset.Ioo a b = {a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidableEq α<VAR>h : a < b<GOAL>Finset.Ioc a b \ Finset.Ioo a b = {b}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c : α<GOAL>Finset.Ico a b ∩ Finset.Ico b c = ∅
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Finset.Icc a b = Finset.cons b (Finset.Ico a b) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Finset.Icc a b = Finset.cons a (Finset.Ioc a b) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Finset.Ioc a b = Finset.cons b (Finset.Ioo a b) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Finset.Ico a b = Finset.cons a (Finset.Ioo a b) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidablePred fun x => x ≤ a<VAR>hab : a < b<GOAL>Finset.filter (fun x => x ≤ a) (Finset.Ico a b) = {a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ico a b).card = (Finset.Icc a b).card - 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ioc a b).card = (Finset.Icc a b).card - 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ioo a b).card = (Finset.Ico a b).card - 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ioo a b).card = (Finset.Ioc a b).card - 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ioo a b).card = (Finset.Icc a b).card - 2
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderTop α<VAR>DecidableEq α<VAR>a : α<GOAL>(Finset.Ici a).erase a = Finset.Ioi a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderTop α<VAR>DecidableEq α<VAR>a : α<GOAL>insert a (Finset.Ioi a) = Finset.Ici a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderTop α<VAR>b : α<GOAL>b ∉ Finset.Ioi b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>Finset.Ici a = Finset.cons a (Finset.Ioi a) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>(Finset.Ioi a).card = (Finset.Ici a).card - 1
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderBot α<VAR>DecidableEq α<VAR>b : α<GOAL>(Finset.Iic b).erase b = Finset.Iio b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderBot α<VAR>DecidableEq α<VAR>b : α<GOAL>insert b (Finset.Iio b) = Finset.Iic b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderBot α<VAR>b : α<GOAL>b ∉ Finset.Iio b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderBot α<VAR>b : α<GOAL>Finset.Iic b = Finset.cons b (Finset.Iio b) ⋯
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>(Finset.Iio a).card = (Finset.Iic a).card - 1
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>(Finset.Iic a).sup' ⋯ id = a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>LocallyFiniteOrderBot α<VAR>OrderBot α<VAR>a : α<GOAL>(Finset.Iic a).sup id = a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>LocallyFiniteOrderTop α<VAR>a : α<GOAL>(Finset.Ici a).inf' ⋯ id = a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>LocallyFiniteOrderTop α<VAR>OrderTop α<VAR>a : α<GOAL>(Finset.Ici a).inf id = a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a₁ b₁ a₂ b₂ : α<VAR>h : a₁ < b₁<GOAL>Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Finset.Ico a b ∪ Finset.Ico b c = Finset.Ico a c
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Finset.Ioc a b ∪ Finset.Ioc b c = Finset.Ioc a c
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.Ico a c ⊆ Finset.Ico a b ∪ Finset.Ico b c
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c d : α<VAR>hcb : c ≤ b<VAR>had : a ≤ d<GOAL>Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Finset.Ico a b ∩ Finset.Ico c d = Finset.Ico (max a c) (min b d)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a (min b c)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.filter (fun x => c ≤ x) (Finset.Ico a b) = Finset.Ico (max a c) b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.filter (fun x => x < c) (Finset.Ioo a b) = Finset.Ioo a (min b c)
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>LocallyFiniteOrderBot α<VAR>a b : α<GOAL>Finset.filter (fun x => x < b) (Finset.Iio a) = Finset.Iio (min a b)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.Ico a b \ Finset.Ico a c = Finset.Ico (max a c) b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Finset.Ico a b \ Finset.Ico c b = Finset.Ico a (min b c)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrderBot α<VAR>s : Set α<VAR>hs : s.Infinite<VAR>a : α<GOAL>∃ b ∈ s, a < b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrderBot α<VAR>s : Set α<VAR>Nonempty α<GOAL>s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, a < b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrderTop α<VAR>s : Set α<VAR>hs : s.Infinite<VAR>a : α<GOAL>∃ b ∈ s, b < a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrderTop α<VAR>s : Set α<VAR>Nonempty α<GOAL>s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, b < a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>Fintype α<VAR>LocallyFiniteOrderTop α<VAR>LocallyFiniteOrderBot α<VAR>a : α<GOAL>(Finset.Ioi a).disjUnion (Finset.Iio a) ⋯ = {a}ᶜ
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>[[OrderDual.toDual a, OrderDual.toDual b]] = Finset.map OrderDual.toDual.toEmbedding [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>[[a, b]] = Finset.Icc a b
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>[[a, b]] = Finset.Icc b a
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>[[a, b]] = [[b, a]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>[[a, a]] = {a}
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>[[a, b]].Nonempty
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc a b ⊆ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc b a ⊆ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∈ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∈ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b x : α<VAR>ha : a ≤ x<VAR>hb : x ≤ b<GOAL>x ∈ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b x : α<VAR>hb : b ≤ x<VAR>ha : x ≤ a<GOAL>x ∈ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ∈ [[a₂, b₂]]<VAR>h₂ : b₁ ∈ [[a₂, b₂]]<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ∈ Finset.Icc a₂ b₂<VAR>hb : b₁ ∈ Finset.Icc a₂ b₂<GOAL>[[a₁, b₁]] ⊆ Finset.Icc a₂ b₂
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b x : α<VAR>h : x ∈ [[a, b]]<GOAL>[[x, b]] ⊆ [[a, b]]
<VAR>α : Type u_2<VAR>Lattice α<VAR>LocallyFiniteOrder α<VAR>a b x : α<VAR>h : x ∈ [[a, b]]<GOAL>[[a, x]] ⊆ [[a, b]]
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>a ∈ [[b, c]] → b ∈ [[a, c]] → a = b
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Function.Injective fun b => [[b, a]]
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Function.Injective (Finset.uIcc a)
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc (min a b) (max a b) = [[a, b]]
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : ¬a ≤ b<GOAL>[[a, b]] = Finset.Icc b a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : ¬b ≤ a<GOAL>[[a, b]] = Finset.Icc a b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>[[a, b]] = Finset.Icc a b ∪ Finset.Icc b a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>c < a → c < b → c ∉ [[a, b]]
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>a < c → b < c → c ∉ [[a, b]]
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>[[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>[[a, c]] ⊆ [[a, b]] ∪ [[b, c]]
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x ≤ y<GOAL>Relation.TransGen (fun x x_1 => x ⩿ x_1) x y
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>x y : α<GOAL>x ≤ y ↔ Relation.TransGen (fun x x_1 => x ⩿ x_1) x y
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>x y : α<GOAL>x ≤ y ↔ Relation.ReflTransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<GOAL>Relation.TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>x y : α<GOAL>x < y ↔ Relation.TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone f ↔ ∀ (a b : α), a ⩿ b → f b ≤ f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>Antitone f ↔ ∀ (a b : α), a ⋖ b → f b ≤ f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictAnti f ↔ ∀ (a b : α), a ⋖ b → f b < f a
<VAR>a b : ℤ<VAR>h : a ≤ b<VAR>P : Prop<VAR>h' : ∀ (n : ℕ), a + ↑n = b → P<GOAL>P
<VAR>a b : ℤ<VAR>h : a < b<VAR>P : Prop<VAR>h' : ∀ (n : ℕ), a + ↑n.succ = b → P<GOAL>P
<VAR>a b : ℤ<GOAL>-a * b = -(a * b)
<VAR>a b : ℤ<GOAL>a * -b = -(a * b)
<VAR>a b : ℤ<VAR>h : a * b = 0<GOAL>a = 0 ∨ b = 0
<VAR>n m : ℕ<GOAL>n * m = 0 → n = 0 ∨ m = 0
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n<GOAL>p n
<VAR>p : ℕ → Prop<VAR>a : ℕ<VAR>hz : p 0<VAR>hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p n.succ<GOAL>p a
<VAR>x : ℕ<VAR>d : Decidable (x % 2 = 1)<GOAL>(bif decide (x % 2 = 1) then 1 else 0) = x % 2
<VAR>α : Type u_1<GOAL>Function.Injective WithBot.some
<VAR>α : Type u_1<VAR>a b : α<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u_1<VAR>p : WithBot α → Prop<GOAL>(∀ (x : WithBot α), p x) ↔ p ⊥ ∧ ∀ (x : α), p ↑x
<VAR>α : Type u_1<VAR>p : WithBot α → Prop<GOAL>(∃ x, p x) ↔ p ⊥ ∨ ∃ x, p ↑x
<VAR>α : Type u_1<VAR>a : α<GOAL>some a = ↑a
<VAR>α : Type u_1<VAR>a : α<GOAL>⊥ ≠ ↑a
<VAR>α : Type u_1<VAR>a : α<GOAL>↑a ≠ ⊥
<VAR>α : Type u_1<VAR>C : WithBot α → Sort u_5<VAR>d : C ⊥<VAR>f : (a : α) → C ↑a<GOAL>WithBot.recBotCoe d f ⊥ = d
<VAR>α : Type u_1<VAR>C : WithBot α → Sort u_5<VAR>d : C ⊥<VAR>f : (a : α) → C ↑a<VAR>x : α<GOAL>WithBot.recBotCoe d f ↑x = f x
<VAR>α : Type u_5<VAR>d : α<GOAL>WithBot.unbot' d ⊥ = d
<VAR>α : Type u_5<VAR>d x : α<GOAL>WithBot.unbot' d ↑x = x
<VAR>α : Type u_1<VAR>d y : α<VAR>x : WithBot α<GOAL>WithBot.unbot' d x = y ↔ x = ↑y ∨ x = ⊥ ∧ y = d
<VAR>α : Type u_1<VAR>d : α<VAR>x : WithBot α<GOAL>WithBot.unbot' d x = d ↔ x = ↑d ∨ x = ⊥
<VAR>α : Type u_1<VAR>d : α<VAR>x y : WithBot α<GOAL>WithBot.unbot' d x = WithBot.unbot' d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>WithBot.map f ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>WithBot.map f ↑a = ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>g₁ : β → δ<VAR>g₂ : γ → δ<VAR>h : g₁ ∘ f₁ = g₂ ∘ f₂<VAR>a : α<GOAL>WithBot.map g₁ (WithBot.map f₁ ↑a) = WithBot.map g₂ (WithBot.map f₂ ↑a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>WithBot.map₂ f ↑a ↑b = ↑(f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>b : WithBot β<GOAL>WithBot.map₂ f ⊥ b = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithBot α<GOAL>WithBot.map₂ f a ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : WithBot β<GOAL>WithBot.map₂ f (↑a) b = WithBot.map (fun b => f a b) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithBot α<VAR>b : β<GOAL>WithBot.map₂ f a ↑b = WithBot.map (fun x => f x b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithBot α<VAR>b : WithBot β<GOAL>WithBot.map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
<VAR>α : Type u_1<VAR>x : WithBot α<GOAL>x ≠ ⊥ ↔ ∃ a, ↑a = x
<VAR>α : Type u_1<VAR>x : WithBot α<GOAL>(∀ (a : α), ↑a ≠ x) ↔ x = ⊥
<VAR>α : Type u_1<VAR>x : WithBot α<VAR>hx : x ≠ ⊥<GOAL>↑(x.unbot hx) = x
<VAR>α : Type u_1<VAR>x : α<VAR>h : ↑x ≠ ⊥ := ⋯<GOAL>(↑x).unbot h = x
<VAR>α : Type u_1<VAR>Top α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>Top α<VAR>a : α<GOAL>↑a = ⊤ ↔ a = ⊤
<VAR>α : Type u_1<VAR>Top α<VAR>a : α<GOAL>⊤ = ↑a ↔ ⊤ = a
<VAR>α : Type u_1<VAR>a b : α<VAR>LE α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>a b : α<VAR>LE α<GOAL>some a ≤ some b ↔ a ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<GOAL>none ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>¬↑a ≤ ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<GOAL>a ≤ ⊥ ↔ a = ⊥