ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) (Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) (Set.Ico a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a x : α<GOAL>↑(Set.projIci a x) = max a x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b x : α<GOAL>↑(Set.projIic b x) = min b x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<GOAL>↑(Set.projIcc a b h x) = max a (min b x)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a x : α<VAR>hx : x ≤ a<GOAL>Set.projIci a x = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b x : α<VAR>hx : b ≤ x<GOAL>Set.projIic b x = ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>hx : x ≤ a<GOAL>Set.projIcc a b h x = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>hx : b ≤ x<GOAL>Set.projIcc a b h x = ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.projIci a a = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<GOAL>Set.projIic b b = ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.projIcc a b h a = ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.projIcc a b h b = ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a x : α<GOAL>Set.projIci a x = ⟨a, ⋯⟩ ↔ x ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b x : α<GOAL>Set.projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b x : α<VAR>h : a < b<GOAL>Set.projIcc a b ⋯ x = ⟨a, ⋯⟩ ↔ x ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b x : α<VAR>h : a < b<GOAL>Set.projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a x : α<VAR>hx : x ∈ Set.Ici a<GOAL>Set.projIci a x = ⟨x, hx⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b x : α<VAR>hx : x ∈ Set.Iic b<GOAL>Set.projIic b x = ⟨x, hx⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>hx : x ∈ Set.Icc a b<GOAL>Set.projIcc a b h x = ⟨x, hx⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>x : ↑(Set.Ici a)<GOAL>Set.projIci a ↑x = x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<VAR>x : ↑(Set.Iic b)<GOAL>Set.projIic b ↑x = x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : ↑(Set.Icc a b)<GOAL>Set.projIcc a b h ↑x = x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.SurjOn (Set.projIci a) (Set.Ici a) Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<GOAL>Set.SurjOn (Set.projIic b) (Set.Iic b) Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.SurjOn (Set.projIcc a b h) (Set.Icc a b) Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Function.Surjective (Set.projIci a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<GOAL>Function.Surjective (Set.projIic b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Function.Surjective (Set.projIcc a b h)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.range (Set.projIci a) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Set.range (Set.projIic a) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.range (Set.projIcc a b h) = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Monotone (Set.projIci a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Monotone (Set.projIic a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Monotone (Set.projIcc a b h)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>StrictMonoOn (Set.projIci a) (Set.Ici a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<GOAL>StrictMonoOn (Set.projIic b) (Set.Iic b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>StrictMonoOn (Set.projIcc a b h) (Set.Icc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<VAR>x : α<GOAL>Set.IciExtend f x = f ⟨max a x, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<VAR>x : α<GOAL>Set.IicExtend f x = f ⟨min b x, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<VAR>x : α<GOAL>Set.IccExtend h f x = f ⟨max a (min b x), ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<GOAL>Set.range (Set.IciExtend f) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<GOAL>Set.range (Set.IicExtend f) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<GOAL>Set.range (Set.IccExtend h f) = Set.range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a x : α<VAR>f : ↑(Set.Ici a) → β<VAR>hx : x ≤ a<GOAL>Set.IciExtend f x = f ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b x : α<VAR>f : ↑(Set.Iic b) → β<VAR>hx : b ≤ x<GOAL>Set.IicExtend f x = f ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Set.Icc a b) → β<VAR>hx : x ≤ a<GOAL>Set.IccExtend h f x = f ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Set.Icc a b) → β<VAR>hx : b ≤ x<GOAL>Set.IccExtend h f x = f ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<GOAL>Set.IciExtend f a = f ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<GOAL>Set.IicExtend f b = f ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<GOAL>Set.IccExtend h f a = f ⟨a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<GOAL>Set.IccExtend h f b = f ⟨b, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a x : α<VAR>f : ↑(Set.Ici a) → β<VAR>hx : x ∈ Set.Ici a<GOAL>Set.IciExtend f x = f ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b x : α<VAR>f : ↑(Set.Iic b) → β<VAR>hx : x ∈ Set.Iic b<GOAL>Set.IicExtend f x = f ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>f : ↑(Set.Icc a b) → β<VAR>hx : x ∈ Set.Icc a b<GOAL>Set.IccExtend h f x = f ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<VAR>x : ↑(Set.Ici a)<GOAL>Set.IciExtend f ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<VAR>x : ↑(Set.Iic b)<GOAL>Set.IicExtend f ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<VAR>x : ↑(Set.Icc a b)<GOAL>Set.IccExtend h f ↑x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : α → β<VAR>ha : ∀ x < a, f x = f a<VAR>hb : ∀ (x : α), b < x → f x = f b<GOAL>Set.IccExtend h (f ∘ Subtype.val) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<VAR>hf : Monotone f<GOAL>Monotone (Set.IciExtend f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<VAR>hf : Monotone f<GOAL>Monotone (Set.IicExtend f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<VAR>hf : Monotone f<GOAL>Monotone (Set.IccExtend h f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : ↑(Set.Ici a) → β<VAR>hf : StrictMono f<GOAL>StrictMonoOn (Set.IciExtend f) (Set.Ici a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>b : α<VAR>f : ↑(Set.Iic b) → β<VAR>hf : StrictMono f<GOAL>StrictMonoOn (Set.IicExtend f) (Set.Iic b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a b : α<VAR>h : a ≤ b<VAR>f : ↑(Set.Icc a b) → β<VAR>hf : StrictMono f<GOAL>StrictMonoOn (Set.IccExtend h f) (Set.Icc a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>s : Set ↑(Set.Ici a)<VAR>hs : s.OrdConnected<GOAL>{x | Set.IciExtend (fun x => x ∈ s) x}.OrdConnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>b : α<VAR>s : Set ↑(Set.Iic b)<VAR>hs : s.OrdConnected<GOAL>{x | Set.IicExtend (fun x => x ∈ s) x}.OrdConnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<VAR>hs : s.OrdConnected<GOAL>{x | t.restrict (fun x => x ∈ s) x}.OrdConnected
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑(a ⊔ b) = ↑a ⊔ ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑(max a b) = max ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>↑(min a b) = min ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.Icc a b = Finset.fin n (Finset.Icc ↑a ↑b)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.Ico a b = Finset.fin n (Finset.Ico ↑a ↑b)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.Ioc a b = Finset.fin n (Finset.Ioc ↑a ↑b)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.Ioo a b = Finset.fin n (Finset.Ioo ↑a ↑b)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.uIcc a b = Finset.fin n (Finset.uIcc ↑a ↑b)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Icc a b) = Finset.Icc ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Ico a b) = Finset.Ico ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Ioc a b) = Finset.Ioc ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Finset.Icc a b).card = ↑b + 1 - ↑a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Finset.Ico a b).card = ↑b - ↑a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Finset.Ioc a b).card = ↑b - ↑a
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Finset.Ioo a b).card = ↑b - ↑a - 1
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(Finset.uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Finset.Ici a = Finset.fin n (Finset.Icc (↑a) n)
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Finset.Ioi a = Finset.fin n (Finset.Ioc (↑a) n)
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Finset.Iic b = Finset.fin n (Finset.Iic ↑b)
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Finset.Iio b = Finset.fin n (Finset.Iio ↑b)
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Ici a) = Finset.Icc (↑a) (n - 1)
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Ioi a) = Finset.Ioc (↑a) (n - 1)
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Iic b) = Finset.Iic ↑b
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Finset.map Fin.valEmbedding (Finset.Iio b) = Finset.Iio ↑b
<VAR>n : ℕ<VAR>a : Fin n<GOAL>(Finset.Ici a).card = n - ↑a
<VAR>n : ℕ<VAR>a : Fin n<GOAL>(Finset.Ioi a).card = n - 1 - ↑a
<VAR>n : ℕ<VAR>b : Fin n<GOAL>(Finset.Iic b).card = ↑b + 1
<VAR>n : ℕ<VAR>b : Fin n<GOAL>(Finset.Iio b).card = ↑b
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Fintype.card ↑(Set.Ici a) = n - ↑a
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Fintype.card ↑(Set.Iic b) = ↑b + 1
<VAR>n : ℕ<VAR>b : Fin n<GOAL>Fintype.card ↑(Set.Iio b) = ↑b
<VAR>α : Type u_7<VAR>LE α<VAR>self : NonemptyInterval α<GOAL>self.toProd.1 ≤ self.toProd.2
<VAR>α : Type u_1<VAR>LE α<GOAL>Function.Injective NonemptyInterval.toProd
<VAR>α : Type u_1<VAR>LE α<VAR>s : NonemptyInterval α<GOAL>s.toDualProd = (OrderDual.toDual s.toProd.1, s.toProd.2)
<VAR>α : Type u_1<VAR>LE α<GOAL>Function.Injective NonemptyInterval.toDualProd
<VAR>α : Type u_1<VAR>LE α<VAR>s t : NonemptyInterval α<GOAL>s ≤ t ↔ t.toProd.1 ≤ s.toProd.1 ∧ s.toProd.2 ≤ t.toProd.2
<VAR>α : Type u_1<VAR>LE α<GOAL>∀ (a : NonemptyInterval α), NonemptyInterval.toDualProdHom a = a.toDualProd
<VAR>α : Type u_1<VAR>LE α<VAR>s : NonemptyInterval α<GOAL>(NonemptyInterval.dual s).toProd.1 = OrderDual.toDual s.toProd.2
<VAR>α : Type u_1<VAR>LE α<VAR>s : NonemptyInterval α<GOAL>(NonemptyInterval.dual s).toProd.2 = OrderDual.toDual s.toProd.1
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α × α<VAR>a : α<VAR>hx : x.1 ≤ x.2<GOAL>a ∈ { toProd := x, fst_le_snd := hx } ↔ x.1 ≤ a ∧ a ≤ x.2
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : NonemptyInterval α<VAR>a : α<GOAL>a ∈ s ↔ s.toProd.1 ≤ a ∧ a ≤ s.toProd.2
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : NonemptyInterval α<GOAL>(Set.Icc s.toProd.1 s.toProd.2).Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(NonemptyInterval.pure a).toProd.2 = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(NonemptyInterval.pure a).toProd.1 = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>a ∈ NonemptyInterval.pure a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Function.Injective NonemptyInterval.pure
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>NonemptyInterval.dual (NonemptyInterval.pure a) = NonemptyInterval.pure (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : NonemptyInterval α<GOAL>(NonemptyInterval.map f a).toProd.1 = f a.1.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : NonemptyInterval α<GOAL>(NonemptyInterval.map f a).toProd.2 = f a.1.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : α<GOAL>NonemptyInterval.map f (NonemptyInterval.pure a) = NonemptyInterval.pure (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<VAR>a : NonemptyInterval α<GOAL>NonemptyInterval.map g (NonemptyInterval.map f a) = NonemptyInterval.map (g.comp f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : NonemptyInterval α<GOAL>NonemptyInterval.dual (NonemptyInterval.map f a) = NonemptyInterval.map (OrderHom.dual f) (NonemptyInterval.dual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>h₀ : ∀ (b : β), Monotone fun a => f a b<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.1 = f a.toProd.1 a_1.toProd.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>h₀ : ∀ (b : β), Monotone fun a => f a b<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>∀ (a : NonemptyInterval α) (a_1 : NonemptyInterval β), (NonemptyInterval.map₂ f h₀ h₁ a a_1).toProd.2 = f a.toProd.2 a_1.toProd.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>h₀ : ∀ (b : β), Monotone fun a => f a b<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>a : α<VAR>b : β<GOAL>NonemptyInterval.map₂ f h₀ h₁ (NonemptyInterval.pure a) (NonemptyInterval.pure b) = NonemptyInterval.pure (f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>h₀ : ∀ (b : β), Monotone fun a => f a b<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>s : NonemptyInterval α<VAR>t : NonemptyInterval β<GOAL>NonemptyInterval.dual (NonemptyInterval.map₂ f h₀ h₁ s t) = NonemptyInterval.map₂ (fun a b => OrderDual.toDual (f (OrderDual.ofDual a) (OrderDual.ofDual b))) ⋯ ⋯ (NonemptyInterval.dual s) (NonemptyInterval.dual t)
<VAR>α : Type u_1<VAR>Preorder α<VAR>BoundedOrder α<GOAL>NonemptyInterval.dual ⊤ = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : NonemptyInterval α<GOAL>↑s ⊆ ↑t ↔ s ≤ t
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : NonemptyInterval α<GOAL>↑s ⊂ ↑t ↔ s < t
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>⇑NonemptyInterval.coeHom = SetLike.coe
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : NonemptyInterval α<GOAL>↑s = Set.Icc s.toProd.1 s.toProd.2
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>↑(NonemptyInterval.pure a) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>b ∈ NonemptyInterval.pure a ↔ b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : NonemptyInterval α<GOAL>↑(NonemptyInterval.dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α →o β<VAR>s : NonemptyInterval α<GOAL>⇑f '' ↑s ⊆ ↑(NonemptyInterval.map f s)
<VAR>α : Type u_1<VAR>Lattice α<VAR>s t : NonemptyInterval α<GOAL>(s ⊔ t).toProd.1 = s.toProd.1 ⊓ t.toProd.1
<VAR>α : Type u_1<VAR>Lattice α<VAR>s t : NonemptyInterval α<GOAL>(s ⊔ t).toProd.2 = s.toProd.2 ⊔ t.toProd.2
<VAR>α : Type u_1<VAR>LE α<GOAL>Function.Injective WithBot.some
<VAR>α : Type u_1<VAR>LE α<VAR>s t : NonemptyInterval α<GOAL>↑s = ↑t ↔ s = t
<VAR>α : Type u_1<VAR>LE α<VAR>p : Interval α → Prop<GOAL>(∀ (s : Interval α), p s) ↔ p ⊥ ∧ ∀ (s : NonemptyInterval α), p ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>p : Interval α → Prop<GOAL>(∃ s, p s) ↔ p ⊥ ∨ ∃ s, p ↑s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Function.Injective Interval.pure
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Interval.dual (Interval.pure a) = Interval.pure (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Interval.dual ⊥ = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Interval.pure a ≠ ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>⊥ ≠ Interval.pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : α<GOAL>Interval.map f (Interval.pure a) = Interval.pure (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<VAR>s : Interval α<GOAL>Interval.map g (Interval.map f s) = Interval.map (g.comp f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>s : Interval α<GOAL>Interval.dual (Interval.map f s) = Interval.map (OrderHom.dual f) (Interval.dual s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>BoundedOrder α<GOAL>Interval.dual ⊤ = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Interval α<GOAL>↑s ⊆ ↑t ↔ s ≤ t
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s t : Interval α<GOAL>↑s ⊂ ↑t ↔ s < t
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>↑(Interval.pure a) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : NonemptyInterval α<GOAL>↑↑s = ↑s
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>↑⊥ = ∅
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Interval α<GOAL>↑(Interval.dual s) = ⇑OrderDual.ofDual ⁻¹' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α →o β<VAR>s : Interval α<GOAL>⇑f '' ↑s ⊆ ↑(Interval.map f s)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>b ∈ Interval.pure a ↔ b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>a ∈ Interval.pure a
<VAR>α : Type u_1<VAR>Lattice α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Interval α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>Lattice α<VAR>s t : Interval α<GOAL>Disjoint ↑s ↑t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑(NonemptyInterval.pure a) = Interval.pure a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : NonemptyInterval α<VAR>a : α<GOAL>↑s = Interval.pure a ↔ s = NonemptyInterval.pure a
<VAR>α : Type u_1<VAR>Preorder α<VAR>BoundedOrder α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : NonemptyInterval α<VAR>x : α<GOAL>x ∈ ↑s ↔ x ∈ s
<VAR>α : Type u_1<VAR>Lattice α<VAR>s t : NonemptyInterval α<GOAL>↑(s ⊔ t) = ↑s ⊔ ↑t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>S : Set (Interval α)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>CompleteLattice α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>f : ι → Interval α<GOAL>↑(⨅ i, f i) = ⋂ i, ↑(f i)
<VAR>α : Type u_1<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>CompleteLattice α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>f : (i : ι) → κ i → Interval α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>AntisymmRel (Function.swap r) = AntisymmRel r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>a : α<GOAL>AntisymmRel r a a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>AntisymmRel r a b → AntisymmRel r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>a b c : α<VAR>hab : AntisymmRel r a b<VAR>hbc : AntisymmRel r b c<GOAL>AntisymmRel r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>IsAntisymm α r<VAR>a b : α<GOAL>AntisymmRel r a b ↔ a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsPreorder α r<VAR>a b : α<GOAL>Setoid.r a b = AntisymmRel r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsPreorder α r<VAR>p : Antisymmetrization α r → Prop<GOAL>(∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsPreorder α r<VAR>p : Antisymmetrization α r → Prop<VAR>a : Antisymmetrization α r<VAR>h : ∀ (a : α), p (toAntisymmetrization r a)<GOAL>p a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsPreorder α r<VAR>a : Antisymmetrization α r<GOAL>toAntisymmetrization r (ofAntisymmetrization r a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a b : α<VAR>h : AntisymmRel (fun x x_1 => x ≤ x_1) a b<VAR>f : α → β<VAR>hf : Monotone f<GOAL>AntisymmRel (fun x x_1 => x ≤ x_1) (f a) (f b)
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x ≤ x_1)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Acc (fun x x_1 => x < x_1) (toAntisymmetrization (fun x x_1 => x ≤ x_1) a) ↔ Acc (fun x x_1 => x < x_1) a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>WellFounded LT.lt ↔ WellFounded LT.lt
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>toAntisymmetrization (fun x x_1 => x ≤ x_1) a ≤ toAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>toAntisymmetrization (fun x x_1 => x ≤ x_1) a < toAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Antisymmetrization α fun x x_1 => x ≤ x_1<GOAL>ofAntisymmetrization (fun x x_1 => x ≤ x_1) a ≤ ofAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Antisymmetrization α fun x x_1 => x ≤ x_1<GOAL>ofAntisymmetrization (fun x x_1 => x ≤ x_1) a < ofAntisymmetrization (fun x x_1 => x ≤ x_1) b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Monotone (toAntisymmetrization fun x x_1 => x ≤ x_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>(Setoid.r ⇒ Setoid.r) ⇑f ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>⇑f.antisymmetrization = Quotient.map' ⇑f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : Antisymmetrization α fun x x_1 => x ≤ x_1<GOAL>f.antisymmetrization a = Quotient.map' ⇑f ⋯ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<VAR>a : α<GOAL>f.antisymmetrization (toAntisymmetrization (fun x x_1 => x ≤ x_1) a) = toAntisymmetrization (fun x x_1 => x ≤ x_1) (f a)
<VAR>α : Type u_1<VAR>Preorder α<GOAL>∀ (a : Antisymmetrization α fun x x_1 => x ≤ x_1), (OrderEmbedding.ofAntisymmetrization α) a = ofAntisymmetrization (fun x x_1 => x ≤ x_1) a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(OrderIso.dualAntisymmetrization α) (OrderDual.toDual (toAntisymmetrization (fun x x_1 => x ≤ x_1) a)) = toAntisymmetrization (fun x x_1 => x ≤ x_1) (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>(OrderIso.dualAntisymmetrization α).symm (toAntisymmetrization (fun x x_1 => x ≤ x_1) (OrderDual.toDual a)) = OrderDual.toDual (toAntisymmetrization (fun x x_1 => x ≤ x_1) a)
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>Set.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Set.uIcc a b = Set.Icc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Set.uIcc a b = Set.Icc b a
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>Set.uIcc a b = Set.uIcc b a
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<VAR>h : a < b<GOAL>Set.uIcc a b = Set.Icc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<VAR>h : b < a<GOAL>Set.uIcc a b = Set.Icc b a
<VAR>α : Type u_1<VAR>Lattice α<VAR>a : α<GOAL>Set.uIcc a a = {a}
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>(Set.uIcc a b).Nonempty
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>Set.Icc a b ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>Set.Icc b a ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>a ∈ Set.uIcc a b