ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>LE α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x y : α<GOAL>(cmpLE x y).swap = cmpLE y x
<VAR>α : Type u_3<VAR>Preorder α<VAR>IsTotal α fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>DecidableRel fun x x_1 => x < x_1<VAR>x y : α<GOAL>cmpLE x y = cmp x y
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>Ordering.lt.Compares a b = (a < b)
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>Ordering.eq.Compares a b = (a = b)
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>Ordering.gt.Compares a b = (a > b)
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<VAR>o : Ordering<GOAL>o.swap.Compares a b ↔ o.Compares b a
<VAR>o o' : Ordering<GOAL>o.swap = o' ↔ o = o'.swap
<VAR>α : Type u_1<VAR>Preorder α<VAR>o : Ordering<VAR>a b : α<GOAL>o.Compares a b → (o = Ordering.lt ↔ a < b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>o : Ordering<VAR>a b : α<GOAL>o.Compares a b → (o ≠ Ordering.lt ↔ b ≤ a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>o : Ordering<VAR>a b : α<GOAL>o.Compares a b → (o = Ordering.eq ↔ a = b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>o : Ordering<VAR>a b : α<VAR>h : o.Compares a b<GOAL>o = Ordering.gt ↔ b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>o : Ordering<VAR>a b : α<VAR>h : o.Compares a b<GOAL>o ≠ Ordering.gt ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>o : Ordering<GOAL>o.Compares a b → a ≤ b ∨ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>o : Ordering<GOAL>o.Compares a b → a ≤ b → b ≤ a → a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>o₁ o₂ : Ordering<VAR>a b : α<GOAL>o₁.Compares a b → o₂.Compares a b → o₁ = o₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>a b : α<VAR>a' b' : β<VAR>h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'<VAR>o : Ordering<GOAL>o.Compares a b ↔ o.Compares a' b'
<VAR>o₁ o₂ : Ordering<GOAL>(o₁.orElse o₂).swap = o₁.swap.orElse o₂.swap
<VAR>o₁ o₂ : Ordering<GOAL>o₁.orElse o₂ = Ordering.lt ↔ o₁ = Ordering.lt ∨ o₁ = Ordering.eq ∧ o₂ = Ordering.lt
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<VAR>o : Ordering<GOAL>o.Compares (OrderDual.toDual a) (OrderDual.toDual b) ↔ o.Compares b a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : αᵒᵈ<VAR>o : Ordering<GOAL>o.Compares (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ o.Compares b a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<GOAL>(cmp a b).Compares a b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>o : Ordering<VAR>h : o.Compares a b<GOAL>cmp a b = o
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a b : α<GOAL>(cmp a b).swap = cmp b a
<VAR>α : Type u_1<VAR>LE α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x y : α<GOAL>cmpLE (OrderDual.toDual x) (OrderDual.toDual y) = cmpLE y x
<VAR>α : Type u_1<VAR>LE α<VAR>DecidableRel fun x x_1 => x ≤ x_1<VAR>x y : αᵒᵈ<GOAL>cmpLE (OrderDual.ofDual x) (OrderDual.ofDual y) = cmpLE y x
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>x y : α<GOAL>cmp (OrderDual.toDual x) (OrderDual.toDual y) = cmp y x
<VAR>α : Type u_1<VAR>LT α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>x y : αᵒᵈ<GOAL>cmp (OrderDual.ofDual x) (OrderDual.ofDual y) = cmp y x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<GOAL>cmp x y = Ordering.lt ↔ x < y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<GOAL>cmp x y = Ordering.eq ↔ x = y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<GOAL>cmp x y = Ordering.gt ↔ y < x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x : α<GOAL>cmp x x = Ordering.eq
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>LinearOrder β<VAR>x' y' : β<GOAL>cmp x y = cmp x' y' ↔ cmp y x = cmp y' x'
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x < y ↔ x' < y'
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x ≤ y ↔ x' ≤ y'
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x = y ↔ x' = y'
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>h : x < y<GOAL>cmp x y = Ordering.lt
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>h : x < y<GOAL>cmp y x = Ordering.gt
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>h : x = y<GOAL>cmp x y = Ordering.eq
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<VAR>h : x = y<GOAL>cmp y x = Ordering.eq
<VAR>n : ℕ<GOAL>⊤ = Fin.last n
<VAR>n : ℕ<GOAL>⊥ = 0
<VAR>n : ℕ<VAR>NeZero n<GOAL>⊥.rev = ⊤
<VAR>n : ℕ<VAR>NeZero n<GOAL>⊤.rev = ⊥
<VAR>n : ℕ<VAR>NeZero n<GOAL>Fin.rev 0 = ⊤
<VAR>n : ℕ<GOAL>(Fin.last n).rev = ⊥
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → Fin (n + 1)<VAR>hf : ∀ (a : α), f a ≠ 0<VAR>hf₂ : StrictMono f<GOAL>StrictMono fun a => (f a).pred ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → Fin (n + 1)<VAR>hf : ∀ (a : α), f a ≠ 0<VAR>hf₂ : Monotone f<GOAL>Monotone fun a => (f a).pred ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → Fin (n + 1)<VAR>hf : ∀ (a : α), f a ≠ Fin.last n<VAR>hf₂ : StrictMono f<GOAL>StrictMono fun a => (f a).castPred ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : α → Fin (n + 1)<VAR>hf : ∀ (a : α), f a ≠ Fin.last n<VAR>hf₂ : Monotone f<GOAL>Monotone fun a => (f a).castPred ⋯
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : Fin (n + 1) → α<GOAL>StrictMono f ↔ ∀ (i : Fin n), f i.castSucc < f i.succ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : Fin (n + 1) → α<GOAL>Monotone f ↔ ∀ (i : Fin n), f i.castSucc ≤ f i.succ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : Fin (n + 1) → α<GOAL>StrictAnti f ↔ ∀ (i : Fin n), f i.succ < f i.castSucc
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f : Fin (n + 1) → α<GOAL>Antitone f ↔ ∀ (i : Fin n), f i.succ ≤ f i.castSucc
<VAR>n : ℕ<GOAL>StrictMono Fin.val
<VAR>n : ℕ<GOAL>StrictMono Fin.succ
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>StrictMono (Fin.castLE h)
<VAR>n : ℕ<VAR>m : ℕ<GOAL>StrictMono (Fin.castAdd m)
<VAR>n : ℕ<GOAL>StrictMono Fin.castSucc
<VAR>m : ℕ<VAR>n : ℕ<GOAL>StrictMono (Fin.natAdd n)
<VAR>n : ℕ<VAR>m : ℕ<GOAL>StrictMono fun x => x.addNat m
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>StrictMono p.succAbove
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<GOAL>p.succAbove i < p.succAbove j ↔ i < j
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<GOAL>p.succAbove i ≤ p.succAbove j ↔ i ≤ j
<VAR>n : ℕ<VAR>p : Fin n<GOAL>Monotone p.predAbove
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Monotone fun p => p.predAbove i
<VAR>n : ℕ<VAR>p : Fin n<VAR>i : Fin (n + 1)<GOAL>p.predAboveOrderHom i = p.predAbove i
<VAR>n : ℕ<VAR>a : Fin n<GOAL>Fin.orderIsoSubtype a = ⟨↑a, ⋯⟩
<VAR>n : ℕ<VAR>a : { i // i < n }<GOAL>(RelIso.symm Fin.orderIsoSubtype) a = ⟨↑a, ⋯⟩
<VAR>m n : ℕ<VAR>eq : n = m<VAR>i : Fin m<GOAL>(RelIso.symm (Fin.castOrderIso eq)) i = Fin.cast ⋯ i
<VAR>m n : ℕ<VAR>eq : n = m<VAR>i : Fin n<GOAL>(Fin.castOrderIso eq) i = Fin.cast eq i
<VAR>m n : ℕ<VAR>h : n = m<GOAL>(Fin.castOrderIso h).symm = Fin.castOrderIso ⋯
<VAR>n : ℕ<VAR>h : n = n := ⋯<GOAL>Fin.castOrderIso h = OrderIso.refl (Fin n)
<VAR>m n : ℕ<VAR>h : n = m<GOAL>(Fin.castOrderIso h).toEquiv = Equiv.cast ⋯
<VAR>n : ℕ<GOAL>∀ (a : (Fin n)ᵒᵈ), Fin.revOrderIso a = (OrderDual.ofDual a).rev
<VAR>n : ℕ<GOAL>Fin.revOrderIso.toEquiv = OrderDual.ofDual.trans Fin.revPerm
<VAR>n : ℕ<VAR>i : Fin n<GOAL>Fin.revOrderIso.symm i = OrderDual.toDual i.rev
<VAR>n : ℕ<VAR>self : Fin n<GOAL>(Fin.valOrderEmb n) self = ↑self
<VAR>n : ℕ<GOAL>⇑(Fin.succOrderEmb n) = Fin.succ
<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>i : Fin n<GOAL>(Fin.castLEOrderEmb h) i = Fin.castLE h i
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>(Fin.castLEOrderEmb h).toEmbedding = { toFun := Fin.castLE h, inj' := ⋯ }
<VAR>n : ℕ<VAR>m : ℕ<GOAL>(Fin.castAddOrderEmb m).toEmbedding = { toFun := Fin.castAdd m, inj' := ⋯ }
<VAR>n : ℕ<VAR>m : ℕ<GOAL>∀ (a : Fin n), (Fin.castAddOrderEmb m) a = Fin.castAdd m a
<VAR>n : ℕ<GOAL>Fin.castSuccOrderEmb.toEmbedding = { toFun := Fin.castSucc, inj' := ⋯ }
<VAR>n : ℕ<GOAL>∀ (a : Fin n), Fin.castSuccOrderEmb a = a.castSucc
<VAR>n : ℕ<VAR>m : ℕ<GOAL>(Fin.addNatOrderEmb m).toEmbedding = { toFun := fun x => x.addNat m, inj' := ⋯ }
<VAR>n : ℕ<VAR>m : ℕ<GOAL>∀ (x : Fin n), (Fin.addNatOrderEmb m) x = x.addNat m
<VAR>m : ℕ<VAR>n : ℕ<VAR>i : Fin m<GOAL>(Fin.natAddOrderEmb n) i = Fin.natAdd n i
<VAR>m : ℕ<VAR>n : ℕ<GOAL>(Fin.natAddOrderEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := ⋯ }
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>p.succAboveOrderEmb.toEmbedding = { toFun := p.succAbove, inj' := ⋯ }
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAboveOrderEmb i = p.succAbove i
<VAR>m n : ℕ<VAR>e : Fin n ≃o Fin m<VAR>i : Fin n<GOAL>↑(e i) = ↑i
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : Fin n → α<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>h : Set.range f = Set.range g<GOAL>f = g
<VAR>n : ℕ<VAR>α : Type u_1<VAR>Preorder α<VAR>f g : Fin n ↪o α<VAR>h : Set.range ⇑f = Set.range ⇑g<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ R.leftDual) (R.rightDual ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J J' : Set α<VAR>h : J' ∈ R.leftFixedPoints<VAR>h₁ : J ≤ J'<GOAL>R.rightDual (R.leftDual J) ≤ J'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I I' : Set β<VAR>h : I' ∈ R.rightFixedPoints<VAR>h₁ : I ≤ I'<GOAL>R.leftDual (R.rightDual I) ≤ I'
<VAR>α : Type u_1<VAR>Preorder α<VAR>SupSet α<VAR>s : Set (WithTop α)<VAR>hs : ⊤ ∉ s<VAR>hs' : BddAbove (WithTop.some ⁻¹' s)<GOAL>sSup s = ↑(sSup (WithTop.some ⁻¹' s))
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfSet α<VAR>s : Set (WithTop α)<VAR>hs : ¬s ⊆ {⊤}<VAR>h's : BddBelow s<GOAL>sInf s = ↑(sInf (WithTop.some ⁻¹' s))
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfSet α<VAR>s : Set (WithBot α)<VAR>hs : ⊥ ∉ s<VAR>hs' : BddBelow (WithBot.some ⁻¹' s)<GOAL>sInf s = ↑(sInf (WithBot.some ⁻¹' s))
<VAR>α : Type u_1<VAR>Preorder α<VAR>SupSet α<VAR>s : Set (WithBot α)<VAR>hs : ¬s ⊆ {⊥}<VAR>h's : BddAbove s<GOAL>sSup s = ↑(sSup (WithBot.some ⁻¹' s))
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfSet α<GOAL>sInf ∅ = ⊤
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>IsEmpty ι<VAR>InfSet α<VAR>f : ι → WithTop α<GOAL>⨅ i, f i = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfSet α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>h's : BddBelow s<GOAL>↑(sInf s) = sInf ((fun a => ↑a) '' s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>Nonempty ι<VAR>InfSet α<VAR>f : ι → α<VAR>hf : BddBelow (Set.range f)<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>SupSet α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>↑(sSup s) = sSup ((fun a => ↑a) '' s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>SupSet α<VAR>f : ι → α<VAR>h : BddAbove (Set.range f)<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>SupSet α<GOAL>sSup ∅ = ⊥
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>IsEmpty ι<VAR>SupSet α<VAR>f : ι → WithBot α<GOAL>⨆ i, f i = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>SupSet α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>h's : BddAbove s<GOAL>↑(sSup s) = sSup ((fun a => ↑a) '' s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>Nonempty ι<VAR>SupSet α<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfSet α<VAR>s : Set α<VAR>hs : BddBelow s<GOAL>↑(sInf s) = sInf ((fun a => ↑a) '' s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>InfSet α<VAR>f : ι → α<VAR>h : BddBelow (Set.range f)<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<GOAL>s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<GOAL>s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<GOAL>BddBelow s → a ∈ s → sInf s ≤ a
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<GOAL>BddAbove s → a ∈ s → a ≤ sSup s
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLinearOrder α<VAR>s : Set α<GOAL>¬BddAbove s → sSup s = sSup ∅
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLinearOrder α<VAR>s : Set α<GOAL>¬BddBelow s → sInf s = sInf ∅
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLinearOrder α<VAR>a b : α<GOAL>a ≤ b ∨ b ≤ a
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLinearOrderBot α<GOAL>sSup ∅ = ⊥
<VAR>α : Type u_5<VAR>self : ConditionallyCompleteLinearOrderBot α<VAR>x : α<GOAL>⊥ ≤ x
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h₁ : BddAbove s<VAR>h₂ : a ∈ s<GOAL>a ≤ sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h₁ : s.Nonempty<VAR>h₂ : ∀ b ∈ s, b ≤ a<GOAL>sSup s ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h₁ : BddBelow s<VAR>h₂ : a ∈ s<GOAL>sInf s ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h₁ : s.Nonempty<VAR>h₂ : ∀ b ∈ s, a ≤ b<GOAL>a ≤ sInf s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a b : α<VAR>hs : BddAbove s<VAR>hb : b ∈ s<VAR>h : a ≤ b<GOAL>a ≤ sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a b : α<VAR>hs : BddBelow s<VAR>hb : b ∈ s<VAR>h : b ≤ a<GOAL>sInf s ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>ht : BddAbove t<VAR>hs : s.Nonempty<VAR>h : s ⊆ t<GOAL>sSup s ≤ sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>ht : BddBelow t<VAR>hs : s.Nonempty<VAR>h : s ⊆ t<GOAL>sInf t ≤ sInf s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h : BddAbove s<VAR>hs : s.Nonempty<GOAL>a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>h : BddBelow s<VAR>hs : s.Nonempty<GOAL>sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>H : BddAbove (Set.range f)<GOAL>IsLUB (Set.range f) (⨆ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddAbove (f '' s)<VAR>Hne : s.Nonempty<GOAL>IsLUB (f '' s) (⨆ i, f ↑i)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>ne : s.Nonempty<VAR>H : BddBelow s<GOAL>IsGLB s (sInf s)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>H : BddBelow (Set.range f)<GOAL>IsGLB (Set.range f) (⨅ i, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddBelow (f '' s)<VAR>Hne : s.Nonempty<GOAL>IsGLB (f '' s) (⨅ i, f ↑i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<VAR>hf : BddAbove (Set.range f)<GOAL>iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>a : α<VAR>hf : BddBelow (Set.range f)<GOAL>a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>ι : Type u_5<VAR>s : Set ι<VAR>f : ι → α<VAR>a : α<VAR>hs : s.Nonempty<VAR>hf : BddAbove (f '' s)<GOAL>⨆ i, f ↑i ≤ a ↔ ∀ i ∈ s, f i ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>ι : Type u_5<VAR>s : Set ι<VAR>f : ι → α<VAR>a : α<VAR>hs : s.Nonempty<VAR>hf : BddBelow (f '' s)<GOAL>a ≤ ⨅ i, f ↑i ↔ ∀ i ∈ s, a ≤ f i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsLUB s a<VAR>ne : s.Nonempty<GOAL>sSup s = a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>H : IsLUB (Set.range f) a<GOAL>⨆ i, f i = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>s : Set β<VAR>f : β → α<VAR>H : IsLUB (f '' s) a<VAR>Hne : s.Nonempty<GOAL>⨆ i, f ↑i = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsGreatest s a<GOAL>sSup s = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsGreatest s a<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsGLB s a<VAR>ne : s.Nonempty<GOAL>sInf s = a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>Nonempty ι<VAR>f : ι → α<VAR>H : IsGLB (Set.range f) a<GOAL>⨅ i, f i = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>s : Set β<VAR>f : β → α<VAR>H : IsGLB (f '' s) a<VAR>Hne : s.Nonempty<GOAL>⨅ i, f ↑i = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsLeast s a<GOAL>sInf s = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>H : IsLeast s a<GOAL>sInf s ∈ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>hb : BddBelow s<VAR>ha : BddAbove s<GOAL>s ⊆ Set.Icc (sInf s) (sSup s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>hb : BddAbove s<VAR>hs : s.Nonempty<GOAL>sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>hb : BddBelow s<VAR>hs : s.Nonempty<GOAL>a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddBelow s<VAR>hs : s.Nonempty<GOAL>sSup (lowerBounds s) = sInf s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddAbove s<VAR>hs : s.Nonempty<GOAL>sInf (upperBounds s) = sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>x : α<VAR>s : Set α<VAR>h : x < sInf s<VAR>hs : BddBelow s<GOAL>x ∉ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>x : α<VAR>s : Set α<VAR>h : sSup s < x<VAR>hs : BddAbove s<GOAL>x ∉ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>b : α<VAR>hs : s.Nonempty<VAR>H : ∀ a ∈ s, a ≤ b<VAR>H' : ∀ w < b, ∃ a ∈ s, w < a<GOAL>sSup s = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>b : α<GOAL>s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a b : α<VAR>hs : BddAbove s<VAR>ha : a ∈ s<VAR>h : b < a<GOAL>b < sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a b : α<GOAL>BddBelow s → a ∈ s → a < b → sInf s < b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>sne : s.Nonempty<VAR>tne : t.Nonempty<VAR>hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y<GOAL>(upperBounds s ∩ lowerBounds t).Nonempty
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<GOAL>sSup {a} = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<GOAL>sInf {a} = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<GOAL>sSup {a, b} = a ⊔ b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<GOAL>sInf {a, b} = a ⊓ b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>hb : BddBelow s<VAR>ha : BddAbove s<VAR>ne : s.Nonempty<GOAL>sInf s ≤ sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>hs : BddAbove s<VAR>sne : s.Nonempty<VAR>ht : BddAbove t<VAR>tne : t.Nonempty<GOAL>sSup (s ∪ t) = sSup s ⊔ sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>hs : BddBelow s<VAR>sne : s.Nonempty<VAR>ht : BddBelow t<VAR>tne : t.Nonempty<GOAL>sInf (s ∪ t) = sInf s ⊓ sInf t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>hs : BddAbove s<VAR>ht : BddAbove t<VAR>hst : (s ∩ t).Nonempty<GOAL>sSup (s ∩ t) ≤ sSup s ⊓ sSup t
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s t : Set α<GOAL>BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>hs : BddAbove s<VAR>sne : s.Nonempty<GOAL>sSup (insert a s) = a ⊔ sSup s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>s : Set α<VAR>a : α<VAR>hs : BddBelow s<VAR>sne : s.Nonempty<GOAL>sInf (insert a s) = a ⊓ sInf s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<GOAL>sInf (Set.Icc a b) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<GOAL>sInf (Set.Ici a) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a < b<GOAL>sInf (Set.Ico a b) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>DenselyOrdered α<VAR>h : a < b<GOAL>sInf (Set.Ioc a b) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>NoMaxOrder α<VAR>DenselyOrdered α<GOAL>sInf (Set.Ioi a) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>DenselyOrdered α<VAR>h : a < b<GOAL>sInf (Set.Ioo a b) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<GOAL>sSup (Set.Icc a b) = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>DenselyOrdered α<VAR>h : a < b<GOAL>sSup (Set.Ico a b) = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<GOAL>sSup (Set.Iic a) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>NoMinOrder α<VAR>DenselyOrdered α<GOAL>sSup (Set.Iio a) = a
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a < b<GOAL>sSup (Set.Ioc a b) = b
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>DenselyOrdered α<VAR>h : a < b<GOAL>sSup (Set.Ioo a b) = b
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>c : α<VAR>H : ∀ (x : ι), f x ≤ c<GOAL>iSup f ≤ c
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>f : ι → α<VAR>H : BddAbove (Set.range f)<VAR>c : ι<GOAL>f c ≤ iSup f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>f : ι → α<VAR>H : BddAbove (Set.range f)<VAR>c : ι<VAR>h : a ≤ f c<GOAL>a ≤ iSup f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>f g : ι → α<VAR>B : BddAbove (Set.range g)<VAR>H : ∀ (x : ι), f x ≤ g x<GOAL>iSup f ≤ iSup g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddAbove (f '' s)<VAR>c : β<VAR>hc : c ∈ s<GOAL>f c ≤ ⨆ i, f ↑i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>f g : ι → α<VAR>B : BddBelow (Set.range f)<VAR>H : ∀ (x : ι), f x ≤ g x<GOAL>iInf f ≤ iInf g
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>f : ι → α<VAR>c : α<VAR>H : ∀ (x : ι), c ≤ f x<GOAL>c ≤ iInf f
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>f : ι → α<VAR>H : BddBelow (Set.range f)<VAR>c : ι<GOAL>iInf f ≤ f c
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>a : α<VAR>f : ι → α<VAR>H : BddBelow (Set.range f)<VAR>c : ι<VAR>h : f c ≤ a<GOAL>iInf f ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>f : β → α<VAR>s : Set β<VAR>H : BddBelow (f '' s)<VAR>c : β<VAR>hc : c ∈ s<GOAL>⨅ i, f ↑i ≤ f c
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>hι : Nonempty ι<VAR>a : α<GOAL>⨆ x, a = a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Nonempty ι<VAR>a : α<GOAL>⨅ x, a = a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Unique ι<VAR>s : ι → α<GOAL>⨆ i, s i = s default
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Unique ι<VAR>s : ι → α<GOAL>⨅ i, s i = s default
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Subsingleton ι<VAR>i : ι<VAR>s : ι → α<GOAL>⨆ i, s i = s i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ConditionallyCompleteLattice α<VAR>Subsingleton ι<VAR>i : ι<VAR>s : ι → α<GOAL>⨅ i, s i = s i
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : p<GOAL>⨆ (h : p), f h = f hp
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : p<GOAL>⨅ (h : p), f h = f hp
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : ¬p<GOAL>⨆ (h : p), f h = sSup ∅
<VAR>α : Type u_1<VAR>ConditionallyCompleteLattice α<VAR>p : Prop<VAR>f : p → α<VAR>hp : ¬p<GOAL>⨅ (h : p), f h = sInf ∅