ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<GOAL>Set.Iio ⊥ = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<GOAL>Set.Ici ⊥ = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>a : α<GOAL>Set.Icc ⊥ a = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>a : α<GOAL>Set.Ico ⊥ a = Set.Iio a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>Set.Icc ⊥ ⊤ = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a c : α<GOAL>c ∉ Set.Ici a ↔ c < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c : α<GOAL>c ∉ Set.Iic b ↔ b < c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a c : α<GOAL>c ∉ Set.Ioi a ↔ c ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c : α<GOAL>c ∉ Set.Iio b ↔ b ≤ c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>(Set.Iic a)ᶜ = Set.Ioi a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>(Set.Ici a)ᶜ = Set.Iio a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>(Set.Iio a)ᶜ = Set.Ici a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>(Set.Ioi a)ᶜ = Set.Iic a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ici a \ Set.Ici b = Set.Ico a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ici a \ Set.Ioi b = Set.Icc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a \ Set.Ioi b = Set.Ioc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a \ Set.Ici b = Set.Ioo a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iic b \ Set.Iic a = Set.Ioc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio b \ Set.Iic a = Set.Ioo a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iic b \ Set.Iio a = Set.Icc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio b \ Set.Iio a = Set.Ico a b
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>Function.Injective Set.Ioi
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>Function.Injective Set.Iio
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a = Set.Ioi b ↔ a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio a = Set.Iio b ↔ a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ < b₁<GOAL>Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ < b₁<GOAL>Set.Ioc a₁ b₁ ⊆ Set.Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>DenselyOrdered α<VAR>h₁ : a₁ < b₁<GOAL>Set.Ioo a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : a₁ < b₁ ∨ a₂ < b₂<GOAL>Set.Ico a₁ b₁ = Set.Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x : α<GOAL>Set.Ici x = {x} ↔ IsTop x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi b ⊆ Set.Ioi a ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>Set.Ioi b ⊆ Set.Ici a ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio a ⊆ Set.Iio b ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>Set.Iio a ⊆ Set.Iic b ↔ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iic b ∪ Set.Ioi a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iio b ∪ Set.Ici a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iic b ∪ Set.Ici a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iio b ∪ Set.Ioi a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Iic a ∪ Set.Ici a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Iio a ∪ Set.Ici a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Iic a ∪ Set.Ioi a = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Iio a ∪ Set.Ioi a = {a}ᶜ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c < b<GOAL>Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h : c < max a b<GOAL>Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a ⊆ Set.Ioo a b ∪ Set.Ici b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ioo a b ∪ Set.Ici b = Set.Ioi a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ici a ⊆ Set.Ico a b ∪ Set.Ici b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Ico a b ∪ Set.Ici b = Set.Ici a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c ≤ b<GOAL>Set.Ico a b ∪ Set.Ici c = Set.Ici (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h : c ≤ max a b<GOAL>Set.Ico a b ∪ Set.Ici c = Set.Ici (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ioi b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Ioc a b ∪ Set.Ioi b = Set.Ioi a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c ≤ b<GOAL>Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h : c ≤ max a b<GOAL>Set.Ioc a b ∪ Set.Ioi c = Set.Ioi (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ici a ⊆ Set.Icc a b ∪ Set.Ioi b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Icc a b ∪ Set.Ioi b = Set.Ici a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ici b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ioc a b ∪ Set.Ici b = Set.Ioi a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ici a ⊆ Set.Icc a b ∪ Set.Ici b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Icc a b ∪ Set.Ici b = Set.Ici a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : c ≤ b<GOAL>Set.Icc a b ∪ Set.Ici c = Set.Ici (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h : c ≤ max a b<GOAL>Set.Icc a b ∪ Set.Ici c = Set.Ici (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iic b ⊆ Set.Iio a ∪ Set.Icc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iio a ∪ Set.Icc a b = Set.Iic b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio b ⊆ Set.Iio a ∪ Set.Ico a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iio a ∪ Set.Ico a b = Set.Iio b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h₁ : c ≤ b<GOAL>Set.Iio b ∪ Set.Ico c d = Set.Iio (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h : min c d ≤ b<GOAL>Set.Iio b ∪ Set.Ico c d = Set.Iio (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iic b ⊆ Set.Iic a ∪ Set.Ioc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iic a ∪ Set.Ioc a b = Set.Iic b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h₁ : c < b<GOAL>Set.Iic b ∪ Set.Ioc c d = Set.Iic (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h : min c d < b<GOAL>Set.Iic b ∪ Set.Ioc c d = Set.Iic (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio b ⊆ Set.Iic a ∪ Set.Ioo a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iic a ∪ Set.Ioo a b = Set.Iio b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h₁ : c < b<GOAL>Set.Iio b ∪ Set.Ioo c d = Set.Iio (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h : min c d < b<GOAL>Set.Iio b ∪ Set.Ioo c d = Set.Iio (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iic b ⊆ Set.Iic a ∪ Set.Icc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.Iic a ∪ Set.Icc a b = Set.Iic b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h₁ : c ≤ b<GOAL>Set.Iic b ∪ Set.Icc c d = Set.Iic (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b c d : α<VAR>h : min c d ≤ b<GOAL>Set.Iic b ∪ Set.Icc c d = Set.Iic (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio b ⊆ Set.Iic a ∪ Set.Ico a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iic a ∪ Set.Ico a b = Set.Iio b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioo a c ⊆ Set.Ioo a b ∪ Set.Ico b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : b ≤ c<GOAL>Set.Ioo a b ∪ Set.Ico b c = Set.Ioo a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<GOAL>Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Icc a c ⊆ Set.Ico a b ∪ Set.Icc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Set.Ico a b ∪ Set.Icc b c = Set.Icc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a c ⊆ Set.Ioo a b ∪ Set.Icc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : b ≤ c<GOAL>Set.Ioo a b ∪ Set.Icc b c = Set.Ioc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioo a c ⊆ Set.Ioc a b ∪ Set.Ioo b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b < c<GOAL>Set.Ioc a b ∪ Set.Ioo b c = Set.Ioo a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ico a c ⊆ Set.Icc a b ∪ Set.Ioo b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b < c<GOAL>Set.Icc a b ∪ Set.Ioo b c = Set.Ico a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Icc a c ⊆ Set.Icc a b ∪ Set.Ioc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Set.Icc a b ∪ Set.Ioc b c = Set.Icc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a c ⊆ Set.Ioc a b ∪ Set.Ioc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<GOAL>Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : min a b ≤ max c d<VAR>h₂ : min c d ≤ max a b<GOAL>Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioo a c ⊆ Set.Ioc a b ∪ Set.Ico b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : b < c<GOAL>Set.Ioc a b ∪ Set.Ico b c = Set.Ioo a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ico a c ⊆ Set.Icc a b ∪ Set.Ico b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b < c<GOAL>Set.Icc a b ∪ Set.Ico b c = Set.Ico a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Icc a c ⊆ Set.Icc a b ∪ Set.Icc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ b<VAR>h₂ : b ≤ c<GOAL>Set.Icc a b ∪ Set.Icc b c = Set.Icc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : c ≤ b<VAR>h₂ : a ≤ d<GOAL>Set.Icc a b ∪ Set.Icc c d = Set.Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : min a b < max c d<VAR>h₂ : min c d < max a b<GOAL>Set.Icc a b ∪ Set.Icc c d = Set.Icc (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a c ⊆ Set.Ioc a b ∪ Set.Icc b c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>h₁ : a < b<VAR>h₂ : b ≤ c<GOAL>Set.Ioc a b ∪ Set.Icc b c = Set.Ioc a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : c < b<VAR>h₂ : a < d<GOAL>Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : min a b < max c d<VAR>h₂ : min c d < max a b<GOAL>Set.Ioo a b ∪ Set.Ioo c d = Set.Ioo (min a c) (max b d)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b : α<GOAL>Set.Iic a ∩ Set.Iic b = Set.Iic (a ⊓ b)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>Set.Ioc a b ∩ Set.Iic c = Set.Ioc a (b ⊓ c)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b : α<GOAL>Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>Set.Ico a b ∩ Set.Ici c = Set.Ico (a ⊔ c) b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.Icc a₁ b₁ ∩ Set.Icc a₂ b₂ = Set.Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Set.Icc a b ∩ Set.Icc b c = {b}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioi a ∩ Set.Ioi b = Set.Ioi (a ⊔ b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Iio a ∩ Set.Iio b = Set.Iio (a ⊓ b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.Ico a₁ b₁ ∩ Set.Ico a₂ b₂ = Set.Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.Ioc a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.Ioo a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioo a b ∩ Set.Iio c = Set.Ioo a (min b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Iio a ∩ Set.Ioo b c = Set.Ioo b (min a c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioo a b ∩ Set.Ioi c = Set.Ioo (max a c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : b₁ < b₂<GOAL>Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioc (max a₁ a₂) b₁
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : b₂ ≤ b₁<GOAL>Set.Ioc a₁ b₁ ∩ Set.Ioo a₂ b₂ = Set.Ioo (max a₁ a₂) b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioo (max a₁ a₂) b₁
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h : b₂ < b₁<GOAL>Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (max a₁ a₂) b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ico a b \ Set.Iio c = Set.Ico (max a c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a b \ Set.Ioi c = Set.Ioc a (min b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a b ∩ Set.Ioi c = Set.Ioc (a ⊔ c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ico a b ∩ Set.Iio c = Set.Ico a (min b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a b \ Set.Iic c = Set.Ioc (max a c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a b ∪ Set.Ioc a c = Set.Ioc a (max b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a c ∪ Set.Ioc b c = Set.Ioc (min a b) c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioc a b ∪ Set.Ioc b a = Set.Ioc (min a b) (max a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.Ioc a b ∪ Set.Ioc b c ∪ Set.Ioc c a = Set.Ioc (min a (min b c)) (max a (max b c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>Set.Iic a ×ˢ Set.Iic b = Set.Iic (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>Set.Ici a ×ˢ Set.Ici b = Set.Ici (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α × β<GOAL>Set.Ici a = Set.Ici a.1 ×ˢ Set.Ici a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α × β<GOAL>Set.Iic a = Set.Iic a.1 ×ˢ Set.Iic a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Set.Icc a₁ a₂ ×ˢ Set.Icc b₁ b₂ = Set.Icc (a₁, b₁) (a₂, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α × β<GOAL>Set.Icc a b = Set.Icc a.1 b.1 ×ˢ Set.Icc a.2 b.2
<VAR>α : Sort u<VAR>p : α → Prop<GOAL>(x : α) ×' p x → ∃ x, p x
<VAR>α : Type u<VAR>β : α → Type v<VAR>p₁ p₂ : (a : α) × β a<VAR>h₁ : p₁.fst = p₂.fst<GOAL>Eq.recOn h₁ p₁.snd = p₂.snd → p₁ = p₂
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>p₁ p₂ : (a : α) ×' β a<VAR>h₁ : p₁.fst = p₂.fst<GOAL>Eq.recOn h₁ p₁.snd = p₂.snd → p₁ = p₂
<VAR>α : Type u<VAR>a y : α<VAR>l : List α<GOAL>(a ∈ y :: l) = (a = y ∨ a ∈ l)
<VAR>α : Type u<VAR>p : α → Prop<GOAL>¬∃ x, x ∈ [] ∧ p x
<VAR>α : Type u<VAR>β : Type v<VAR>σ : Type w₂<VAR>f : α → σ → σ × β<VAR>x : List α<VAR>s : σ<GOAL>(List.mapAccumr f x s).snd.length = x.length
<VAR>α : Type u<VAR>β : Type v<VAR>φ : Type w₁<VAR>σ : Type w₂<VAR>f : α → β → σ → σ × φ<VAR>x : List α<VAR>y : List β<VAR>c : σ<GOAL>(List.mapAccumr₂ f x y c).snd.length = min x.length y.length
<VAR>α : Type u<VAR>a b : Set α<VAR>h : ∀ (x : α), x ∈ a ↔ x ∈ b<GOAL>a = b
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>↑i = ↑j → i = j
<VAR>n : ℕ<VAR>i j : Fin n<GOAL>i = j → ↑i = ↑j
<VAR>n : ℕ<VAR>i j : Fin n<VAR>h : ↑i ≠ ↑j<GOAL>i ≠ j
<VAR>n : ℕ<VAR>i j : Fin n<VAR>h : i ≠ j<GOAL>↑i ≠ ↑j
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>InfIrred (UpperSet.Ici a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : UpperSet α<VAR>Finite α<GOAL>InfIrred s ↔ ∃ a, UpperSet.Ici a = s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>SupIrred (LowerSet.Iic a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : LowerSet α<VAR>Finite α<GOAL>SupIrred s ↔ ∃ a, LowerSet.Iic a = s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>OrderEmbedding.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>OrderEmbedding.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Finite α<GOAL>Function.Surjective ⇑OrderEmbedding.supIrredLowerSet
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Finite α<GOAL>Function.Surjective ⇑OrderEmbedding.infIrredUpperSet
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Finite α<VAR>a : α<GOAL>OrderIso.supIrredLowerSet a = ⟨LowerSet.Iic a, ⋯⟩
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Finite α<VAR>a : α<GOAL>OrderIso.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>Finite α<VAR>s : { s // SupIrred s }<VAR>Fintype ↥↑s<GOAL>OrderIso.supIrredLowerSet.symm s = (↑↑s).toFinset.sup id
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>Finite α<VAR>s : { s // InfIrred s }<VAR>Fintype ↥↑s<GOAL>OrderIso.infIrredUpperSet.symm s = (↑↑s).toFinset.inf id
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>a : α<GOAL>↑(OrderEmbedding.birkhoffFinset a) = OrderEmbedding.birkhoffSet a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>a b : α<GOAL>OrderEmbedding.birkhoffSet (a ⊔ b) = OrderEmbedding.birkhoffSet a ∪ OrderEmbedding.birkhoffSet b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>a b : α<GOAL>OrderEmbedding.birkhoffSet (a ⊓ b) = OrderEmbedding.birkhoffSet a ∩ OrderEmbedding.birkhoffSet b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>DecidableEq α<VAR>a b : α<GOAL>OrderEmbedding.birkhoffFinset (a ⊔ b) = OrderEmbedding.birkhoffFinset a ∪ OrderEmbedding.birkhoffFinset b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>DecidableEq α<VAR>a b : α<GOAL>OrderEmbedding.birkhoffFinset (a ⊓ b) = OrderEmbedding.birkhoffFinset a ∩ OrderEmbedding.birkhoffFinset b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>Fintype α<VAR>DecidablePred SupIrred<VAR>a : α<GOAL>OrderEmbedding.birkhoffSet a = ↑(OrderIso.lowerSetSupIrred a)
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>Fintype α<VAR>DecidablePred SupIrred<GOAL>Function.Injective ⇑LatticeHom.birkhoffFinset
<VAR>α : Type u<VAR>Finite α<VAR>DistribLattice α<GOAL>∃ β x x_1 f, Function.Injective ⇑f
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Icc a b).Nonempty ↔ a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ico a b).Nonempty ↔ a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Finset.Ioc a b).Nonempty ↔ a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>(Finset.Ioo a b).Nonempty ↔ a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Icc a b = ∅ ↔ ¬a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ico a b = ∅ ↔ ¬a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioc a b = ∅ ↔ ¬a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>Finset.Ioo a b = ∅ ↔ ¬a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>Finset.Ioo a b = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b < a<GOAL>Finset.Icc a b = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Finset.Ico a b = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Finset.Ioc a b = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Finset.Ioo a b = ∅
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∈ Finset.Icc a b ↔ a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∈ Finset.Ico a b ↔ a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∈ Finset.Icc a b ↔ a ≤ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∈ Finset.Ioc a b ↔ a < b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∉ Finset.Ioc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∉ Finset.Ioo a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∉ Finset.Ico a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∉ Finset.Ioo a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ 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>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Finset.Ioc a₁ b₁ ⊆ Finset.Ioc a₂ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Finset.Ioo a₁ b₁ ⊆ Finset.Ioo a₂ b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Finset.Icc a₂ b ⊆ Finset.Icc a₁ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Finset.Ico a₂ b ⊆ Finset.Ico a₁ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Finset.Ioc a₂ b ⊆ Finset.Ioc a₁ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b : α<VAR>h : a₁ ≤ a₂<GOAL>Finset.Ioo a₂ b ⊆ Finset.Ioo a₁ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Finset.Icc a b₁ ⊆ Finset.Icc a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Finset.Ico a b₁ ⊆ Finset.Ico a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Finset.Ioc a b₁ ⊆ Finset.Ioc a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ ≤ b₂<GOAL>Finset.Ioo a b₁ ⊆ Finset.Ioo a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b : α<VAR>h : a₁ < a₂<GOAL>Finset.Ico a₂ b ⊆ Finset.Ioo a₁ b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ < b₂<GOAL>Finset.Ioc a b₁ ⊆ Finset.Ioo a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b₁ b₂ : α<VAR>h : b₁ < b₂<GOAL>Finset.Icc a b₁ ⊆ Finset.Ico a b₂
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo a b ⊆ Finset.Ico a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo a b ⊆ Finset.Ioc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ico a b ⊆ Finset.Icc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioc a b ⊆ Finset.Icc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Finset.Ioo a b ⊆ Finset.Icc a b
<VAR>α : Type u_2<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ≤ b₁<GOAL>Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂