ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ b = a ⊔ b ⇨ a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>a ⇔ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⊔ b ⇨ a ⇔ b = a ⇔ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ (a ⇨ b) = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>(b ⇨ a) ⇔ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⊓ (a ⊔ b) = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>(a ⊔ b) ⊓ a ⇔ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⇔ (a ⊔ b) = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>(a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>a ∆ ⊤ = ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>⊤ ∆ a = ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>(￢a) ∆ a = ⊤
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>a ∆ (￢a) = ⊤
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>a ∆ b = ⊤
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ⇔ ⊥ = aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>⊥ ⇔ a = aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>aᶜ ⇔ a = ⊥
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ⇔ aᶜ = ⊥
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>a ⇔ b = ⊥
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>(a ⊔ b) \ a ∆ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Disjoint (a ∆ b) (a ⊓ b)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b \ a = b \ a
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b \ b = a \ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a \ a ∆ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>b \ a ∆ b = a ⊓ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = a ⊔ b ↔ Disjoint a b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ≤ a ∆ b ↔ Disjoint a b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>b ≤ a ∆ b ↔ Disjoint a b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b ∆ c = a ∆ (b ∆ c)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ (b ∆ c) = b ∆ (a ∆ c)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b ∆ c = a ∆ c ∆ b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ (a ∆ b) = b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>b ∆ a ∆ a = b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b ∆ a = b
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Involutive fun x => x ∆ a
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Involutive fun x => a ∆ x
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Injective fun x => x ∆ a
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Injective fun x => a ∆ x
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Surjective fun x => x ∆ a
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a : α<GOAL>Function.Surjective fun x => a ∆ x
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b = c ∆ b ↔ a = c
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ b = a ∆ c ↔ b = c
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = a ↔ b = ⊥
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = b ↔ a = ⊥
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<VAR>ha : Disjoint a c<VAR>hb : Disjoint b c<GOAL>Disjoint (a ∆ b) c
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<VAR>ha : Disjoint a b<VAR>hb : Disjoint a c<GOAL>Disjoint a (b ∆ c)
<VAR>α : Type u_2<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<VAR>ha : a ≤ c<GOAL>a ∆ b = c ↔ c \ a = b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⇨ a ⊓ b = a ⊔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>Codisjoint (a ⇔ b) (a ⊔ b)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇨ a ⇔ b = a ⇨ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>b ⇨ a ⇔ b = b ⇨ a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⇨ a = a ⊔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⇨ b = a ⊔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = a ⊓ b ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ≤ a ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ≤ b ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ⇔ b ⇔ c = a ⇔ (b ⇔ c)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ⇔ b ⇔ c = a ⇔ c ⇔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ (a ⇔ b) = b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>b ⇔ a ⇔ a = b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b ⇔ a = b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Involutive fun x => x ⇔ a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Involutive fun x => a ⇔ x
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Injective fun x => x ⇔ a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Injective fun x => a ⇔ x
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Surjective fun x => x ⇔ a
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Function.Surjective fun x => a ⇔ x
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ⇔ b = c ⇔ b ↔ a = c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ⇔ b = a ⇔ c ↔ b = c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = a ↔ b = ⊤
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = b ↔ a = ⊤
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>ha : Codisjoint a c<VAR>hb : Codisjoint b c<GOAL>Codisjoint (a ⇔ b) c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>ha : Codisjoint a b<VAR>hb : Codisjoint a c<GOAL>Codisjoint a (b ⇔ c)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = a ⊓ b ⊔ aᶜ ⊓ bᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>a ∆ ⊤ = aᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>⊤ ∆ a = aᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>(a ∆ b)ᶜ = a ⇔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>(a ⇔ b)ᶜ = a ∆ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>aᶜ ∆ bᶜ = a ∆ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>aᶜ ⇔ bᶜ = a ⇔ b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ∆ b = ⊤ ↔ IsCompl a b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b : α<GOAL>a ⇔ b = ⊥ ↔ IsCompl a b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>aᶜ ∆ a = ⊤
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>a ∆ aᶜ = ⊤
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<GOAL>a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>h : Disjoint a b<GOAL>c ≤ a ∆ c ⊔ b ∆ c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>h : Disjoint b c<GOAL>a ≤ a ∆ b ⊔ a ∆ c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>h : Codisjoint a b<GOAL>a ⇔ c ⊓ b ⇔ c ≤ c
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a b c : α<VAR>h : Codisjoint b c<GOAL>a ⇔ b ⊓ a ⇔ c ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GeneralizedCoheytingAlgebra α<VAR>GeneralizedCoheytingAlgebra β<VAR>a b : α × β<GOAL>(a ∆ b).1 = a.1 ∆ b.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GeneralizedCoheytingAlgebra α<VAR>GeneralizedCoheytingAlgebra β<VAR>a b : α × β<GOAL>(a ∆ b).2 = a.2 ∆ b.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GeneralizedHeytingAlgebra α<VAR>GeneralizedHeytingAlgebra β<VAR>a b : α × β<GOAL>(a ⇔ b).1 = a.1 ⇔ b.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>GeneralizedHeytingAlgebra α<VAR>GeneralizedHeytingAlgebra β<VAR>a b : α × β<GOAL>(a ⇔ b).2 = a.2 ⇔ b.2
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → GeneralizedCoheytingAlgebra (π i)<VAR>a b : (i : ι) → π i<GOAL>a ∆ b = fun i => a i ∆ b i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → GeneralizedHeytingAlgebra (π i)<VAR>a b : (i : ι) → π i<GOAL>a ⇔ b = fun i => a i ⇔ b i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → GeneralizedCoheytingAlgebra (π i)<VAR>a b : (i : ι) → π i<VAR>i : ι<GOAL>(a ∆ b) i = a i ∆ b i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → GeneralizedHeytingAlgebra (π i)<VAR>a b : (i : ι) → π i<VAR>i : ι<GOAL>(a ⇔ b) i = a i ⇔ b i
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : SuccOrder α<VAR>a b : α<GOAL>a < b → SuccOrder.succ a ≤ b
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : SuccOrder α<VAR>a b : α<GOAL>a < SuccOrder.succ b → a ≤ b
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : SuccOrder α<VAR>a : α<GOAL>a ≤ SuccOrder.succ a
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : SuccOrder α<VAR>a : α<GOAL>SuccOrder.succ a ≤ a → IsMax a
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : PredOrder α<VAR>a : α<GOAL>a ≤ PredOrder.pred a → IsMin a
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : PredOrder α<VAR>a b : α<GOAL>PredOrder.pred a < b → a ≤ b
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : PredOrder α<VAR>a b : α<GOAL>a < b → a ≤ PredOrder.pred b
<VAR>α : Type u_3<VAR>Preorder α<VAR>self : PredOrder α<VAR>a : α<GOAL>PredOrder.pred a ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>succ : α → α<VAR>hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b<VAR>hm : ∀ (a : α), IsMax a → succ a = a<GOAL>∀ (a : α), SuccOrder.succ a = succ a
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>pred : α → α<VAR>hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b ≤ pred a ↔ b < a<VAR>hm : ∀ (a : α), IsMin a → pred a = a<GOAL>∀ (a : α), PredOrder.pred a = pred a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<GOAL>a ≤ Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ a ≤ a → IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<GOAL>a < b → Order.succ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<GOAL>a < Order.succ b → a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ a ≤ a ↔ IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<GOAL>a < Order.succ a ↔ ¬IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<GOAL>a ⩿ Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<VAR>h : ¬IsMax a<GOAL>a ⋖ Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>b < Order.succ a ↔ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>Order.succ a ≤ b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a < b<VAR>hb : ¬IsMax b<GOAL>Order.succ a < Order.succ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>Order.succ a < Order.succ b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>Order.succ a ≤ Order.succ b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Order.succ a ≤ Order.succ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<GOAL>Monotone Order.succ
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>b ≤ Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>k : ℕ<VAR>x : α<GOAL>x ≤ Order.succ^[k] x
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<VAR>n m : ℕ<VAR>h_eq : Order.succ^[n] a = Order.succ^[m] a<VAR>h_lt : n < m<GOAL>IsMax (Order.succ^[n] a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<VAR>n m : ℕ<VAR>h_eq : Order.succ^[n] a = Order.succ^[m] a<VAR>h_ne : n ≠ m<GOAL>IsMax (Order.succ^[n] a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<VAR>ha : ¬IsMax a<GOAL>Set.Iio (Order.succ a) = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a : α<VAR>ha : ¬IsMax a<GOAL>Set.Ici (Order.succ a) = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>hb : ¬IsMax b<GOAL>Set.Ico a (Order.succ b) = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>hb : ¬IsMax b<GOAL>Set.Ioo a (Order.succ b) = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>Set.Icc (Order.succ a) b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>Set.Ico (Order.succ a) b = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>a < Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>a < Order.succ b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a ≤ b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a ≤ Order.succ b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a < Order.succ b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<GOAL>StrictMono Order.succ
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>a ⋖ Order.succ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Iio (Order.succ a) = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Ici (Order.succ a) = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Ico a (Order.succ b) = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Ioo a (Order.succ b) = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Icc (Order.succ a) b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Ico (Order.succ a) b = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ a = a ↔ IsMax a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<VAR>hb : ¬IsMax b<GOAL>Order.succ a = Order.succ b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<GOAL>a ≤ b ∧ b ≤ Order.succ a ↔ b = a ∨ b = Order.succ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Order.succ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<GOAL>a ≤ Order.succ b ↔ a = Order.succ b ∨ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>hb : ¬IsMax b<GOAL>a < Order.succ b ↔ a = b ∨ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<GOAL>Set.Iic (Order.succ a) = insert (Order.succ a) (Set.Iic a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a ≤ Order.succ b<GOAL>Set.Icc a (Order.succ b) = insert (Order.succ b) (Set.Icc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>h : a < Order.succ b<GOAL>Set.Ioc a (Order.succ b) = insert (Order.succ b) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>h : ¬IsMax a<GOAL>Set.Iio (Order.succ a) = insert a (Set.Iio a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>h₁ : a ≤ b<VAR>h₂ : ¬IsMax b<GOAL>Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>h₁ : a < b<VAR>h₂ : ¬IsMax b<GOAL>Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a = Order.succ b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>NoMaxOrder α<GOAL>Function.Injective Order.succ
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a ≠ Order.succ b ↔ a ≠ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>a < Order.succ b ↔ a = b ∨ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<GOAL>Order.succ a = b ↔ a ⋖ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Iio (Order.succ a) = insert a (Set.Iio a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<VAR>h : a ≤ b<GOAL>Set.Ico a (Order.succ b) = insert b (Set.Ico a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a b : α<VAR>NoMaxOrder α<VAR>h : a < b<GOAL>Set.Ioo a (Order.succ b) = insert b (Set.Ioo a b)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>OrderTop α<GOAL>Order.succ ⊤ = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>OrderTop α<GOAL>Order.succ a ≤ a ↔ a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>OrderTop α<GOAL>a < Order.succ a ↔ a ≠ ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>OrderBot α<VAR>NoMaxOrder α<GOAL>a < Order.succ ⊥ ↔ a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>a : α<VAR>OrderBot α<GOAL>a ≤ Order.succ ⊥ ↔ a = ⊥ ∨ a = Order.succ ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>OrderBot α<VAR>Nontrivial α<VAR>a : α<GOAL>⊥ < Order.succ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>SuccOrder α<VAR>OrderBot α<VAR>Nontrivial α<VAR>a : α<GOAL>Order.succ a ≠ ⊥
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>SuccOrder α<VAR>a : α<GOAL>Order.succ a = ⨅ b, ⨅ (_ : a < b), b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred a ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<GOAL>a ≤ Order.pred a → IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<GOAL>a < b → a ≤ Order.pred b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred a < b → a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<GOAL>a ≤ Order.pred a ↔ IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred a < a ↔ ¬IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred a ⩿ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<VAR>h : ¬IsMin a<GOAL>Order.pred a ⋖ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Order.pred a < b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>b ≤ Order.pred a ↔ b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>h : a < b<VAR>ha : ¬IsMin a<GOAL>Order.pred a < Order.pred b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>Order.pred a < Order.pred b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>Order.pred a ≤ Order.pred b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Order.pred a ≤ Order.pred b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<GOAL>Monotone Order.pred
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>h : a ⩿ b<GOAL>Order.pred b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>k : ℕ<VAR>x : α<GOAL>Order.pred^[k] x ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<VAR>n m : ℕ<VAR>h_eq : Order.pred^[n] a = Order.pred^[m] a<VAR>h_lt : n < m<GOAL>IsMin (Order.pred^[n] a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<VAR>n m : ℕ<VAR>h_eq : Order.pred^[n] a = Order.pred^[m] a<VAR>h_ne : n ≠ m<GOAL>IsMin (Order.pred^[n] a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<VAR>ha : ¬IsMin a<GOAL>Set.Ioi (Order.pred a) = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a : α<VAR>ha : ¬IsMin a<GOAL>Set.Iic (Order.pred a) = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Set.Ioc (Order.pred a) b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Set.Ioo (Order.pred a) b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin b<GOAL>Set.Icc a (Order.pred b) = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin b<GOAL>Set.Ioc a (Order.pred b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Order.pred a < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a < b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>a ≤ Order.pred b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a ≤ Order.pred b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>a b : α<VAR>NoMinOrder α<GOAL>Order.pred a < Order.pred b ↔ a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<GOAL>StrictMono Order.pred
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Order.pred a ⋖ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Ioi (Order.pred a) = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Iic (Order.pred a) = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Ioc (Order.pred a) b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Ioo (Order.pred a) b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Icc a (Order.pred b) = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>PredOrder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Ioc a (Order.pred b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<GOAL>Order.pred a = a ↔ IsMin a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>Order.pred a = Order.pred b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = Order.pred a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>Order.pred b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<GOAL>Order.pred a ≤ b ↔ b = Order.pred a ∨ a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<GOAL>Order.pred a < b ↔ a = b ∨ a < b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<GOAL>Set.Ici (Order.pred a) = insert (Order.pred a) (Set.Ici a)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>a : α<VAR>ha : ¬IsMin a<GOAL>Set.Ioi (Order.pred a) = insert a (Set.Ioi a)