ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>h₁ : α = β<VAR>h₂ : HEq r s<VAR>a : α<GOAL>(RelIso.cast h₁ h₂) a = cast h₁ a
<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>h₁ : α = β<VAR>h₂ : HEq r s<GOAL>(RelIso.cast h₁ h₂).symm = RelIso.cast ⋯ ⋯
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>h₁ : α = α := ⋯<VAR>h₂ : HEq r r := ⋯<GOAL>RelIso.cast h₁ h₂ = RelIso.refl r
<VAR>α β γ : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>h₁ : α = β<VAR>h₁' : β = γ<VAR>h₂ : HEq r s<VAR>h₂' : HEq s t<GOAL>(RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast ⋯ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α ≃ β<VAR>o : ∀ {a b : α}, s (f a) (f b) ↔ r a b<GOAL>⇑{ toEquiv := f, map_rel_iff' := o }.symm = ⇑f.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>x : β<GOAL>e (e.symm x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>x : α<GOAL>e.symm (e x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>x : α<VAR>y : β<GOAL>r x (e.symm y) ↔ s (e x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>x : β<VAR>y : α<GOAL>r (e.symm x) y ↔ s x (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>e.trans e.symm = RelIso.refl r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>e.symm.trans e = RelIso.refl s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>Function.Bijective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>Function.Injective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>Function.Surjective ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>a b : α<GOAL>f a = f b ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>H : Function.Surjective ⇑f<VAR>a : α<GOAL>(RelIso.ofSurjective f H) a = f a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a g : α<VAR>h : ι → α<VAR>H : ∀ (j : ι), a ≤ g * h j<GOAL>a ≤ g * iInf h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a g : α<VAR>h : ι → α<VAR>H : ∀ (j : ι), a ≤ g + h j<GOAL>a ≤ g + iInf h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a g : α<VAR>h : ι → α<VAR>H : ∀ (j : ι), g + h j ≤ a<GOAL>g + iSup h ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a g : α<VAR>h : ι → α<VAR>H : ∀ (j : ι), g * h j ≤ a<GOAL>g * iSup h ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : α<VAR>H : ∀ (i : ι), a ≤ g i + h<GOAL>a ≤ iInf g + h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : α<VAR>H : ∀ (i : ι), a ≤ g i * h<GOAL>a ≤ iInf g * h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : α<VAR>H : ∀ (i : ι), g i + h ≤ a<GOAL>iSup g + h ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : α<VAR>H : ∀ (i : ι), g i * h ≤ a<GOAL>iSup g * h ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : ι' → α<VAR>H : ∀ (i : ι) (j : ι'), a ≤ g i * h j<GOAL>a ≤ iInf g * iInf h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : ι' → α<VAR>H : ∀ (i : ι) (j : ι'), a ≤ g i + h j<GOAL>a ≤ iInf g + iInf h
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>ConditionallyCompleteLattice α<VAR>Group α<VAR>CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : ι' → α<VAR>H : ∀ (i : ι) (j : ι'), g i * h j ≤ a<GOAL>iSup g * iSup h ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>Nonempty ι<VAR>Nonempty ι'<VAR>ConditionallyCompleteLattice α<VAR>AddGroup α<VAR>CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a : α<VAR>g : ι → α<VAR>h : ι' → α<VAR>H : ∀ (i : ι) (j : ι'), g i + h j ≤ a<GOAL>iSup g + iSup h ≤ a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>sSup ↑s = s.max' h
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>sInf ↑s = s.min' h
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>sSup ↑s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>sInf ↑s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>h : s.Nonempty<VAR>hs : s.Finite<GOAL>sSup s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>h : s.Nonempty<VAR>hs : s.Finite<GOAL>sInf s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>h : s.Nonempty<GOAL>sSup s < a ↔ ∀ x ∈ s, x < a
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>h : s.Nonempty<GOAL>a < sInf s ↔ ∀ x ∈ s, a < x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<GOAL>s.sup' H f = sSup (f '' ↑s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<GOAL>s.inf' H f = sInf (f '' ↑s)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.sup' hs id = sSup ↑s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.inf' hs id = sInf ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>Fintype ι<VAR>Nonempty ι<VAR>f : ι → α<GOAL>Finset.univ.sup' ⋯ f = ⨆ i, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>Fintype ι<VAR>Nonempty ι<VAR>f : ι → α<GOAL>Finset.univ.inf' ⋯ f = ⨅ i, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrderBot α<VAR>Fintype ι<VAR>f : ι → α<GOAL>Finset.univ.sup f = ⨆ i, f i
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>h : f a ≤ a<GOAL>OrderHom.lfp f ≤ a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>h : f a = a<GOAL>OrderHom.lfp f ≤ a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>h : ∀ (b : α), f b ≤ b → a ≤ b<GOAL>a ≤ OrderHom.lfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>ha : a ≤ OrderHom.lfp f<GOAL>f a ≤ OrderHom.lfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>f (OrderHom.lfp f) = OrderHom.lfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>Function.IsFixedPt (⇑f) (OrderHom.lfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>ha : OrderHom.lfp f ≤ a<GOAL>OrderHom.lfp f ≤ f a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>IsLeast {a | f a ≤ a} (OrderHom.lfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>IsLeast (Function.fixedPoints ⇑f) (OrderHom.lfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → a ≤ OrderHom.lfp f → p (f a)<VAR>hSup : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sSup s)<GOAL>p (OrderHom.lfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>h : a ≤ f a<GOAL>a ≤ OrderHom.gfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>h : ∀ b ≤ f b, b ≤ a<GOAL>OrderHom.gfp f ≤ a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>Function.IsFixedPt (⇑f) (OrderHom.gfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>f (OrderHom.gfp f) = OrderHom.gfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>ha : a ≤ OrderHom.gfp f<GOAL>f a ≤ OrderHom.gfp f
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>a : α<VAR>ha : OrderHom.gfp f ≤ a<GOAL>OrderHom.gfp f ≤ f a
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>IsGreatest {a | a ≤ f a} (OrderHom.gfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<GOAL>IsGreatest (Function.fixedPoints ⇑f) (OrderHom.gfp f)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>p : α → Prop<VAR>step : ∀ (a : α), p a → OrderHom.gfp f ≤ a → p (f a)<VAR>hInf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)<GOAL>p (OrderHom.gfp f)
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<GOAL>f (OrderHom.lfp (g.comp f)) = OrderHom.lfp (f.comp g)
<VAR>α : Type u<VAR>β : Type v<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : β →o α<VAR>g : α →o β<GOAL>f (OrderHom.gfp (g.comp f)) = OrderHom.gfp (f.comp g)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>h : α →o α →o α<GOAL>OrderHom.lfp (OrderHom.lfp.comp h) = OrderHom.lfp h.onDiag
<VAR>α : Type u<VAR>CompleteLattice α<VAR>h : α →o α →o α<GOAL>OrderHom.gfp (OrderHom.gfp.comp h) = OrderHom.gfp h.onDiag
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<GOAL>OrderHom.gfp ((OrderHom.const α) x ⊓ f) ≤ x
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : f x ≤ x<GOAL>↑(f.prevFixed x hx) ≤ x
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : x ≤ f x<GOAL>x ≤ ↑(f.nextFixed x hx)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : x ≤ f x<VAR>y : ↑(Function.fixedPoints ⇑f)<VAR>h : x ≤ ↑y<GOAL>f.nextFixed x hx ≤ y
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : x ≤ f x<VAR>y : ↑(Function.fixedPoints ⇑f)<GOAL>f.nextFixed x hx ≤ y ↔ x ≤ ↑y
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : f x ≤ x<VAR>y : ↑(Function.fixedPoints ⇑f)<GOAL>y ≤ f.prevFixed x hx ↔ ↑y ≤ x
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>hx : f x ≤ x<VAR>y : ↑(Function.fixedPoints ⇑f)<VAR>h : ↑y ≤ x<GOAL>y ≤ f.prevFixed x hx
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x y : ↑(Function.fixedPoints ⇑f)<GOAL>↑x ⊔ ↑y ≤ f (↑x ⊔ ↑y)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>x y : ↑(Function.fixedPoints ⇑f)<GOAL>f (↑x ⊓ ↑y) ≤ ↑x ⊓ ↑y
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>A : Set α<VAR>hA : A ⊆ Function.fixedPoints ⇑f<GOAL>sSup A ≤ f (sSup A)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>f : α →o α<VAR>A : Set α<VAR>hA : A ⊆ Function.fixedPoints ⇑f<GOAL>f (sInf A) ≤ sInf A
<VAR>P : Type u_2<VAR>Preorder P<VAR>self : Order.Ideal.PrimePair P<GOAL>IsCompl ↑self.I ↑self.F
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>(↑IF.I)ᶜ = ↑IF.F
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>(↑IF.F)ᶜ = ↑IF.I
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>IF.I.IsProper
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>Disjoint ↑IF.I ↑IF.F
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>↑IF.I ∪ ↑IF.F = Set.univ
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>↑IF.F ∪ ↑IF.I = Set.univ
<VAR>P : Type u_1<VAR>Preorder P<VAR>I : Order.Ideal P<VAR>self : I.IsPrime<GOAL>Order.IsPFilter (↑I)ᶜ
<VAR>P : Type u_1<VAR>Preorder P<VAR>I : Order.Ideal P<GOAL>I.IsPrime ↔ I.IsProper ∧ Order.IsPFilter (↑I)ᶜ
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>IF.I.IsPrime
<VAR>P : Type u_1<VAR>SemilatticeInf P<VAR>I : Order.Ideal P<VAR>hI : I.IsPrime<VAR>x y : P<GOAL>x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
<VAR>P : Type u_1<VAR>SemilatticeInf P<VAR>I : Order.Ideal P<VAR>I.IsProper<VAR>hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I<GOAL>I.IsPrime
<VAR>P : Type u_1<VAR>SemilatticeInf P<VAR>I : Order.Ideal P<VAR>I.IsProper<GOAL>I.IsPrime ↔ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>x : P<VAR>I : Order.Ideal P<VAR>hI : I.IsPrime<GOAL>x ∈ I ∨ xᶜ ∈ I
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>x : P<VAR>I : Order.Ideal P<VAR>hI : I.IsPrime<VAR>hxnI : x ∉ I<GOAL>xᶜ ∈ I
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>I : Order.Ideal P<VAR>I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<GOAL>I.IsPrime
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>I : Order.Ideal P<VAR>I.IsProper<GOAL>I.IsPrime ↔ ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Order.PFilter P<GOAL>F.IsPrime ↔ Order.IsIdeal (↑F)ᶜ
<VAR>P : Type u_1<VAR>Preorder P<VAR>F : Order.PFilter P<VAR>self : F.IsPrime<GOAL>Order.IsIdeal (↑F)ᶜ
<VAR>P : Type u_1<VAR>Preorder P<VAR>IF : Order.Ideal.PrimePair P<GOAL>IF.F.IsPrime
<VAR>α : Type u<VAR>self : Preorder α<VAR>a : α<GOAL>a ≤ a
<VAR>α : Type u<VAR>self : Preorder α<VAR>a b : α<GOAL>a < b ↔ a ≤ b ∧ ¬b ≤ a
<VAR>α : Type u<VAR>self : Preorder α<VAR>a b c : α<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>a ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a ≤ b → b ≤ c → a ≤ c
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a < b ↔ a ≤ b ∧ ¬b ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a ≤ b → ¬b ≤ a → a < b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a < b → a ≤ b ∧ ¬b ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a = b → a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a ≥ b → b ≥ c → a ≥ c
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>¬a < a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>¬a > a
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a < b → b < c → a < c
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a > b → b > c → a > c
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>a ≠ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : b < a<GOAL>a ≠ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>¬b < a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a < b → a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a < b → b ≤ c → a < c
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<GOAL>a ≤ b → b < c → a < c
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<VAR>h₁ : a > b<VAR>h₂ : b ≥ c<GOAL>a > c
<VAR>α : Type u<VAR>Preorder α<VAR>a b c : α<VAR>h₁ : a ≥ b<VAR>h₂ : b > c<GOAL>a > c
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a > b<GOAL>¬a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≥ b<GOAL>¬a < b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>a < b ∨ a = b → a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a = b ∨ a < b<GOAL>a ≤ b
<VAR>α : Type u<VAR>self : PartialOrder α<VAR>a b : α<GOAL>a ≤ b → b ≤ a → a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b → b ≤ a → a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>a b : α<GOAL>a = b ↔ a ≤ b ∧ b ≤ a
<VAR>α : Type u<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b → a ≠ b → a < b
<VAR>α : Type u<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>hab : a ≤ b<GOAL>a < b ∨ a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>hab : a ≤ b<GOAL>a = b ∨ a < b
<VAR>α : Type u<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ a < b ∨ a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b → a < b ∨ a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>a b : α<GOAL>a ≤ b ↔ a < b ∨ a = b
<VAR>α : Type u<VAR>self : LinearOrder α<VAR>a b : α<GOAL>min a b = if a ≤ b then a else b
<VAR>α : Type u<VAR>self : LinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ b ≤ a
<VAR>α : Type u<VAR>self : LinearOrder α<VAR>a b : α<GOAL>max a b = if a ≤ b then b else a
<VAR>α : Type u<VAR>self : LinearOrder α<VAR>a b : α<GOAL>compare a b = compareOfLessAndEq a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a ≥ b → a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a ≤ b → b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a > b<GOAL>¬a < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a < b ∨ a = b ∨ b < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬b < a<GOAL>a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a > b → a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬a ≥ b<GOAL>a < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a < b ∨ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ b < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a < b ∨ a ≥ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ a > b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≠ b<GOAL>a < b ∨ a > b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>a ≠ b ↔ a < b ∨ a > b
<VAR>α : Type u<VAR>LinearOrder α<VAR>x y : α<GOAL>x < y ↔ ¬x ≥ y
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a < b ↔ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>¬a ≤ b ↔ b < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>h : ¬a < b<GOAL>a = b ∨ b < a
<VAR>α : Type u<VAR>β : Type u_1<VAR>Preorder α<VAR>LinearOrder β<VAR>a b : α<VAR>c d : β<VAR>H : d < c → b < a<VAR>h : a ≤ b<GOAL>c ≤ d
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.lt ↔ a < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.gt ↔ a > b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.eq ↔ a = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>compare a b ≠ Ordering.gt ↔ a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>compare a b ≠ Ordering.lt ↔ a ≥ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>o : Ordering<GOAL>compare a b = o ↔ o.toRel a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>maximals r s ⊆ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>minimals r s ⊆ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>maximals r ∅ = ∅
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>minimals r ∅ = ∅
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>maximals r {a} = {a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>minimals r {a} = {a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>maximals (Function.swap r) s = minimals r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>minimals (Function.swap r) s = maximals r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x : α<VAR>rlt : α → α → Prop<VAR>IsNonstrictStrictOrder α r rlt<GOAL>x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → y ∉ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x : α<VAR>rlt : α → α → Prop<VAR>IsNonstrictStrictOrder α r rlt<GOAL>x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt x y → y ∉ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a b : α<VAR>IsAntisymm α r<VAR>ha : a ∈ maximals r s<VAR>hb : b ∈ s<VAR>h : r a b<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a b : α<VAR>IsAntisymm α r<VAR>ha : a ∈ minimals r s<VAR>hb : b ∈ s<VAR>h : r b a<GOAL>a = b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x : α<VAR>IsAntisymm α r<GOAL>x ∈ maximals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r x y → x = y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<VAR>IsAntisymm α r<VAR>P : α → Prop<GOAL>x ∈ maximals r (setOf P) ↔ P x ∧ ∀ ⦃y : α⦄, P y → r x y → x = y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x : α<VAR>IsAntisymm α r<GOAL>x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y ∈ s → r y x → x = y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<VAR>IsAntisymm α r<VAR>P : α → Prop<GOAL>x ∈ minimals r (setOf P) ↔ P x ∧ ∀ ⦃y : α⦄, P y → r y x → x = y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>IsAntisymm α r<VAR>IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r y x<GOAL>minimals r s = minimals r t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>IsAntisymm α r<VAR>IsTrans α r<VAR>hts : t ⊆ s<VAR>h : ∀ x ∈ s, ∃ y ∈ t, r x y<GOAL>maximals r s = maximals r t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsAntisymm α r<GOAL>IsAntichain r (maximals r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsAntisymm α r<GOAL>IsAntichain r (minimals r s)
<VAR>α : Type u_1<VAR>x : Set α<VAR>s : Set (Set α)<GOAL>x ∈ minimals (fun x x_1 => x ⊆ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : Set α⦄, y ⊂ x → y ∉ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α<VAR>s : Set α<GOAL>x ∈ minimals (fun x x_1 => x ≤ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, y < x → y ∉ s
<VAR>α : Type u_1<VAR>x : Set α<VAR>s : Set (Set α)<GOAL>x ∈ maximals (fun x x_1 => x ⊆ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : Set α⦄, x ⊂ y → y ∉ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α<VAR>s : Set α<GOAL>x ∈ maximals (fun x x_1 => x ≤ x_1) s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, x < y → y ∉ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P t → s ⊆ t → P s<GOAL>s ∈ maximals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
<VAR>α : Type u_1<VAR>s : Set α<VAR>P : Set α → Prop<VAR>hP : ∀ ⦃s t : Set α⦄, P s → s ⊆ t → P t<GOAL>s ∈ minimals (fun x x_1 => x ⊆ x_1) {t | P t} ↔ P s ∧ ∀ x ∈ s, ¬P (s \ {x})
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsSymm α r<GOAL>maximals r s = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsSymm α r<GOAL>minimals r s = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsSymm α r<GOAL>maximals r s = minimals r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : s.Subsingleton<GOAL>maximals r s = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : s.Subsingleton<GOAL>minimals r s = s
<VAR>α : Type u_1<VAR>r₁ r₂ : α → α → Prop<VAR>s : Set α<VAR>IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<GOAL>maximals r₂ s ⊆ maximals r₁ s
<VAR>α : Type u_1<VAR>r₁ r₂ : α → α → Prop<VAR>s : Set α<VAR>IsAntisymm α r₂<VAR>h : ∀ (a b : α), r₁ a b → r₂ a b<GOAL>minimals r₂ s ⊆ minimals r₁ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>minimals r (s ∪ t) ⊆ minimals r s ∪ minimals r t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>maximals r s ∩ t ⊆ maximals r (s ∩ t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>minimals r s ∩ t ⊆ minimals r (s ∩ t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>s ∩ maximals r t ⊆ maximals r (s ∩ t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>s ∩ minimals r t ⊆ minimals r (s ∩ t)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : IsAntichain r s<GOAL>maximals r s = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : IsAntichain r s<GOAL>minimals r s = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>maximals r (maximals r s) = maximals r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>minimals r (minimals r s) = minimals r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>ht : IsAntichain r t<VAR>h : maximals r s ⊆ t<VAR>hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ maximals r s, r b a<GOAL>maximals r s = t