ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>a b : α<VAR>LE α<VAR>o : Option α<GOAL>b ∈ o → (↑a ≤ o ↔ a ≤ b)
<VAR>α : Type u_1<VAR>a : α<VAR>LE α<VAR>x : WithBot α<GOAL>↑a ≤ x ↔ ∃ b, x = ↑b ∧ a ≤ b
<VAR>α : Type u_1<VAR>b : α<VAR>LE α<VAR>x : WithBot α<GOAL>x ≤ ↑b ↔ ∀ (a : α), x = ↑a → a ≤ b
<VAR>α : Type u_1<VAR>a : α<VAR>LE α<VAR>h : IsMax a<GOAL>IsMax ↑a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<VAR>b : WithBot α<VAR>h : b ≠ ⊥<GOAL>a ≤ b.unbot h ↔ ↑a ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<VAR>h : a ≠ ⊥<VAR>b : α<GOAL>a.unbot h ≤ b ↔ a ≤ ↑b
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<VAR>b c : α<VAR>h : a = ⊥ → b ≤ c<GOAL>WithBot.unbot' b a ≤ c ↔ a ≤ ↑c
<VAR>α : Type u_1<VAR>a b : α<VAR>LT α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>⊥ < ↑a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot α<GOAL>¬a < ⊥
<VAR>α : Type u_1<VAR>a b : α<VAR>LT α<GOAL>some a < some b ↔ a < b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>none < ↑a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot α<GOAL>¬a < none
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithBot α<GOAL>a < b ↔ ∃ p, b = ↑p ∧ a < ↑p
<VAR>α : Type u_1<VAR>b : α<VAR>LT α<VAR>x : WithBot α<GOAL>x < ↑b ↔ ∀ (a : α), x = ↑a → a < b
<VAR>α : Type u_1<VAR>LT α<VAR>x : WithBot α<GOAL>⊥ < x ↔ x ≠ ⊥
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot α<VAR>b c : α<VAR>h : a = ⊥ → b < c<GOAL>WithBot.unbot' b a < c ↔ a < ↑c
<VAR>α : Type u_1<VAR>Preorder α<GOAL>StrictMono fun a => ↑a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Monotone fun a => ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithBot α → β<GOAL>Monotone f ↔ (Monotone fun a => f ↑a) ∧ ∀ (x : α), f ⊥ ≤ f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone (WithBot.map f) ↔ Monotone f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithBot α → β<GOAL>StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ⊥ < f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithBot α → β<GOAL>StrictAnti f ↔ (StrictAnti fun a => f ↑a) ∧ ∀ (x : α), f ↑x < f ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono (WithBot.map f) ↔ StrictMono f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<VAR>a b : WithBot α<GOAL>WithBot.map f a ≤ WithBot.map f b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : WithBot α<VAR>b : α<GOAL>a ≤ ↑(WithBot.unbot' b a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<VAR>x : WithBot α<GOAL>x < ↑⊥ ↔ x = ⊥
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b : α<GOAL>↑(a ⊔ b) = ↑a ⊔ ↑b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b : α<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<GOAL>↑(min x y) = min ↑x ↑y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x y : α<GOAL>↑(max x y) = max ↑x ↑y
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a b : WithBot α<GOAL>a < b ↔ ∃ x, a < ↑x ∧ ↑x < b
<VAR>α : Type u_1<GOAL>Function.Injective WithTop.some
<VAR>α : Type u_1<VAR>p : WithTop α → Prop<GOAL>(∀ (x : WithTop α), p x) ↔ p ⊤ ∧ ∀ (x : α), p ↑x
<VAR>α : Type u_1<VAR>p : WithTop α → Prop<GOAL>(∃ x, p x) ↔ p ⊤ ∨ ∃ x, p ↑x
<VAR>α : Type u_1<VAR>a : α<GOAL>⊤ ≠ ↑a
<VAR>α : Type u_1<VAR>a : α<GOAL>↑a ≠ ⊤
<VAR>α : Type u_1<VAR>C : WithTop α → Sort u_5<VAR>d : C ⊤<VAR>f : (a : α) → C ↑a<GOAL>WithTop.recTopCoe d f ⊤ = d
<VAR>α : Type u_1<VAR>C : WithTop α → Sort u_5<VAR>d : C ⊤<VAR>f : (a : α) → C ↑a<VAR>x : α<GOAL>WithTop.recTopCoe d f ↑x = f x
<VAR>α : Type u_1<VAR>a : WithBot αᵒᵈ<GOAL>WithTop.toDual.symm a = WithBot.ofDual a
<VAR>α : Type u_1<VAR>a : WithBot α<GOAL>WithTop.ofDual.symm a = WithBot.toDual a
<VAR>α : Type u_1<GOAL>WithTop.toDual ⊤ = ⊥
<VAR>α : Type u_1<GOAL>WithTop.ofDual ⊤ = ⊥
<VAR>α : Type u_1<VAR>a : α<GOAL>WithTop.toDual ↑a = ↑(OrderDual.toDual a)
<VAR>α : Type u_1<VAR>a : αᵒᵈ<GOAL>WithTop.ofDual ↑a = ↑(OrderDual.ofDual a)
<VAR>α : Type u_5<VAR>d : α<GOAL>WithTop.untop' d ⊤ = d
<VAR>α : Type u_5<VAR>d x : α<GOAL>WithTop.untop' d ↑x = x
<VAR>α : Type u_1<VAR>d y : α<VAR>x : WithTop α<GOAL>WithTop.untop' d x = y ↔ x = ↑y ∨ x = ⊤ ∧ y = d
<VAR>α : Type u_1<VAR>d : α<VAR>x : WithTop α<GOAL>WithTop.untop' d x = d ↔ x = ↑d ∨ x = ⊤
<VAR>α : Type u_1<VAR>d : α<VAR>x y : WithTop α<GOAL>WithTop.untop' d x = WithTop.untop' d y ↔ x = y ∨ x = ↑d ∧ y = ⊤ ∨ x = ⊤ ∧ y = ↑d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>WithTop.map f ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>WithTop.map f ↑a = ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>g₁ : β → δ<VAR>g₂ : γ → δ<VAR>h : g₁ ∘ f₁ = g₂ ∘ f₂<VAR>a : α<GOAL>WithTop.map g₁ (WithTop.map f₁ ↑a) = WithTop.map g₂ (WithTop.map f₂ ↑a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>WithTop.map₂ f ↑a ↑b = ↑(f a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>b : WithTop β<GOAL>WithTop.map₂ f ⊤ b = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithTop α<GOAL>WithTop.map₂ f a ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : α<VAR>b : WithTop β<GOAL>WithTop.map₂ f (↑a) b = WithTop.map (fun b => f a b) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithTop α<VAR>b : β<GOAL>WithTop.map₂ f a ↑b = WithTop.map (fun x => f x b) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>a : WithTop α<VAR>b : WithTop β<GOAL>WithTop.map₂ f a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : αᵒᵈ → βᵒᵈ<VAR>a : WithBot α<GOAL>WithTop.map f (WithBot.toDual a) = WithBot.map (⇑OrderDual.toDual ∘ f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : WithBot αᵒᵈ<GOAL>WithTop.map f (WithBot.ofDual a) = WithBot.map (⇑OrderDual.ofDual ∘ f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : WithTop α<GOAL>WithTop.toDual (WithTop.map f a) = WithBot.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithTop.toDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : αᵒᵈ → βᵒᵈ<VAR>a : WithTop αᵒᵈ<GOAL>WithTop.ofDual (WithTop.map f a) = WithBot.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithTop.ofDual a)
<VAR>α : Type u_1<VAR>x : WithTop α<GOAL>x ≠ ⊤ ↔ ∃ a, ↑a = x
<VAR>α : Type u_1<VAR>x : WithTop α<GOAL>(∀ (a : α), ↑a ≠ x) ↔ x = ⊤
<VAR>α : Type u_1<VAR>x : WithTop α<VAR>hx : x ≠ ⊤<GOAL>↑(x.untop hx) = x
<VAR>α : Type u_1<VAR>x : α<VAR>h : ↑x ≠ ⊤ := ⋯<GOAL>(↑x).untop h = x
<VAR>α : Type u_1<VAR>Bot α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>Bot α<VAR>a : α<GOAL>↑a = ⊥ ↔ a = ⊥
<VAR>α : Type u_1<VAR>Bot α<VAR>a : α<GOAL>⊥ = ↑a ↔ ⊥ = a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<VAR>b : WithBot αᵒᵈ<GOAL>WithTop.toDual a ≤ b ↔ WithBot.ofDual b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot αᵒᵈ<VAR>b : WithTop α<GOAL>a ≤ WithTop.toDual b ↔ b ≤ WithBot.ofDual a
<VAR>α : Type u_1<VAR>LE α<VAR>a b : WithTop α<GOAL>WithTop.toDual a ≤ WithTop.toDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop αᵒᵈ<VAR>b : WithBot α<GOAL>WithTop.ofDual a ≤ b ↔ WithBot.toDual b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<VAR>b : WithTop αᵒᵈ<GOAL>a ≤ WithTop.ofDual b ↔ b ≤ WithBot.toDual a
<VAR>α : Type u_1<VAR>LE α<VAR>a b : WithTop αᵒᵈ<GOAL>WithTop.ofDual a ≤ WithTop.ofDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<GOAL>a ≤ none
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>¬⊤ ≤ ↑a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<GOAL>⊤ ≤ a ↔ a = ⊤
<VAR>α : Type u_1<VAR>a b : α<VAR>LE α<VAR>o : Option α<GOAL>a ∈ o → (o ≤ ↑b ↔ a ≤ b)
<VAR>α : Type u_1<VAR>b : α<VAR>LE α<VAR>x : WithTop α<GOAL>x ≤ ↑b ↔ ∃ a, x = ↑a ∧ a ≤ b
<VAR>α : Type u_1<VAR>a : α<VAR>LE α<VAR>x : WithTop α<GOAL>↑a ≤ x ↔ ∀ (b : α), x = ↑b → a ≤ b
<VAR>α : Type u_1<VAR>a : α<VAR>LE α<VAR>h : IsMin a<GOAL>IsMin ↑a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<VAR>b : α<VAR>h : a ≠ ⊤<GOAL>a.untop h ≤ b ↔ a ≤ ↑b
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<VAR>b : WithTop α<VAR>h : b ≠ ⊤<GOAL>a ≤ b.untop h ↔ ↑a ≤ b
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<VAR>b c : α<VAR>h : a = ⊤ → c ≤ b<GOAL>c ≤ WithTop.untop' b a ↔ ↑c ≤ a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop α<VAR>b : WithBot αᵒᵈ<GOAL>WithTop.toDual a < b ↔ WithBot.ofDual b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot αᵒᵈ<VAR>b : WithTop α<GOAL>a < WithTop.toDual b ↔ b < WithBot.ofDual a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithTop α<GOAL>WithTop.toDual a < WithTop.toDual b ↔ b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop αᵒᵈ<VAR>b : WithBot α<GOAL>WithTop.ofDual a < b ↔ WithBot.toDual b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot α<VAR>b : WithTop αᵒᵈ<GOAL>a < WithTop.ofDual b ↔ b < WithBot.toDual a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithTop αᵒᵈ<GOAL>WithTop.ofDual a < WithTop.ofDual b ↔ b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop α<VAR>b c : α<VAR>h : a = ⊤ → c < b<GOAL>c < WithTop.untop' b a ↔ ↑c < a
<VAR>α : Type u_1<VAR>a : WithTop αᵒᵈ<GOAL>WithBot.toDual.symm a = WithTop.ofDual a
<VAR>α : Type u_1<VAR>a : WithTop α<GOAL>WithBot.ofDual.symm a = WithTop.toDual a
<VAR>α : Type u_1<GOAL>WithBot.toDual ⊥ = ⊤
<VAR>α : Type u_1<GOAL>WithBot.ofDual ⊥ = ⊤
<VAR>α : Type u_1<VAR>a : α<GOAL>WithBot.toDual ↑a = ↑(OrderDual.toDual a)
<VAR>α : Type u_1<VAR>a : αᵒᵈ<GOAL>WithBot.ofDual ↑a = ↑(OrderDual.ofDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : αᵒᵈ → βᵒᵈ<VAR>a : WithTop α<GOAL>WithBot.map f (WithTop.toDual a) = WithTop.map (⇑OrderDual.toDual ∘ f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : WithTop αᵒᵈ<GOAL>WithBot.map f (WithTop.ofDual a) = WithTop.map (⇑OrderDual.ofDual ∘ f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : WithBot α<GOAL>WithBot.toDual (WithBot.map f a) = WithBot.map (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual) (WithBot.toDual a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : αᵒᵈ → βᵒᵈ<VAR>a : WithBot αᵒᵈ<GOAL>WithBot.ofDual (WithBot.map f a) = WithBot.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithBot.ofDual a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : WithBot α<GOAL>(∀ (y : α), x < ↑y) ↔ x = ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot α<VAR>b : WithTop αᵒᵈ<GOAL>WithBot.toDual a ≤ b ↔ WithTop.ofDual b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop αᵒᵈ<VAR>b : WithBot α<GOAL>a ≤ WithBot.toDual b ↔ b ≤ WithTop.ofDual a
<VAR>α : Type u_1<VAR>LE α<VAR>a b : WithBot α<GOAL>WithBot.toDual a ≤ WithBot.toDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithBot αᵒᵈ<VAR>b : WithTop α<GOAL>WithBot.ofDual a ≤ b ↔ WithTop.toDual b ≤ a
<VAR>α : Type u_1<VAR>LE α<VAR>a : WithTop α<VAR>b : WithBot αᵒᵈ<GOAL>a ≤ WithBot.ofDual b ↔ b ≤ WithTop.toDual a
<VAR>α : Type u_1<VAR>LE α<VAR>a b : WithBot αᵒᵈ<GOAL>WithBot.ofDual a ≤ WithBot.ofDual b ↔ b ≤ a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot α<VAR>b : WithTop αᵒᵈ<GOAL>WithBot.toDual a < b ↔ WithTop.ofDual b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop αᵒᵈ<VAR>b : WithBot α<GOAL>a < WithBot.toDual b ↔ b < WithTop.ofDual a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithBot α<GOAL>WithBot.toDual a < WithBot.toDual b ↔ b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithBot αᵒᵈ<VAR>b : WithTop α<GOAL>WithBot.ofDual a < b ↔ WithTop.toDual b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop α<VAR>b : WithBot αᵒᵈ<GOAL>a < WithBot.ofDual b ↔ b < WithTop.toDual a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithBot αᵒᵈ<GOAL>WithBot.ofDual a < WithBot.ofDual b ↔ b < a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>↑a < ⊤
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop α<GOAL>¬⊤ < a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : α<GOAL>some a < some b ↔ a < b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<GOAL>some a < none
<VAR>α : Type u_1<VAR>LT α<VAR>a : WithTop α<GOAL>¬none < a
<VAR>α : Type u_1<VAR>LT α<VAR>a b : WithTop α<GOAL>a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
<VAR>α : Type u_1<VAR>LT α<VAR>a : α<VAR>x : WithTop α<GOAL>↑a < x ↔ ∀ (b : α), x = ↑b → a < b
<VAR>α : Type u_1<VAR>LT α<VAR>x : WithTop α<GOAL>x < ⊤ ↔ x ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithTop α → β<GOAL>Monotone f ↔ (Monotone fun a => f ↑a) ∧ ∀ (x : α), f ↑x ≤ f ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>Monotone (WithTop.map f) ↔ Monotone f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithTop α → β<GOAL>StrictMono f ↔ (StrictMono fun a => f ↑a) ∧ ∀ (x : α), f ↑x < f ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : WithTop α → β<GOAL>StrictAnti f ↔ (StrictAnti fun a => f ↑a) ∧ ∀ (x : α), f ⊤ < f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<GOAL>StrictMono (WithTop.map f) ↔ StrictMono f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>a b : WithTop α<VAR>mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b<GOAL>WithTop.map f a ≤ WithTop.map f b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : WithTop α<VAR>b : α<GOAL>↑(WithTop.untop' b a) ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>x : WithTop α<GOAL>↑⊤ < x ↔ x = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : WithTop α<GOAL>(∀ (y : α), ↑y < x) ↔ x = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a b : WithTop α<GOAL>a < b ↔ ∃ x, a < ↑x ∧ ↑x < b
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>a b : R<VAR>h : ↑p ∣ a - b<VAR>k : ℕ<GOAL>↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
<VAR>F : Type u_1<VAR>NormedField F<VAR>n : ℕ<VAR>χ : DirichletCharacter F n<VAR>a : (ZMod n)ˣ<GOAL>‖χ ↑a‖ = 1
<VAR>F : Type u_1<VAR>NormedField F<VAR>n : ℕ<VAR>χ : DirichletCharacter F n<VAR>a : ZMod n<GOAL>‖χ a‖ ≤ 1
<VAR>α : Type u_1<VAR>LE α<GOAL>IsUpperSet ∅
<VAR>α : Type u_1<VAR>LE α<GOAL>IsLowerSet ∅
<VAR>α : Type u_1<VAR>LE α<GOAL>IsUpperSet Set.univ
<VAR>α : Type u_1<VAR>LE α<GOAL>IsLowerSet Set.univ
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>IsLowerSet sᶜ
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>IsUpperSet sᶜ
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>IsUpperSet sᶜ ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>IsLowerSet sᶜ ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsUpperSet s<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s ∪ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsLowerSet s<VAR>ht : IsLowerSet t<GOAL>IsLowerSet (s ∪ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsUpperSet s<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s ∩ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsLowerSet s<VAR>ht : IsLowerSet t<GOAL>IsLowerSet (s ∩ t)
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (Set α)<VAR>hf : ∀ s ∈ S, IsUpperSet s<GOAL>IsUpperSet (⋃₀ S)
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (Set α)<VAR>hf : ∀ s ∈ S, IsLowerSet s<GOAL>IsLowerSet (⋃₀ S)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsUpperSet (f i)<GOAL>IsUpperSet (⋃ i, f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsLowerSet (f i)<GOAL>IsLowerSet (⋃ i, f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)<GOAL>IsUpperSet (⋃ i, ⋃ j, f i j)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)<GOAL>IsLowerSet (⋃ i, ⋃ j, f i j)
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (Set α)<VAR>hf : ∀ s ∈ S, IsUpperSet s<GOAL>IsUpperSet (⋂₀ S)
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (Set α)<VAR>hf : ∀ s ∈ S, IsLowerSet s<GOAL>IsLowerSet (⋂₀ S)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsUpperSet (f i)<GOAL>IsUpperSet (⋂ i, f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsLowerSet (f i)<GOAL>IsLowerSet (⋂ i, f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsUpperSet (f i j)<GOAL>IsUpperSet (⋂ i, ⋂ j, f i j)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → Set α<VAR>hf : ∀ (i : ι) (j : κ i), IsLowerSet (f i j)<GOAL>IsLowerSet (⋂ i, ⋂ j, f i j)
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>IsLowerSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>IsUpperSet (⇑OrderDual.ofDual ⁻¹' s) ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set αᵒᵈ<GOAL>IsLowerSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set αᵒᵈ<GOAL>IsUpperSet (⇑OrderDual.toDual ⁻¹' s) ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>IsUpperSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsUpperSet s<VAR>ht : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t<GOAL>IsUpperSet (s \ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsLowerSet s<VAR>ht : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<GOAL>IsLowerSet (s \ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsUpperSet s<VAR>ht : IsLowerSet t<GOAL>IsUpperSet (s \ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Set α<VAR>hs : IsLowerSet s<VAR>ht : IsUpperSet t<GOAL>IsLowerSet (s \ t)
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>a : α<VAR>hs : IsUpperSet s<VAR>has : ∀ b ∈ s, b ≤ a → b = a<GOAL>IsUpperSet (s \ {a})
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>a : α<VAR>hs : IsLowerSet s<VAR>has : ∀ b ∈ s, a ≤ b → b = a<GOAL>IsLowerSet (s \ {a})
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsUpperSet (Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsLowerSet (Set.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsUpperSet (Set.Ioi a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsLowerSet (Set.Iio a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iic a ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsUpperSet s<VAR>a : α<VAR>ha : a ∈ s<GOAL>Set.Ioi a ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsLowerSet s<VAR>a : α<VAR>ha : a ∈ s<GOAL>Set.Iio a ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>s.OrdConnected
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>s.OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>f : β → α<VAR>hf : Monotone f<GOAL>IsUpperSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>f : β → α<VAR>hf : Monotone f<GOAL>IsLowerSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>f : α ≃o β<GOAL>IsUpperSet (⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>f : α ≃o β<GOAL>IsLowerSet (⇑f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : IsUpperSet (Set.range ⇑e)<VAR>a : α<GOAL>⇑e '' Set.Ici a = Set.Ici (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : IsLowerSet (Set.range ⇑e)<VAR>a : α<GOAL>⇑e '' Set.Iic a = Set.Iic (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : IsUpperSet (Set.range ⇑e)<VAR>a : α<GOAL>⇑e '' Set.Ioi a = Set.Ioi (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>he : IsLowerSet (Set.range ⇑e)<VAR>a : α<GOAL>⇑e '' Set.Iio a = Set.Iio (e a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>(Monotone fun x => x ∈ s) ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>(Antitone fun x => x ∈ s) ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<GOAL>IsUpperSet {a | p a} ↔ Monotone p
<VAR>α : Type u_1<VAR>Preorder α<VAR>p : α → Prop<GOAL>IsLowerSet {a | p a} ↔ Antitone p
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>s.Nonempty → upperBounds s ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>s.Nonempty → lowerBounds s ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderTop α<VAR>hs : IsLowerSet s<GOAL>⊤ ∈ s ↔ s = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderTop α<VAR>hs : IsUpperSet s<GOAL>⊤ ∈ s ↔ s.Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderTop α<VAR>hs : IsUpperSet s<GOAL>⊤ ∉ s ↔ s = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderBot α<VAR>hs : IsUpperSet s<GOAL>⊥ ∈ s ↔ s = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderBot α<VAR>hs : IsLowerSet s<GOAL>⊥ ∈ s ↔ s.Nonempty
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>OrderBot α<VAR>hs : IsLowerSet s<GOAL>⊥ ∉ s ↔ s = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>NoMaxOrder α<VAR>hs : IsUpperSet s<GOAL>s.Nonempty → ¬BddAbove s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMaxOrder α<GOAL>¬BddAbove (Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMaxOrder α<GOAL>¬BddAbove (Set.Ioi a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>NoMinOrder α<VAR>hs : IsLowerSet s<GOAL>s.Nonempty → ¬BddBelow s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMinOrder α<GOAL>¬BddBelow (Set.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>NoMinOrder α<GOAL>¬BddBelow (Set.Iio a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<GOAL>IsUpperSet s ↔ ∀ ⦃a b : α⦄, a < b → a ∈ s → b ∈ s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<GOAL>IsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<GOAL>IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Ioi a ⊆ s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<GOAL>IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Set.Iio a ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LE α<VAR>LE β<VAR>hf : Relation.Fibration (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) f<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>IsLowerSet (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>LE β<GOAL>Relation.Fibration (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) f ↔ ∀ (x : α), IsLowerSet (f '' Set.Iic x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>LE β<GOAL>Relation.Fibration (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) f ↔ ∀ (s : Set α), IsLowerSet s → IsLowerSet (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>hf : Monotone f<GOAL>Relation.Fibration (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) f ↔ ∀ (x : α), f '' Set.Iic x = Set.Iic (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LE α<VAR>LE β<VAR>hf : Relation.Fibration (fun x x_1 => x ≥ x_1) (fun x x_1 => x ≥ x_1) f<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>IsUpperSet (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>LE β<GOAL>Relation.Fibration (fun x x_1 => x ≥ x_1) (fun x x_1 => x ≥ x_1) f ↔ ∀ (x : α), IsUpperSet (f '' Set.Ici x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>LE β<GOAL>Relation.Fibration (fun x x_1 => x ≥ x_1) (fun x x_1 => x ≥ x_1) f ↔ ∀ (s : Set α), IsUpperSet s → IsUpperSet (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>Preorder α<VAR>Preorder β<VAR>hf : Monotone f<GOAL>Relation.Fibration (fun x x_1 => x ≥ x_1) (fun x x_1 => x ≥ x_1) f ↔ ∀ (x : α), f '' Set.Ici x = Set.Ici (f x)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<VAR>hs : IsUpperSet s<VAR>ht : IsUpperSet t<GOAL>s ⊆ t ∨ t ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<VAR>hs : IsLowerSet s<VAR>ht : IsLowerSet t<GOAL>s ⊆ t ∨ t ⊆ s
<VAR>α : Type u_6<VAR>LE α<VAR>self : UpperSet α<GOAL>IsUpperSet self.carrier
<VAR>α : Type u_6<VAR>LE α<VAR>self : LowerSet α<GOAL>IsLowerSet self.carrier
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>↑s = ↑t → s = t
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>s.carrier = ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>IsUpperSet ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>↑{ carrier := s, upper' := hs } = s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>a : α<GOAL>a ∈ { carrier := s, upper' := hs } ↔ a ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>↑s = ↑t → s = t