ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>Order.Coframe α<VAR>ι : Type u_1<VAR>Preorder ι<VAR>IsDirected ι (Function.swap fun x x_1 => x ≤ x_1)<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i
<VAR>α : Type u<VAR>Order.Coframe α<VAR>ι : Type u_1<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Antitone f<VAR>hg : Antitone g<GOAL>⨅ i, f i ⊔ g i = (⨅ i, f i) ⊔ ⨅ i, g i
<VAR>α : Type u_1<VAR>self : CompleteBooleanAlgebra α<VAR>a : α<VAR>s : Set α<GOAL>⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
<VAR>α : Type u_1<VAR>self : CompleteBooleanAlgebra α<VAR>a : α<VAR>s : Set α<GOAL>a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u<VAR>ι : Sort w<VAR>CompleteBooleanAlgebra α<VAR>f : ι → α<GOAL>(iInf f)ᶜ = ⨆ i, (f i)ᶜ
<VAR>α : Type u<VAR>ι : Sort w<VAR>CompleteBooleanAlgebra α<VAR>f : ι → α<GOAL>(iSup f)ᶜ = ⨅ i, (f i)ᶜ
<VAR>α : Type u<VAR>CompleteBooleanAlgebra α<VAR>s : Set α<GOAL>(sInf s)ᶜ = ⨆ i ∈ s, iᶜ
<VAR>α : Type u<VAR>CompleteBooleanAlgebra α<VAR>s : Set α<GOAL>(sSup s)ᶜ = ⨅ i ∈ s, iᶜ
<VAR>α : Type u<VAR>CompleteBooleanAlgebra α<VAR>s : Set α<GOAL>(sInf s)ᶜ = sSup (compl '' s)
<VAR>α : Type u<VAR>CompleteBooleanAlgebra α<VAR>s : Set α<GOAL>(sSup s)ᶜ = sInf (compl '' s)
<VAR>α : Type u<VAR>ι : Sort w<VAR>CompleteBooleanAlgebra α<VAR>f g : ι → α<GOAL>symmDiff (⨆ i, f i) (⨆ i, g i) ≤ ⨆ i, symmDiff (f i) (g i)
<VAR>α : Type u<VAR>ι : Sort w<VAR>CompleteBooleanAlgebra α<VAR>p : ι → Prop<VAR>f g : (i : ι) → p i → α<GOAL>symmDiff (⨆ i, ⨆ (h : p i), f i h) (⨆ i, ⨆ (h : p i), g i h) ≤ ⨆ i, ⨆ (h : p i), symmDiff (f i h) (g i h)
<VAR>α : Type u<VAR>self : CompleteAtomicBooleanAlgebra α<VAR>ι : Type u<VAR>κ : ι → Type u<VAR>f : (a : ι) → κ a → α<GOAL>⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
<VAR>s : Set PUnit.{u + 1}<GOAL>sSup s = PUnit.unit
<VAR>s : Set PUnit.{u + 1}<GOAL>sInf s = PUnit.unit
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HImp α<VAR>HImp β<VAR>a b : α × β<GOAL>(a ⇨ b).1 = a.1 ⇨ b.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HImp α<VAR>HImp β<VAR>a b : α × β<GOAL>(a ⇨ b).2 = a.2 ⇨ b.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HNot α<VAR>HNot β<VAR>a : α × β<GOAL>(￢a).1 = ￢a.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HNot α<VAR>HNot β<VAR>a : α × β<GOAL>(￢a).2 = ￢a.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SDiff α<VAR>SDiff β<VAR>a b : α × β<GOAL>(a \ b).1 = a.1 \ b.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SDiff α<VAR>SDiff β<VAR>a b : α × β<GOAL>(a \ b).2 = a.2 \ b.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HasCompl α<VAR>HasCompl β<VAR>a : α × β<GOAL>aᶜ.1 = a.1ᶜ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HasCompl α<VAR>HasCompl β<VAR>a : α × β<GOAL>aᶜ.2 = a.2ᶜ
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → HImp (π 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 : ι) → HNot (π i)<VAR>a : (i : ι) → π i<GOAL>￢a = fun i => ￢a i
<VAR>ι : Type u_1<VAR>π : ι → Type u_4<VAR>(i : ι) → HImp (π 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 : ι) → HNot (π i)<VAR>a : (i : ι) → π i<VAR>i : ι<GOAL>(￢a) i = ￢a i
<VAR>α : Type u_4<VAR>self : GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⇨ c ↔ a ⊓ b ≤ c
<VAR>α : Type u_4<VAR>self : GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ b ≤ c ↔ a ≤ b ⊔ c
<VAR>α : Type u_4<VAR>self : HeytingAlgebra α<VAR>a : α<GOAL>a ⇨ ⊥ = aᶜ
<VAR>α : Type u_4<VAR>self : CoheytingAlgebra α<VAR>a : α<GOAL>⊤ \ a = ￢a
<VAR>α : Type u_4<VAR>self : BiheytingAlgebra α<VAR>a : α<GOAL>⊤ \ a = ￢a
<VAR>α : Type u_4<VAR>self : BiheytingAlgebra α<VAR>a b c : α<GOAL>a \ b ≤ c ↔ a ≤ b ⊔ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⇨ c ↔ a ⊓ b ≤ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⇨ c ↔ b ⊓ a ≤ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⇨ c ↔ b ≤ a ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ≤ b ⇨ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ≤ a ⇨ b ↔ a ≤ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>a ⇨ a = ⊤
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>(a ⇨ b) ⊓ a ≤ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⊓ (a ⇨ b) ≤ 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>(a ⇨ b) ⊓ a = b ⊓ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇨ b = ⊤ ↔ a ≤ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>a ⇨ ⊤ = ⊤
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>⊤ ⇨ a = a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⇨ b ⇨ c = a ⊓ b ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>(b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⇨ b ⇨ c = b ⇨ a ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>b ⇨ b ⇨ a = b ⇨ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c)
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>c ⇨ a ≤ c ⇨ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>b ⇨ c ≤ a ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>b ⇨ c ≤ a ⇨ d
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⊔ b ⇨ a = b ⇨ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⊔ b ⇨ b = a ⇨ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>b ⇨ a = a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>a ⇨ b = b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>a ⇨ a ⊓ b = b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : Codisjoint a b<GOAL>b ⇨ a ⊓ b = a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<VAR>hac : Codisjoint a c<VAR>hba : b ≤ a<GOAL>c ⇨ b ≤ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ≤ (a ⇨ b) ⇨ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>b ⇨ a = a ⇨ b ↔ a = b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>b ⇨ a ≠ 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>GeneralizedHeytingAlgebra α<VAR>a b c : α<VAR>hba : b ≤ a<VAR>hcb : c ≤ b<GOAL>(a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ b ≤ c ↔ a ≤ b ⊔ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ b ≤ c ↔ a ≤ c ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ b ≤ c ↔ a \ c ≤ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ≤ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : Disjoint a b<GOAL>Disjoint (a \ c) b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : Disjoint a b<GOAL>Disjoint a (b \ c)
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ≤ b ↔ a ≤ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>a \ a = ⊥
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ≤ b ⊔ a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ≤ a \ b ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ⊔ a \ b = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ⊔ a = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ⊓ a = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ⊓ a \ b = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ⊔ b \ a = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>b \ a ⊔ a = b ⊔ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : c ≤ a<GOAL>a ⊔ b \ c = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>b ⊔ c \ a = c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a ⊔ b \ a = b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : b ≤ a<GOAL>a \ b ⊔ b = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : b ≤ c \ a<VAR>hac : a ≤ c<GOAL>a ⊔ b ≤ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : a ≤ c \ b<VAR>hbc : b ≤ c<GOAL>a ⊔ b ≤ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b = ⊥ ↔ a ≤ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>a \ ⊥ = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>⊥ \ a = ⊥
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>(a \ b) \ (a \ c) ≤ c \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⊔ (a \ c ⊔ c \ b)
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>(a \ b) \ c = a \ (b ⊔ c)
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>(a \ b) \ c = (a \ c) \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a \ b) \ b = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a \ b) \ a = ⊥
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>(a ⊔ b) \ c = a \ c ⊔ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ (b ⊓ c) = a \ b ⊔ a \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a ⊔ b) \ b = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a ⊔ b) \ a = b \ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>a \ c ≤ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>c \ b ≤ c \ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hcd : c ≤ d<GOAL>a \ d ≤ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ (a ⊓ b) = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>b \ (a ⊓ b) = b \ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : Disjoint a b<GOAL>a \ b = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : Disjoint a b<GOAL>b \ a = b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : Disjoint a b<GOAL>(a ⊔ b) \ a = b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : Disjoint a b<GOAL>(a ⊔ b) \ b = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>hac : Disjoint a c<VAR>hab : a ≤ b<GOAL>a ≤ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ (a \ b) ≤ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b = b \ a ↔ a = b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ≠ b \ a ↔ a ≠ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ c ≤ a \ b ⊔ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>hba : b ≤ a<VAR>hcb : c ≤ b<GOAL>a \ b ⊔ b \ c = a \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : c ⊔ a ≤ c ⊔ b<GOAL>a \ c ≤ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>h : a ⊔ c ≤ b ⊔ c<GOAL>a \ c ≤ b \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ c ⊓ (a ⊔ b) = a \ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a \ c ⊓ (b ⊔ a) = a \ c
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ⇨ ⊥ = aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>⊥ ⇨ a = ⊤
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>aᶜ ≤ a ⇨ b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>aᶜ ⊔ b ≤ a ⇨ b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>b ⊔ aᶜ ≤ a ⇨ b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ⇨ aᶜ = aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>a ⇨ bᶜ = b ⇨ aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>a ≤ bᶜ ↔ Disjoint a b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>a ≤ bᶜ ↔ Disjoint b a
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>a ≤ bᶜ ↔ b ≤ aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>Disjoint aᶜ a
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>Disjoint a aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Disjoint aᶜ b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Disjoint a bᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>aᶜ = b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>a = bᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h₀ : a ⊓ b = ⊥<VAR>h₁ : 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 α<GOAL>⊤ᶜ = ⊥
<VAR>α : Type u_2<VAR>HeytingAlgebra α<GOAL>⊥ᶜ = ⊤
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ≤ aᶜ ↔ a = ⊥
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<VAR>Nontrivial α<GOAL>a ≠ aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<VAR>Nontrivial α<GOAL>aᶜ ≠ a
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<VAR>Nontrivial α<GOAL>a < aᶜ ↔ a = ⊥
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>a ≤ aᶜᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<GOAL>Antitone compl
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>bᶜ ≤ aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>aᶜᶜᶜ = aᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>Disjoint aᶜᶜ b ↔ Disjoint a b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>Disjoint a bᶜᶜ ↔ Disjoint a b
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a b : α<GOAL>(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual (￢a) = (OrderDual.ofDual a)ᶜ
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>OrderDual.toDual aᶜ = ￢OrderDual.toDual a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>⊤ \ a = ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>a \ ⊤ = ⊥
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢(a ⊓ b) = ￢a ⊔ ￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ≤ ￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>a \ b ≤ a ⊓ ￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢a \ a = ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢a \ b = ￢b \ a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢a ≤ b ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢a ≤ b ↔ Codisjoint b a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢a ≤ b ↔ ￢b ≤ a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>Codisjoint a (￢a)
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>Codisjoint (￢a) a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Codisjoint (￢a) b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : b ≤ a<GOAL>Codisjoint a (￢b)
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>￢a = b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : IsCompl a b<GOAL>a = ￢b
<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 α<GOAL>￢⊥ = ⊤
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<GOAL>￢⊤ = ⊥
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢￢a ≤ a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<GOAL>Antitone hnot
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>￢b ≤ ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢￢￢a = ￢a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>Codisjoint (￢￢a) b ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>Codisjoint a (￢￢b) ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢(a ⊔ b) ≤ ￢a ⊓ ￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>￢￢(a \ b) = ￢￢a \ ￢￢b
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : αᵒᵈ<GOAL>OrderDual.ofDual aᶜ = ￢OrderDual.ofDual a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a ⇨ b) = OrderDual.ofDual b \ OrderDual.ofDual a
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>OrderDual.toDual (￢a) = (OrderDual.toDual a)ᶜ
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>OrderDual.toDual (a \ b) = OrderDual.toDual b ⇨ OrderDual.toDual a
<VAR>α : Type u_2<VAR>BiheytingAlgebra α<VAR>a : α<GOAL>aᶜ ≤ ￢a
<VAR>p q : Prop<GOAL>p ⇨ q ↔ p → q
<VAR>p : Prop<GOAL>pᶜ ↔ ¬p
<VAR>a b : PUnit.{u + 1}<GOAL>a ⊔ b = PUnit.unit
<VAR>a b : PUnit.{u + 1}<GOAL>a ⊓ b = PUnit.unit
<VAR>a : PUnit.{u + 1}<GOAL>aᶜ = PUnit.unit
<VAR>a b : PUnit.{u + 1}<GOAL>a \ b = PUnit.unit
<VAR>a : PUnit.{u + 1}<GOAL>￢a = PUnit.unit
<VAR>a b : PUnit.{u + 1}<GOAL>a ⇨ b = PUnit.unit
<VAR>α : Type u_1<VAR>OmegaCompletePartialOrder α<GOAL>↑(ωCPO.of α) = α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>b : ↑(Set.Iic a)<VAR>h : CompleteLattice.IsCompactElement ↑b<GOAL>CompleteLattice.IsCompactElement b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Set.Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<GOAL>ComplementedLattice α
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>self : RelSeries r<VAR>i : Fin self.length<GOAL>r (self.toFun i.castSucc) (self.toFun i.succ)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>a : α<GOAL>∀ (x : Fin (0 + 1)), (RelSeries.singleton r a).toFun x = a
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>a : α<GOAL>(RelSeries.singleton r a).length = 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x y : RelSeries r<VAR>length_eq : x.length = y.length<VAR>toFun_eq : x.toFun = y.toFun ∘ Fin.cast ⋯<GOAL>x = y
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>IsTrans α r<VAR>x : RelSeries r<VAR>i j : Fin (x.length + 1)<VAR>h : i < j<GOAL>r (x.toFun i) (x.toFun j)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>IsTrans α r<VAR>x : RelSeries r<VAR>i j : Fin (x.length + 1)<VAR>h : i ≤ j<GOAL>r (x.toFun i) (x.toFun j) ∨ x.toFun i = x.toFun j
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<VAR>s : Rel α α<VAR>h : r ≤ s<GOAL>(x.ofLE h).length = x.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<VAR>s : Rel α α<VAR>h : r ≤ s<GOAL>∀ (a : Fin (x.length + 1)), (x.ofLE h).toFun a = x.toFun a
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<VAR>s : Rel α α<VAR>h : r ≤ s<GOAL>(x.ofLE h).toFun = x.toFun
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>x.toList.length = x.length + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>List.Chain' r x.toList
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>x.toList ≠ []
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : List α<VAR>x_ne_nil : x ≠ []<VAR>hx : List.Chain' r x<GOAL>(RelSeries.fromListChain' x x_ne_nil hx).length = x.length.pred
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : List α<VAR>x_ne_nil : x ≠ []<VAR>hx : List.Chain' r x<GOAL>∀ (a : Fin (x.length.pred + 1)), (RelSeries.fromListChain' x x_ne_nil hx).toFun a = (x.get ∘ Fin.cast ⋯) a
<VAR>α : Type u_1<VAR>r : Rel α α<GOAL>Function.Injective RelSeries.toList
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>self : r.FiniteDimensional<GOAL>∃ x, ∀ (y : RelSeries r), y.length ≤ x.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>self : r.InfiniteDimensional<VAR>n : ℕ<GOAL>∃ x, x.length = n
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>r.FiniteDimensional<VAR>x : RelSeries r<GOAL>x.length ≤ (RelSeries.longestOf r).length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>r.InfiniteDimensional<VAR>n : ℕ<GOAL>(RelSeries.withLength r n).length = n
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>r.InfiniteDimensional<GOAL>Nonempty α
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>x : α<GOAL>x ∈ s ↔ x ∈ Set.range s.toFun
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>x : α<GOAL>x ∈ s.toList ↔ x ∈ s
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>hs : s.length = 0<GOAL>{x | x ∈ s}.Subsingleton
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>h : {x | x ∈ s}.Nontrivial<GOAL>s.length ≠ 0
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>h : {x | x ∈ s}.Nontrivial<GOAL>0 < s.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>irrefl : Irreflexive r<GOAL>s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>irrefl : Irreflexive r<GOAL>0 < s.length ↔ {x | x ∈ s}.Nontrivial
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>irrefl : Irreflexive r<GOAL>s.length = 0 ↔ {x | x ∈ s}.Subsingleton
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>x.toFun (Fin.last x.length) = x.last
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>x.head ∈ x
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>x : RelSeries r<GOAL>x.last ∈ x
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>(p.append q connect).length = p.length + q.length + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (p.length + 1)<GOAL>(p.append q connect).toFun (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) = p.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<VAR>i : Fin (q.length + 1)<GOAL>(p.append q connect).toFun (↑↑(Fin.natAdd p.length i) + 1) = q.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>(p.append q connect).head = p.head
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : r p.last q.head<GOAL>(p.append q connect).last = q.last
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>f : r →r s<GOAL>(p.map f).length = p.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>f : r →r s<VAR>i : Fin (p.length + 1)<GOAL>(p.map f).toFun i = f (p.toFun i)
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<VAR>j : Fin (p.length + 1 + 1)<GOAL>(p.insertNth i a prev_connect connect_next).toFun j = i.succ.castSucc.insertNth a p.toFun j
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>i : Fin p.length<VAR>a : α<VAR>prev_connect : r (p.toFun i.castSucc) a<VAR>connect_next : r a (p.toFun i.succ)<GOAL>(p.insertNth i a prev_connect connect_next).length = p.length + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<GOAL>p.reverse.length = p.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>i : Fin (p.length + 1)<GOAL>p.reverse.toFun i = p.toFun i.rev
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newHead : α<VAR>rel : r newHead p.head<GOAL>(p.cons newHead rel).length = p.length + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newHead : α<VAR>rel : r newHead p.head<GOAL>(p.cons newHead rel).head = newHead
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newHead : α<VAR>rel : r newHead p.head<GOAL>(p.cons newHead rel).last = p.last
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<GOAL>(p.snoc newLast rel).length = p.length + 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<GOAL>(p.snoc newLast rel).head = p.head
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<GOAL>(p.snoc newLast rel).last = newLast