ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsStrongAntichain r s<VAR>a b c : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>hac : r a c<VAR>hbc : r b c<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>h : IsStrongAntichain r s<GOAL>IsAntichain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsDirected α r<VAR>h : IsStrongAntichain r s<GOAL>s.Subsingleton
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsSymm α r<VAR>hs : IsStrongAntichain r s<GOAL>IsStrongAntichain (flip r) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsSymm α r<VAR>hs : IsStrongAntichain r s<GOAL>IsStrongAntichain (Function.swap r) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsStrongAntichain r s<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>h : ∀ (a b : α), r' (f a) (f b) → r a b<GOAL>IsStrongAntichain r' (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>hs : IsStrongAntichain r s<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>h : ∀ (a b : β), r' a b → r (f a) (f b)<GOAL>IsStrongAntichain r' (f ⁻¹' s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<GOAL>IsStrongAntichain r (insert a s) ↔ IsStrongAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : IsStrongAntichain r s<VAR>h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ∀ (c : α), ¬r a c ∨ ¬r b c<GOAL>IsStrongAntichain r (insert a s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>r : α → α → Prop<GOAL>IsStrongAntichain r s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>hf' : AntitoneOn f s<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : MonotoneOn f s<VAR>hf' : StrictAntiOn f s<GOAL>IsAntichain (fun x x_1 => x ≤ x_1) s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s t : Set ((i : ι) → α i)<VAR>hs : IsWeakAntichain s<GOAL>t ⊆ s → IsWeakAntichain t
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ((i : ι) → α i)<VAR>a b : (i : ι) → α i<VAR>hs : IsWeakAntichain s<GOAL>a ∈ s → b ∈ s → StrongLT a b → a = b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ((i : ι) → α i)<VAR>a : (i : ι) → α i<VAR>hs : IsWeakAntichain s<GOAL>(∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT b a) → (∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b) → IsWeakAntichain (insert a s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ((i : ι) → α i)<VAR>a : (i : ι) → α i<GOAL>IsWeakAntichain (insert a s) ↔ IsWeakAntichain s ∧ ∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b ∧ ¬StrongLT b a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ((i : ι) → α i)<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>IsWeakAntichain s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Preorder (α i)<VAR>s : Set ((i : ι) → α i)<VAR>hs : s.Subsingleton<GOAL>IsWeakAntichain s
<VAR>𝕆 : Type u_5<VAR>α : Type u_6<VAR>Preorder 𝕆<VAR>Preorder α<VAR>self : GradeOrder 𝕆 α<VAR>a b : α<GOAL>a ⋖ b → GradeOrder.grade a ⋖ GradeOrder.grade b
<VAR>𝕆 : Type u_5<VAR>α : Type u_6<VAR>Preorder 𝕆<VAR>Preorder α<VAR>self : GradeOrder 𝕆 α<GOAL>StrictMono GradeOrder.grade
<VAR>𝕆 : Type u_5<VAR>α : Type u_6<VAR>Preorder 𝕆<VAR>Preorder α<VAR>self : GradeMinOrder 𝕆 α<VAR>a : α<GOAL>IsMin a → IsMin (GradeOrder.grade a)
<VAR>𝕆 : Type u_5<VAR>α : Type u_6<VAR>Preorder 𝕆<VAR>Preorder α<VAR>self : GradeMaxOrder 𝕆 α<VAR>a : α<GOAL>IsMax a → IsMax (GradeOrder.grade a)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>grade 𝕆 a ⋖ grade 𝕆 b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeOrder 𝕆 α<GOAL>StrictMono (grade 𝕆)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeMinOrder 𝕆 α<VAR>a : α<VAR>h : IsMin a<GOAL>IsMin (grade 𝕆 a)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeMinOrder 𝕆 α<VAR>a : α<GOAL>IsMin (grade 𝕆 a) ↔ IsMin a
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeMaxOrder 𝕆 α<VAR>a : α<VAR>h : IsMax a<GOAL>IsMax (grade 𝕆 a)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeMaxOrder 𝕆 α<VAR>a : α<GOAL>IsMax (grade 𝕆 a) ↔ IsMax a
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>PartialOrder α<VAR>GradeOrder 𝕆 α<GOAL>Monotone (grade 𝕆)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<GOAL>Function.Injective (grade 𝕆)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>grade 𝕆 a < grade 𝕆 b ↔ a < b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>grade 𝕆 a = grade 𝕆 b ↔ a = b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>LinearOrder α<VAR>GradeOrder 𝕆 α<VAR>a b : α<GOAL>grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>PartialOrder 𝕆<VAR>Preorder α<VAR>OrderBot 𝕆<VAR>OrderBot α<VAR>GradeMinOrder 𝕆 α<GOAL>grade 𝕆 ⊥ = ⊥
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>PartialOrder 𝕆<VAR>Preorder α<VAR>OrderTop 𝕆<VAR>OrderTop α<VAR>GradeMaxOrder 𝕆 α<GOAL>grade 𝕆 ⊤ = ⊤
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>grade α a = a
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeOrder 𝕆 α<VAR>a : α<GOAL>grade 𝕆ᵒᵈ (OrderDual.toDual a) = OrderDual.toDual (grade 𝕆 a)
<VAR>𝕆 : Type u_1<VAR>α : Type u_3<VAR>Preorder 𝕆<VAR>Preorder α<VAR>GradeOrder 𝕆 α<VAR>a : αᵒᵈ<GOAL>grade 𝕆 (OrderDual.ofDual a) = OrderDual.ofDual (grade 𝕆ᵒᵈ a)
<VAR>α : Type u_3<VAR>Preorder α<VAR>𝕆 : Type u_5<VAR>Preorder 𝕆<VAR>GradeOrder 𝕆 α<VAR>WellFoundedLT 𝕆<GOAL>WellFoundedLT α
<VAR>α : Type u_3<VAR>Preorder α<VAR>𝕆 : Type u_5<VAR>Preorder 𝕆<VAR>GradeOrder 𝕆 α<VAR>WellFoundedGT 𝕆<GOAL>WellFoundedGT α
<VAR>α : Type u<VAR>LE α<VAR>self : OrderTop α<VAR>a : α<GOAL>a ≤ ⊤
<VAR>α : Type u<VAR>LE α<VAR>OrderTop α<VAR>a : α<GOAL>a ≤ ⊤
<VAR>α : Type u<VAR>LE α<VAR>OrderTop α<GOAL>IsTop ⊤
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<GOAL>IsMax ⊤
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>¬⊤ < a
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<VAR>a b : α<VAR>h : a < b<GOAL>a ≠ ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>IsMax a ↔ a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>IsTop a ↔ a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>¬IsMax a ↔ a ≠ ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>¬IsTop a ↔ a ≠ ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>⊤ ≤ a ↔ a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<VAR>h : ⊤ ≤ a<GOAL>a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>a = ⊤ ↔ ⊤ ≤ a
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>h : a ≤ b<VAR>h₂ : a = ⊤<GOAL>b = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>a < ⊤ ↔ a ≠ ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>¬a < ⊤ ↔ a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>a = ⊤ ∨ a < ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<VAR>h : a ≠ ⊤<GOAL>a < ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<VAR>h : ⊤ ≠ a<GOAL>a < ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>hb : b ≠ ⊤<VAR>hab : a ≤ b<GOAL>a ≠ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>OrderTop α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictMono f<GOAL>f a = f ⊤ ↔ a = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>OrderTop α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictAnti f<GOAL>f a = f ⊤ ↔ a = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderTop α<VAR>Nontrivial α<GOAL>¬IsMin ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>Preorder β<VAR>OrderTop β<VAR>f : α → β<VAR>H : StrictMono f<VAR>a : α<VAR>h_top : f a = ⊤<VAR>x : α<GOAL>x ≤ a
<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A : OrderTop α<VAR>hB : PartialOrder α<VAR>B : OrderTop α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊤ = ⊤
<VAR>α : Type u<VAR>LE α<VAR>self : OrderBot α<VAR>a : α<GOAL>⊥ ≤ a
<VAR>α : Type u<VAR>LE α<VAR>OrderBot α<VAR>a : α<GOAL>⊥ ≤ a
<VAR>α : Type u<VAR>LE α<VAR>OrderBot α<GOAL>IsBot ⊥
<VAR>α : Type u<VAR>Top α<GOAL>OrderDual.ofDual ⊥ = ⊤
<VAR>α : Type u<VAR>Bot α<GOAL>OrderDual.ofDual ⊤ = ⊥
<VAR>α : Type u<VAR>Bot α<GOAL>OrderDual.toDual ⊥ = ⊤
<VAR>α : Type u<VAR>Top α<GOAL>OrderDual.toDual ⊤ = ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<GOAL>IsMin ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<VAR>a : α<GOAL>¬a < ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<VAR>a b : α<VAR>h : a < b<GOAL>b ≠ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>IsMin a ↔ a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>IsBot a ↔ a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>¬IsMin a ↔ a ≠ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>¬IsBot a ↔ a ≠ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>a ≤ ⊥ ↔ a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<VAR>h : a ≤ ⊥<GOAL>a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>a = ⊥ ↔ a ≤ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>h : a ≤ b<VAR>h₂ : b = ⊥<GOAL>a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>⊥ < a ↔ a ≠ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>¬⊥ < a ↔ a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>a = ⊥ ∨ ⊥ < a
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<VAR>h : ∀ (b : α), ¬b < a<GOAL>a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<VAR>h : a ≠ ⊥<GOAL>⊥ < a
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<VAR>h : ⊥ ≠ a<GOAL>⊥ < a
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>hb : b ≠ ⊥<VAR>hab : b ≤ a<GOAL>a ≠ ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>OrderBot α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictMono f<GOAL>f a = f ⊥ ↔ a = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder α<VAR>OrderBot α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>hf : StrictAnti f<GOAL>f a = f ⊥ ↔ a = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>OrderBot α<VAR>Nontrivial α<GOAL>¬IsMax ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>PartialOrder β<VAR>OrderBot β<VAR>f : α → β<VAR>H : StrictMono f<VAR>a : α<VAR>h_bot : f a = ⊥<VAR>x : α<GOAL>a ≤ x
<VAR>α : Type u_3<VAR>hA : PartialOrder α<VAR>A : OrderBot α<VAR>hB : PartialOrder α<VAR>B : OrderBot α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>⊥ = ⊥
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a : α<GOAL>⊤ ⊔ a = ⊤
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a : α<GOAL>a ⊔ ⊤ = ⊤
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>a : α<GOAL>⊥ ⊔ a = a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>a : α<GOAL>a ⊔ ⊥ = a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>a b : α<GOAL>a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>a : α<GOAL>⊤ ⊓ a = a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>a : α<GOAL>a ⊓ ⊤ = a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>a b : α<GOAL>a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a : α<GOAL>⊥ ⊓ a = ⊥
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a : α<GOAL>a ⊓ ⊥ = ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>p q : α → Prop<VAR>m_p : Monotone p<VAR>m_q : Monotone q<GOAL>Monotone fun x => p x ∧ q x
<VAR>α : Type u<VAR>Preorder α<VAR>p q : α → Prop<VAR>m_p : Monotone p<VAR>m_q : Monotone q<GOAL>Monotone fun x => p x ∨ q x
<VAR>α : Type u<VAR>Preorder α<VAR>x : α<GOAL>Monotone fun x_1 => x ≤ x_1
<VAR>α : Type u<VAR>Preorder α<VAR>x : α<GOAL>Monotone fun x_1 => x < x_1
<VAR>α : Type u<VAR>Preorder α<VAR>x : α<GOAL>Antitone fun x_1 => x_1 ≤ x
<VAR>α : Type u<VAR>Preorder α<VAR>x : α<GOAL>Antitone fun x_1 => x_1 < x
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>hP : ∀ (x : β), Monotone (P x)<GOAL>Monotone fun y => ∀ (x : β), P x y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>hP : ∀ (x : β), Antitone (P x)<GOAL>Antitone fun y => ∀ (x : β), P x y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>s : Set β<VAR>hP : ∀ (x : β), x ∈ s → Monotone (P x)<GOAL>Monotone fun y => ∀ (x : β), x ∈ s → P x y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>s : Set β<VAR>hP : ∀ (x : β), x ∈ s → Antitone (P x)<GOAL>Antitone fun y => ∀ (x : β), x ∈ s → P x y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>hP : ∀ (x : β), Monotone (P x)<GOAL>Monotone fun y => ∃ x, P x y
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>P : β → α → Prop<VAR>hP : ∀ (x : β), Antitone (P x)<GOAL>Antitone fun y => ∃ x, P x y
<VAR>α : Type u<VAR>Preorder α<VAR>P : α → Prop<VAR>x₀ : α<VAR>hP : Monotone P<GOAL>(∀ (x : α), x ≥ x₀ → P x) ↔ P x₀
<VAR>α : Type u<VAR>Preorder α<VAR>P : α → Prop<VAR>x₀ : α<VAR>hP : Antitone P<GOAL>(∀ (x : α), x ≤ x₀ → P x) ↔ P x₀
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>P : α → Prop<VAR>x₀ : α<VAR>hP : Monotone P<GOAL>(∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>P : α → Prop<VAR>x₀ : α<VAR>hP : Antitone P<GOAL>(∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x
<VAR>ι : Type u_3<VAR>α' : ι → Type u_4<VAR>(i : ι) → Bot (α' i)<VAR>i : ι<GOAL>⊥ i = ⊥
<VAR>ι : Type u_3<VAR>α' : ι → Type u_4<VAR>(i : ι) → Bot (α' i)<GOAL>⊥ = fun x => ⊥
<VAR>ι : Type u_3<VAR>α' : ι → Type u_4<VAR>(i : ι) → Top (α' i)<VAR>i : ι<GOAL>⊤ i = ⊤
<VAR>ι : Type u_3<VAR>α' : ι → Type u_4<VAR>(i : ι) → Top (α' i)<GOAL>⊤ = fun x => ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>hα : ⊥ = ⊤<VAR>x : α<GOAL>x = ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>hα : ⊥ = ⊤<VAR>x : α<GOAL>x = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>h : ⊤ ≤ ⊥<GOAL>Subsingleton α
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>hα : ⊥ = ⊤<GOAL>Subsingleton α
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>⊥ = ⊤ ↔ Subsingleton α
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderBot α<VAR>OrderBot (Subtype p)<VAR>hbot : p ⊥<GOAL>⟨⊥, hbot⟩ = ⊥
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderTop α<VAR>OrderTop (Subtype p)<VAR>htop : p ⊤<GOAL>⟨⊤, htop⟩ = ⊤
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderBot α<VAR>OrderBot (Subtype p)<VAR>hbot : p ⊥<GOAL>↑⊥ = ⊥
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderTop α<VAR>OrderTop (Subtype p)<VAR>htop : p ⊤<GOAL>↑⊤ = ⊤
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderBot α<VAR>OrderBot (Subtype p)<VAR>hbot : p ⊥<VAR>x : { x // p x }<GOAL>↑x = ⊥ ↔ x = ⊥
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderTop α<VAR>OrderTop (Subtype p)<VAR>htop : p ⊤<VAR>x : { x // p x }<GOAL>↑x = ⊤ ↔ x = ⊤
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderBot α<VAR>OrderBot (Subtype p)<VAR>hbot : p ⊥<VAR>x : α<VAR>hx : p x<GOAL>⟨x, hx⟩ = ⊥ ↔ x = ⊥
<VAR>α : Type u<VAR>p : α → Prop<VAR>PartialOrder α<VAR>OrderTop α<VAR>OrderTop (Subtype p)<VAR>htop : p ⊤<VAR>x : α<VAR>hx : p x<GOAL>⟨x, hx⟩ = ⊤ ↔ x = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>Top α<VAR>Top β<GOAL>⊤.1 = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>Top α<VAR>Top β<GOAL>⊤.2 = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>Bot α<VAR>Bot β<GOAL>⊥.1 = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>Bot α<VAR>Bot β<GOAL>⊥.2 = ⊥
<VAR>α : Type u<VAR>Top α<GOAL>{ down := ⊤ } = ⊤
<VAR>α : Type u<VAR>Top α<GOAL>⊤.down = ⊤
<VAR>α : Type u<VAR>Bot α<GOAL>{ down := ⊥ } = ⊥
<VAR>α : Type u<VAR>Bot α<GOAL>⊥.down = ⊥
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a : α<GOAL>min ⊥ a = ⊥
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a : α<GOAL>max ⊤ a = ⊤
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a : α<GOAL>min ⊤ a = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a : α<GOAL>max ⊥ a = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a : α<GOAL>min a ⊤ = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a : α<GOAL>max a ⊥ = a
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a : α<GOAL>min a ⊥ = ⊥
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a : α<GOAL>max a ⊤ = ⊤
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a b : α<GOAL>min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a b : α<GOAL>max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderBot α<VAR>a b : α<GOAL>max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
<VAR>α : Type u<VAR>LinearOrder α<VAR>OrderTop α<VAR>a b : α<GOAL>min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>Nontrivial α<GOAL>⊥ ≠ ⊤
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>Nontrivial α<GOAL>⊤ ≠ ⊥
<VAR>α : Type u<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>Nontrivial α<GOAL>⊥ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : StrictMonoOn f s<VAR>h₂ : StrictMonoOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<GOAL>StrictMonoOn f (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : StrictMonoOn f (Set.Iic a)<VAR>h₂ : StrictMonoOn f (Set.Ici a)<GOAL>StrictMono f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : StrictAntiOn f s<VAR>h₂ : StrictAntiOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<GOAL>StrictAntiOn f (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : StrictAntiOn f (Set.Iic a)<VAR>h₂ : StrictAntiOn f (Set.Ici a)<GOAL>StrictAnti f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : MonotoneOn f s<VAR>h₂ : MonotoneOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<GOAL>MonotoneOn f (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : MonotoneOn f (Set.Iic a)<VAR>h₂ : MonotoneOn f (Set.Ici a)<GOAL>Monotone f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : AntitoneOn f s<VAR>h₂ : AntitoneOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<GOAL>AntitoneOn f (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a : α<VAR>f : α → β<VAR>h₁ : AntitoneOn f (Set.Iic a)<VAR>h₂ : AntitoneOn f (Set.Ici a)<GOAL>Antitone f
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderBot α<VAR>a x : α<VAR>ha : IsAtom a<VAR>hax : a ≤ x<GOAL>IsAtom ⟨a, hax⟩
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderBot α<VAR>x : α<VAR>a : ↑(Set.Iic x)<VAR>ha : IsAtom a<GOAL>IsAtom ↑a
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderBot α<VAR>a : α<GOAL>IsAtom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a x : α<VAR>h : IsAtom a<GOAL>x < a ↔ x = ⊥
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a x : α<VAR>h : IsAtom a<GOAL>x ≤ a ↔ x = ⊥ ∨ x = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>ha : IsAtom a<VAR>hb : b ≠ ⊥<GOAL>b ≤ a ↔ b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<VAR>h : IsAtom a<GOAL>Set.Iic a = {⊥, a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>⊥ ⋖ a ↔ IsAtom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>Order.Frame α<VAR>a : α<VAR>ha : IsAtom a<VAR>f : ι → α<GOAL>a ≤ iSup f ↔ ∃ i, a ≤ f i
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderBot α<VAR>a : α<GOAL>IsCoatom (OrderDual.toDual a) ↔ IsAtom a
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>IsAtom (OrderDual.toDual a) ↔ IsCoatom a
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderTop α<VAR>a x : α<VAR>ha : IsCoatom a<VAR>hax : x ≤ a<GOAL>IsCoatom ⟨a, hax⟩
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderTop α<VAR>x : α<VAR>a : ↑(Set.Ici x)<VAR>ha : IsCoatom a<GOAL>IsCoatom ↑a
<VAR>α : Type u_2<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>IsCoatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a x : α<VAR>h : IsCoatom a<GOAL>a < x ↔ x = ⊤
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a x : α<VAR>h : IsCoatom a<GOAL>a ≤ x ↔ x = ⊤ ∨ x = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>ha : IsCoatom a<VAR>hb : b ≠ ⊤<GOAL>a ≤ b ↔ b = a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<VAR>h : IsCoatom a<GOAL>Set.Ici a = {⊤, a}
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>a ⋖ ⊤ ↔ IsCoatom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>Order.Coframe α<VAR>a : α<VAR>ha : IsCoatom a<VAR>f : ι → α<GOAL>iInf f ≤ a ↔ ∃ i, f i ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a : α<VAR>b : ↑(Set.Ici a)<GOAL>IsAtom b ↔ a ⋖ ↑b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>b : α<VAR>a : ↑(Set.Iic b)<GOAL>IsCoatom a ↔ ↑a ⋖ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a ⋖ b ↔ IsAtom ⟨b, h⟩
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a ⋖ b ↔ IsCoatom ⟨a, h⟩
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>ha : IsAtom a<VAR>hb : IsAtom b<VAR>hab : a ≠ b<GOAL>a ⊓ b = ⊥
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>ha : IsAtom a<VAR>hb : IsAtom b<VAR>hab : a ≠ b<GOAL>Disjoint a b
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<VAR>ha : IsCoatom a<VAR>hb : IsCoatom b<VAR>hab : a ≠ b<GOAL>a ⊔ b = ⊤
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>self : IsAtomic α<VAR>b : α<GOAL>b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<GOAL>IsAtomic α ↔ ∀ (b : α), b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>self : IsCoatomic α<VAR>b : α<GOAL>b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<GOAL>IsCoatomic α ↔ ∀ (b : α), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<VAR>Nontrivial α<VAR>IsAtomic α<GOAL>∃ a, IsAtom a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<VAR>Nontrivial α<VAR>IsCoatomic α<GOAL>∃ a, IsCoatom a
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<GOAL>IsCoatomic αᵒᵈ ↔ IsAtomic α
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<GOAL>IsAtomic αᵒᵈ ↔ IsCoatomic α
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderBot α<GOAL>IsAtomic α ↔ ∀ (x : α), IsAtomic ↑(Set.Iic x)
<VAR>α : Type u_2<VAR>PartialOrder α<VAR>OrderTop α<GOAL>IsCoatomic α ↔ ∀ (x : α), IsCoatomic ↑(Set.Ici x)
<VAR>α : Type u_5<VAR>Preorder α<VAR>self : IsStronglyAtomic α<VAR>a b : α<GOAL>a < b → ∃ x, a ⋖ x ∧ x ≤ b
<VAR>α : Type u_5<VAR>Preorder α<GOAL>IsStronglyAtomic α ↔ ∀ (a b : α), a < b → ∃ x, a ⋖ x ∧ x ≤ b
<VAR>α : Type u_4<VAR>a b : α<VAR>Preorder α<VAR>IsStronglyAtomic α<VAR>h : a < b<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>α : Type u_5<VAR>Preorder α<GOAL>IsStronglyCoatomic α ↔ ∀ (a b : α), a < b → ∃ x, a ≤ x ∧ x ⋖ b
<VAR>α : Type u_5<VAR>Preorder α<VAR>self : IsStronglyCoatomic α<VAR>a b : α<GOAL>a < b → ∃ x, a ≤ x ∧ x ⋖ b
<VAR>α : Type u_4<VAR>a b : α<VAR>Preorder α<VAR>IsStronglyCoatomic α<VAR>h : a < b<GOAL>∃ x, a ≤ x ∧ x ⋖ b
<VAR>α : Type u_4<VAR>Preorder α<GOAL>IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α
<VAR>α : Type u_4<VAR>Preorder α<GOAL>IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α
<VAR>α : Type u_4<VAR>Preorder α<VAR>IsStronglyAtomic α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>IsStronglyAtomic ↑s
<VAR>α : Type u_4<VAR>Preorder α<VAR>IsStronglyCoatomic α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>IsStronglyCoatomic ↑s