ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b : α<GOAL>b ∈ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b x : α<VAR>ha : a ≤ x<VAR>hb : x ≤ b<GOAL>x ∈ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b x : α<VAR>hb : b ≤ x<VAR>ha : x ≤ a<GOAL>x ∈ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a₁ a₂ b₁ b₂ : α<VAR>h₁ : a₁ ∈ Set.uIcc a₂ b₂<VAR>h₂ : b₁ ∈ Set.uIcc a₂ b₂<GOAL>Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂
<VAR>α : Type u_1<VAR>Lattice α<VAR>a₁ a₂ b₁ b₂ : α<VAR>ha : a₁ ∈ Set.Icc a₂ b₂<VAR>hb : b₁ ∈ Set.Icc a₂ b₂<GOAL>Set.uIcc a₁ b₁ ⊆ Set.Icc a₂ b₂
<VAR>α : Type u_1<VAR>Lattice α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₁ ∈ Set.uIcc a₂ b₂ ∧ b₁ ∈ Set.uIcc a₂ b₂
<VAR>α : Type u_1<VAR>Lattice α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b x : α<VAR>h : x ∈ Set.uIcc a b<GOAL>Set.uIcc x b ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>a b x : α<VAR>h : x ∈ Set.uIcc a b<GOAL>Set.uIcc a x ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>s : Set α<GOAL>BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Lattice β<VAR>a₁ a₂ : α<VAR>b₁ b₂ : β<GOAL>Set.uIcc a₁ a₂ ×ˢ Set.uIcc b₁ b₂ = Set.uIcc (a₁, b₁) (a₂, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Lattice β<VAR>a b : α × β<GOAL>Set.uIcc a b = Set.uIcc a.1 b.1 ×ˢ Set.uIcc a.2 b.2
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>a b c : α<VAR>ha : a ∈ Set.uIcc b c<VAR>hb : b ∈ Set.uIcc a c<GOAL>a = b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>a b c : α<GOAL>b ∈ Set.uIcc a c → c ∈ Set.uIcc a b → b = c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>a : α<GOAL>Function.Injective fun b => Set.uIcc b a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>a : α<GOAL>Function.Injective (Set.uIcc a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : MonotoneOn f (Set.uIcc a b)<GOAL>Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : AntitoneOn f (Set.uIcc a b)<GOAL>Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : Monotone f<GOAL>Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : Antitone f<GOAL>Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : MonotoneOn f (Set.uIcc a b)<GOAL>f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : AntitoneOn f (Set.uIcc a b)<GOAL>f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : Monotone f<GOAL>f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>f : α → β<VAR>a b : α<VAR>hf : Antitone f<GOAL>f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Icc (min a b) (max a b) = Set.uIcc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬a ≤ b<GOAL>Set.uIcc a b = Set.Icc b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬b ≤ a<GOAL>Set.uIcc a b = Set.Icc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ∈ Set.uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>ha : c < a<VAR>hb : c < b<GOAL>c ∉ Set.uIcc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>ha : a < c<VAR>hb : b < c<GOAL>c ∉ Set.uIcc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<GOAL>Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<GOAL>MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Ι a b = Set.Ioc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Ι a b = Set.Ioc b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Ι a b = Set.Ioc a b ∪ Set.Ioc b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>a ∈ Ι a b ↔ b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>b ∈ Ι a b ↔ a < b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>P : α → Prop<GOAL>(∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Set.Ioc a b, P x) ∧ ∀ x ∈ Set.Ioc b a, P x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c d : α<VAR>h : Set.uIcc a b ⊆ Set.uIcc c d<GOAL>Ι a b ⊆ Ι c d
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Ι a b = Ι b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ Ι a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ Ι b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>Ι a b ⊆ Set.uIcc a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ∈ Ι b c → b ∈ Ι a c → a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<GOAL>b ∈ Ι a c → c ∈ Ι a b → b = c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b c : α<VAR>ha : a ≤ c<VAR>hb : b ≤ c<GOAL>a ∉ Ι b c → b ∉ Ι a c → a = b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Function.Injective fun b => Ι b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<GOAL>Function.Injective (Ι a)
<VAR>α : Type u_1<GOAL>OrderDual.toDual.symm = OrderDual.ofDual
<VAR>α : Type u_1<GOAL>OrderDual.ofDual.symm = OrderDual.toDual
<VAR>α : Type u_1<VAR>a : αᵒᵈ<GOAL>OrderDual.toDual (OrderDual.ofDual a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>OrderDual.ofDual (OrderDual.toDual a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>OrderDual.toDual a = OrderDual.toDual b ↔ a = b
<VAR>α : Type u_1<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual a = OrderDual.ofDual b ↔ a = b
<VAR>α : Type u_1<VAR>LE α<VAR>a b : α<GOAL>OrderDual.toDual a ≤ OrderDual.toDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>OrderDual.toDual a < OrderDual.toDual b ↔ b < a
<VAR>α : Type u_1<VAR>LE α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual a ≤ OrderDual.ofDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual a < OrderDual.ofDual b ↔ b < a
<VAR>α : Type u_1<VAR>LE α<VAR>a : αᵒᵈ<VAR>b : α<GOAL>a ≤ OrderDual.toDual b ↔ b ≤ OrderDual.ofDual a
<VAR>α : Type u_1<VAR>LT α<VAR>a : αᵒᵈ<VAR>b : α<GOAL>a < OrderDual.toDual b ↔ b < OrderDual.ofDual a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<VAR>b : αᵒᵈ<GOAL>OrderDual.toDual a ≤ b ↔ OrderDual.ofDual b ≤ a
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<VAR>b : αᵒᵈ<GOAL>OrderDual.toDual a < b ↔ OrderDual.ofDual b < a
<VAR>α : Type u_1<VAR>p : αᵒᵈ → Prop<GOAL>(∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p (OrderDual.toDual a)
<VAR>α : Type u_1<VAR>p : αᵒᵈ → Prop<GOAL>(∃ a, p a) ↔ ∃ a, p (OrderDual.toDual a)
<VAR>α : Type u_1<GOAL>toLex.symm = ofLex
<VAR>α : Type u_1<GOAL>ofLex.symm = toLex
<VAR>α : Type u_1<VAR>a : Lex α<GOAL>toLex (ofLex a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>ofLex (toLex a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>toLex a = toLex b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Lex α<GOAL>ofLex a = ofLex b ↔ a = b
<VAR>α : Type u_1<VAR>p : Lex α → Prop<GOAL>(∀ (a : Lex α), p a) ↔ ∀ (a : α), p (toLex a)
<VAR>α : Type u_1<VAR>p : Lex α → Prop<GOAL>(∃ a, p a) ↔ ∃ a, p (toLex a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Multiset.Icc a b ↔ a ≤ x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Multiset.Ico a b ↔ a ≤ x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Multiset.Ioc a b ↔ a < x ∧ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Multiset.Ioo a b ↔ a < x ∧ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Multiset.Ici a ↔ a ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Multiset.Ioi a ↔ a < x
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>b x : α<GOAL>x ∈ Multiset.Iic b ↔ x ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrderBot α<VAR>b x : α<GOAL>x ∈ Multiset.Iio b ↔ x < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Multiset.Icc a b).Nodup
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Multiset.Ico a b).Nodup
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Multiset.Ioc a b).Nodup
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>(Multiset.Ioo a b).Nodup
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.Icc a b = 0 ↔ ¬a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.Ico a b = 0 ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.Ioc a b = 0 ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DenselyOrdered α<GOAL>Multiset.Ioo a b = 0 ↔ ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>Multiset.Ioo a b = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b < a<GOAL>Multiset.Icc a b = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Multiset.Ico a b = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Multiset.Ioc a b = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Multiset.Ioo a b = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Multiset.Ico a a = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Multiset.Ioc a a = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Multiset.Ioo a a = 0
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∈ Multiset.Icc a b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∈ Multiset.Ico a b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∈ Multiset.Icc a b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∈ Multiset.Ioc a b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∉ Multiset.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>a ∉ Multiset.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∉ Multiset.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>b ∉ Multiset.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hca : c ≤ a<GOAL>Multiset.filter (fun x => x < c) (Multiset.Ico a b) = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hbc : b ≤ c<GOAL>Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => x < c<VAR>hcb : c ≤ b<GOAL>Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a c
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => c ≤ x<VAR>hca : c ≤ a<GOAL>Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidablePred fun x => b ≤ x<GOAL>Multiset.filter (fun x => b ≤ x) (Multiset.Ico a b) = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>DecidablePred fun x => c ≤ x<VAR>hac : a ≤ c<GOAL>Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico c b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a : α<GOAL>Multiset.Icc a a = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>b ::ₘ Multiset.Ico a b = Multiset.Icc a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>h : a < b<GOAL>a ::ₘ Multiset.Ioo a b = Multiset.Ico a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b c d : α<VAR>h : b ≤ c<GOAL>(Multiset.Ico a b).Disjoint (Multiset.Ico c d)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>a b c d : α<VAR>h : b ≤ c<GOAL>Multiset.Ico a b ∩ Multiset.Ico c d = 0
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<VAR>DecidablePred fun x => x ≤ a<VAR>hab : a < b<GOAL>Multiset.filter (fun x => x ≤ a) (Multiset.Ico a b) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.card (Multiset.Ico a b) = Multiset.card (Multiset.Icc a b) - 1
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.card (Multiset.Ioc a b) = Multiset.card (Multiset.Icc a b) - 1
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.card (Multiset.Ioo a b) = Multiset.card (Multiset.Ico a b) - 1
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>a b : α<GOAL>Multiset.card (Multiset.Ioo a b) = Multiset.card (Multiset.Icc a b) - 2
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a₁ b₁ a₂ b₂ : α<VAR>h : a₁ < b₁<GOAL>Multiset.Ico a₁ b₁ ⊆ Multiset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Multiset.Ico a b + Multiset.Ico b c = Multiset.Ico a c
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Multiset.Ico a b ∩ Multiset.Ico c d = Multiset.Ico (max a c) (min b d)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a (min b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.filter (fun x => c ≤ x) (Multiset.Ico a b) = Multiset.Ico (max a c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.Ico a b - Multiset.Ico a c = Multiset.Ico (max a c) b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>LocallyFiniteOrder α<VAR>a b c : α<GOAL>Multiset.Ico a b - Multiset.Ico c b = Multiset.Ico a (min b c)
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<GOAL>Monotone fun n => Finset.Icc (-↑n) ↑n
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<GOAL>Finset.box 0 = {0}
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<GOAL>Finset.box (n + 1) = Finset.Icc (-↑n.succ) ↑n.succ \ Finset.Icc (-↑n) ↑n
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<GOAL>Disjoint (Finset.box (n + 1)) (Finset.Icc (-↑n) ↑n)
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<GOAL>Finset.box (n + 1) ∪ Finset.Icc (-↑n) ↑n = Finset.Icc (-↑n.succ) ↑n.succ
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<GOAL>(Finset.box (n + 1)).disjUnion (Finset.Icc (-↑n) ↑n) ⋯ = Finset.Icc (-↑n.succ) ↑n.succ
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<GOAL>0 ∈ Finset.box n ↔ n = 0
<VAR>α : Type u_1<VAR>OrderedRing α<VAR>LocallyFiniteOrder α<VAR>DecidableEq α<VAR>n : ℕ<VAR>x : α<VAR>hx : x ∈ Finset.box n<GOAL>x = 0 ↔ n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>OrderedRing α<VAR>OrderedRing β<VAR>LocallyFiniteOrder α<VAR>LocallyFiniteOrder β<VAR>DecidableEq α<VAR>DecidableEq β<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>n : ℕ<GOAL>(Finset.box (n + 1)).card = (Finset.Icc (-↑n.succ) ↑n.succ).card * (Finset.Icc (-↑n.succ) ↑n.succ).card - (Finset.Icc (-↑n) ↑n).card * (Finset.Icc (-↑n) ↑n).card
<VAR>n : ℕ<GOAL>n ≠ 0 → (Finset.box n).card = 8 * n
<VAR>x : ℤ × ℤ<VAR>n : ℕ<GOAL>x ∈ Finset.box n ↔ max x.1.natAbs x.2.natAbs = n
<VAR>x : ℤ × ℤ<GOAL>∃! n, x ∈ Finset.box n
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>LinearOrderedAddCommGroup G<VAR>OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : StrictMonoOn f (Set.Ici 0)<GOAL>StrictMono f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>LinearOrderedAddCommGroup G<VAR>OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : StrictAntiOn f (Set.Ici 0)<GOAL>StrictAnti f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>LinearOrderedAddCommGroup G<VAR>OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : MonotoneOn f (Set.Ici 0)<GOAL>Monotone f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>LinearOrderedAddCommGroup G<VAR>OrderedAddCommGroup H<VAR>f : G → H<VAR>h₁ : ∀ (x : G), f (-x) = -f x<VAR>h₂ : AntitoneOn f (Set.Ici 0)<GOAL>Antitone f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Symmetric r<GOAL>Symmetric rᶜ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hs : IsAntichain r s<VAR>h : t ⊆ s<GOAL>IsAntichain r t
<VAR>α : Type u_1<VAR>r₁ r₂ : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r₁ s<VAR>h : r₂ ≤ r₁<GOAL>IsAntichain r₂ s
<VAR>α : Type u_1<VAR>r₁ r₂ : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r₁ s<VAR>h : s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b<GOAL>IsAntichain r₂ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : r a b<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>h : r b a<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : IsAntichain r Set.univ<GOAL>IsAntisymm α r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsTrichotomous α r<VAR>h : IsAntichain r s<GOAL>s.Subsingleton
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<GOAL>IsAntichain (flip r) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<GOAL>IsAntichain (Function.swap r) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>f : α → β<VAR>h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b<GOAL>IsAntichain r' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>h : ∀ ⦃a b : β⦄, r' a b → r (f a) (f b)<GOAL>IsAntichain r' (f ⁻¹' s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<GOAL>IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : IsAntichain r s<VAR>hl : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r b a<VAR>hr : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b<GOAL>IsAntichain r (insert a s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hr : Symmetric r<GOAL>IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : IsAntichain r s<VAR>hr : Symmetric r<VAR>h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b<GOAL>IsAntichain r (insert a s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>φ : r ↪r r'<GOAL>IsAntichain r' (⇑φ '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>t : Set β<VAR>ht : IsAntichain r' t<VAR>φ : r ↪r r'<GOAL>IsAntichain r (⇑φ ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsAntichain r s<VAR>φ : r ≃r r'<GOAL>IsAntichain r' (⇑φ '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>t : Set β<VAR>hs : IsAntichain r' t<VAR>φ : r ≃r r'<GOAL>IsAntichain r (⇑φ ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>φ : r ↪r r'<GOAL>IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>φ : r ≃r r'<GOAL>IsAntichain r' (⇑φ '' s) ↔ IsAntichain r s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>LE α<VAR>LE β<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>φ : α ↪o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>t : Set β<VAR>ht : IsAntichain (fun x x_1 => x ≤ x_1) t<VAR>φ : α ↪o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>LE α<VAR>LE β<VAR>φ : α ↪o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ '' s) ↔ IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>LE α<VAR>LE β<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>φ : α ≃o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>LE α<VAR>LE β<VAR>φ : α ≃o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ '' s) ↔ IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>t : Set β<VAR>ht : IsAntichain (fun x x_1 => x ≤ x_1) t<VAR>φ : α ≃o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>t : Set β<VAR>φ : α ≃o β<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (⇑φ ⁻¹' t) ↔ IsAntichain (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>s : Set α<VAR>LE α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LE α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ↔ IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>BooleanAlgebra α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (compl '' s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>BooleanAlgebra α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) (compl ⁻¹' s)
<VAR>α : Type u_1<VAR>a : α<VAR>r : α → α → Prop<GOAL>IsAntichain r {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>r : α → α → Prop<GOAL>IsAntichain r s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a b : α<VAR>Preorder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>¬a < b
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsLeast s a ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsGreatest s a ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsLeast s a ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsGreatest s a ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>hs : IsLeast s a<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>hs : IsGreatest s a<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>OrderBot α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>⊥ ∈ s ↔ s = {⊥}
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>OrderTop α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>⊤ ∈ s ↔ s = {⊤}
<VAR>α : Type u_1<VAR>s : Set α<VAR>PartialOrder α<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬a < b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hs : IsStrongAntichain r s<VAR>h : t ⊆ s<GOAL>IsStrongAntichain r t
<VAR>α : Type u_1<VAR>r₁ r₂ : α → α → Prop<VAR>s : Set α<VAR>hs : IsStrongAntichain r₁ s<VAR>h : r₂ ≤ r₁<GOAL>IsStrongAntichain r₂ s