ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>x y : α<GOAL>l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>f : ι → α<GOAL>l.toFun (⋃ i, ↑(l.toFun ↑(f i))) = l.toFun (⋃ i, ↑(f i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>f : (i : ι) → κ i → α<GOAL>l.toFun (⋃ i, ⋃ j, ↑(l.toFun ↑(f i j))) = l.toFun (⋃ i, ⋃ j, ↑(f i j))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>∀ (a : α), gc.lowerAdjoint.toFun a = l a
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x : α<GOAL>gc.closureOperator.IsClosed x = (u (l x) = x)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>x : α<GOAL>gc.closureOperator x = u (l x)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<GOAL>⋯.closureOperator = c
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>self : r ≼i s<VAR>a : α<VAR>b : β<GOAL>s b (self.toRelEmbedding a) → ∃ a', self.toRelEmbedding a' = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f g : r ≼i s<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≼i s<GOAL>⇑f.toRelEmbedding = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≼i s<VAR>a : α<VAR>b : β<GOAL>s b (f a) → ∃ a', f a' = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>a b : α<VAR>f : r ≼i s<GOAL>s (f a) (f b) ↔ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≼i s<VAR>a : α<VAR>b : β<GOAL>s b (f a) ↔ ∃ a', f a' = b ∧ r a' a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>x : α<GOAL>(InitialSeg.refl r) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≼i s<VAR>g : s ≼i t<VAR>a : α<GOAL>(f.trans g) a = g (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f g : r ≼i s<VAR>a : α<GOAL>f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>f : r ≼i s<VAR>g : s ≼i r<GOAL>Function.LeftInverse ⇑g ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ≼i s<VAR>g : s ≼i r<GOAL>⇑(f.antisymm g) = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder α r<VAR>IsWellOrder β s<VAR>f : r ≼i s<VAR>g : s ≼i r<GOAL>(f.antisymm g).symm = g.antisymm f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ≼i s<GOAL>Function.Surjective ⇑f ∨ ∃ b, ∀ (x : β), s x b ↔ ∃ y, f y = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>p : Set β<VAR>f : r ≼i s<VAR>H : ∀ (a : α), f a ∈ p<VAR>a : α<GOAL>(InitialSeg.codRestrict p f H) a = ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>a : α<GOAL>(InitialSeg.leAdd r s) a = Sum.inl a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≼i s<VAR>a : α<GOAL>Acc r a ↔ Acc s (f a)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>self : r ≺i s<VAR>b : β<GOAL>s b self.top ↔ ∃ a, self.toRelEmbedding a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>t : β<VAR>o : ∀ (b : β), s b t ↔ ∃ a, f a = b<GOAL>⇑{ toRelEmbedding := f, top := t, down' := o }.toRelEmbedding = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≺i s<VAR>b : β<GOAL>s b f.top ↔ ∃ a, f.toRelEmbedding a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≺i s<VAR>a : α<GOAL>s (f.toRelEmbedding a) f.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans β s<VAR>f : r ≺i s<VAR>a : α<VAR>b : β<VAR>h : s b (f.toRelEmbedding a)<GOAL>∃ a', f.toRelEmbedding a' = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans β s<VAR>f : r ≺i s<GOAL>⇑{ toRelEmbedding := f.toRelEmbedding, init' := ⋯ } = ⇑f.toRelEmbedding
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans β s<VAR>f : r ≺i s<VAR>a : α<VAR>b : β<GOAL>s b (f.toRelEmbedding a) ↔ ∃ a', f.toRelEmbedding a' = b ∧ r a' a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsWellOrder α r<VAR>f : r ≺i r<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≺i s<VAR>g : s ≼i t<VAR>a : α<GOAL>(f.ltLe g).toRelEmbedding a = g (f.toRelEmbedding a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≺i s<VAR>g : s ≼i t<GOAL>(f.ltLe g).top = g f.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>IsTrans γ t<VAR>f : r ≺i s<VAR>g : s ≺i t<VAR>a : α<GOAL>(f.trans g).toRelEmbedding a = g.toRelEmbedding (f.toRelEmbedding a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>IsTrans γ t<VAR>f : r ≺i s<VAR>g : s ≺i t<GOAL>(f.trans g).top = g.toRelEmbedding f.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≃r s<VAR>g : s ≺i t<VAR>a : α<GOAL>(PrincipalSeg.equivLT f g).toRelEmbedding a = g.toRelEmbedding (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>f : r ≃r s<VAR>g : s ≺i t<GOAL>(PrincipalSeg.equivLT f g).top = g.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>IsWellOrder γ t<VAR>e : r ≃r s<VAR>f : r ≺i t<VAR>g : s ≺i t<GOAL>f.top = g.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>IsWellOrder γ t<VAR>f : r ≺i s<VAR>g : s ≺i t<VAR>h : r ≺i t<GOAL>t h.top g.top
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>a : α<VAR>b : ↑{b | r b a}<GOAL>(PrincipalSeg.ofElement r a).toRelEmbedding b = ↑b
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>a : α<GOAL>(PrincipalSeg.ofElement r a).top = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≺i s<GOAL>∀ (a : α), f.subrelIso.symm a = (Equiv.setCongr ⋯) ⟨f.toRelEmbedding a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≺i s<VAR>b : ↑{b | s b f.top}<GOAL>f.toRelEmbedding (f.subrelIso b) = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≺i s<VAR>a : α<GOAL>f.subrelIso ⟨f.toRelEmbedding a, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>p : Set β<VAR>f : r ≺i s<VAR>H : ∀ (a : α), f.toRelEmbedding a ∈ p<VAR>H₂ : f.top ∈ p<VAR>a : α<GOAL>(PrincipalSeg.codRestrict p f H H₂).toRelEmbedding a = ⟨f.toRelEmbedding a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>p : Set β<VAR>f : r ≺i s<VAR>H : ∀ (a : α), f.toRelEmbedding a ∈ p<VAR>H₂ : f.top ∈ p<GOAL>(PrincipalSeg.codRestrict p f H H₂).top = ⟨f.top, H₂⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : β → β → Prop<VAR>r : α → α → Prop<VAR>IsEmpty α<VAR>b : β<VAR>H : ∀ (b' : β), ¬s b' b<GOAL>(PrincipalSeg.ofIsEmpty r H).top = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsTrans β s<VAR>f : r ≺i s<VAR>a : α<GOAL>Acc r a ↔ Acc s (f.toRelEmbedding a)
<VAR>β : Type u_4<VAR>s : β → β → Prop<VAR>IsTrans β s<GOAL>WellFounded s ↔ ∀ (b : β), WellFounded (Subrel s {b' | s b' b})
<VAR>β : Type u<VAR>s : β → β → Prop<VAR>IsTrans β s<GOAL>WellFounded s ↔ ∀ (α : Type u) (r : α → α → Prop), r ≺i s → WellFounded r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ≼i s<VAR>g : r ≺i s<VAR>a : α<GOAL>g.toRelEmbedding a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ≼i s<VAR>g : r ≃r s<VAR>a : α<GOAL>g a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>IsWellOrder β s<VAR>IsTrans γ t<VAR>f : r ≼i s<VAR>g : s ≺i t<VAR>a : α<GOAL>(f.leLT g).toRelEmbedding a = g.toRelEmbedding (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ↪r s<VAR>a a' : α<GOAL>r a' a → s ↑(f.collapseF a') ↑(f.collapseF a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<VAR>b : β<VAR>h : ∀ (a' : α), r a' a → s (↑(f.collapseF a')) b<GOAL>¬s b ↑(f.collapseF a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<GOAL>f.collapse a = ↑(f.collapseF a)
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>a ⊓ ￢a = ∂ a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>∂ a ≤ a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>∂ a ≤ ￢a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<GOAL>∂ ⊥ = ⊥
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<GOAL>∂ ⊤ = ⊥
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>∂ (￢a) ≤ ∂ a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>∂ (￢￢a) = ∂ (￢a)
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢∂ a = ⊤
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ (a ⊓ b) ≤ ∂ a ⊔ ∂ b
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ b ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a b : α<GOAL>∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ b
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>∂ ∂ a = ∂ a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢￢a ⊔ ∂ a = a
<VAR>α : Type u_1<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>￢a = ⊤ ↔ ∃ b, ∂ b = a
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a : α<GOAL>∂ a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>Subsingleton α<GOAL>Disjoint a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b ↔ Disjoint b a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b → Disjoint b a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<GOAL>Symmetric Disjoint
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>Disjoint ⊥ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>Disjoint a ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>Disjoint b d → Disjoint a c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Disjoint b c → Disjoint a c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b c : α<GOAL>b ≤ c → Disjoint a c → Disjoint a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a : α<GOAL>Disjoint a a ↔ a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>ha : a ≠ ⊥<VAR>hab : Disjoint a b<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>hab : Disjoint a b<VAR>h : a ≤ b<GOAL>a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>hab : Disjoint a b<GOAL>b ≤ a → b = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>hab : Disjoint a b<GOAL>a = b ↔ a = ⊥ ∧ b = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>a b : α<VAR>hab : Disjoint a b<GOAL>a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a : α<GOAL>Disjoint a ⊤ ↔ a = ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a : α<GOAL>Disjoint ⊤ a ↔ a = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b ↔ a ⊓ b ≤ ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b ↔ a ⊓ b = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b → a ⊓ b ≤ ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b → a ⊓ b = ⊥
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b c : α<GOAL>Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b c : α<GOAL>Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b c : α<GOAL>Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>c : α<VAR>h : Disjoint a b<GOAL>Disjoint (a ⊓ c) b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>c : α<VAR>h : Disjoint a b<GOAL>Disjoint (c ⊓ a) b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>c : α<VAR>h : Disjoint a b<GOAL>Disjoint a (b ⊓ c)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<VAR>c : α<VAR>h : Disjoint a b<GOAL>Disjoint a (c ⊓ b)
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b c : α<VAR>h : Disjoint (a ⊓ b) c<VAR>hle : a ≤ c<GOAL>Disjoint a b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b c : α<VAR>h : Disjoint (a ⊓ b) c<VAR>hle : b ≤ c<GOAL>Disjoint a b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<GOAL>Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<GOAL>Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<VAR>ha : Disjoint a c<VAR>hb : Disjoint b c<GOAL>Disjoint (a ⊔ b) c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<VAR>hb : Disjoint a b<VAR>hc : Disjoint a c<GOAL>Disjoint a (b ⊔ c)
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<VAR>h : a ≤ b ⊔ c<VAR>hd : Disjoint a c<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b c : α<VAR>h : a ≤ c ⊔ b<VAR>hd : Disjoint a c<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b ↔ Codisjoint b a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b → Codisjoint b a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<GOAL>Symmetric Codisjoint
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>Codisjoint ⊤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>Codisjoint a ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>Codisjoint a c → Codisjoint b d
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Codisjoint a c → Codisjoint b c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b c : α<GOAL>b ≤ c → Codisjoint a b → Codisjoint a c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a : α<GOAL>Codisjoint a a ↔ a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>ha : a ≠ ⊤<VAR>hab : Codisjoint a b<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>hab : Codisjoint a b<VAR>h : b ≤ a<GOAL>a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>hab : Codisjoint a b<GOAL>a ≤ b → b = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>hab : Codisjoint a b<GOAL>a = b ↔ a = ⊤ ∧ b = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>a b : α<VAR>hab : Codisjoint a b<GOAL>a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a : α<GOAL>Codisjoint a ⊥ ↔ a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a : α<GOAL>Codisjoint ⊥ a ↔ a = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a b : α<VAR>h : Codisjoint a b<VAR>ha : a ≠ ⊤<GOAL>b ≠ ⊥
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a b : α<VAR>h : Codisjoint a b<VAR>hb : b ≠ ⊤<GOAL>a ≠ ⊥
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b ↔ ⊤ ≤ a ⊔ b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b ↔ a ⊔ b = ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b → ⊤ ≤ a ⊔ b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b → a ⊔ b = ⊤
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b c : α<GOAL>Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b c : α<GOAL>Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b c : α<GOAL>Codisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<VAR>c : α<VAR>h : Codisjoint a b<GOAL>Codisjoint (a ⊔ c) b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<VAR>c : α<VAR>h : Codisjoint a b<GOAL>Codisjoint (c ⊔ a) b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<VAR>c : α<VAR>h : Codisjoint a b<GOAL>Codisjoint a (b ⊔ c)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<VAR>c : α<VAR>h : Codisjoint a b<GOAL>Codisjoint a (c ⊔ b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b c : α<VAR>h : Codisjoint (a ⊔ b) c<VAR>hle : c ≤ a<GOAL>Codisjoint a b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b c : α<VAR>h : Codisjoint (a ⊔ b) c<VAR>hle : c ≤ b<GOAL>Codisjoint a b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<GOAL>Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<GOAL>Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<VAR>ha : Codisjoint a c<VAR>hb : Codisjoint b c<GOAL>Codisjoint (a ⊓ b) c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<VAR>hb : Codisjoint a b<VAR>hc : Codisjoint a c<GOAL>Codisjoint a (b ⊓ c)
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<VAR>h : a ⊓ b ≤ c<VAR>hd : Codisjoint b c<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderTop α<VAR>a b c : α<VAR>h : b ⊓ a ≤ c<VAR>hd : Codisjoint b c<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Disjoint a b → Codisjoint (OrderDual.toDual a) (OrderDual.toDual b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Codisjoint a b → Disjoint (OrderDual.toDual a) (OrderDual.toDual b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : α<GOAL>Disjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Codisjoint a b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : αᵒᵈ<GOAL>Disjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Codisjoint a b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>a b : α<GOAL>Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Disjoint a b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>a b : αᵒᵈ<GOAL>Codisjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Disjoint a b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b c : α<VAR>hab : Disjoint a b<VAR>hbc : Codisjoint b c<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>x y : α<VAR>self : IsCompl x y<GOAL>Codisjoint x y
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>x y : α<VAR>self : IsCompl x y<GOAL>Disjoint x y
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a b : α<GOAL>IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>x y : α<VAR>h : IsCompl x y<GOAL>IsCompl y x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>x y : α<GOAL>IsCompl x y ↔ IsCompl y x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>x y : α<VAR>h : IsCompl x y<GOAL>IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<VAR>a b : αᵒᵈ<VAR>h : IsCompl a b<GOAL>IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b)
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x y : α<VAR>h₁ : x ⊓ y ≤ ⊥<VAR>h₂ : ⊤ ≤ x ⊔ y<GOAL>IsCompl x y
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x y : α<VAR>h₁ : x ⊓ y = ⊥<VAR>h₂ : x ⊔ y = ⊤<GOAL>IsCompl x y
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x y : α<VAR>h : IsCompl x y<GOAL>x ⊓ y = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x y : α<VAR>h : IsCompl x y<GOAL>x ⊔ y = ⊤
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>a b x y : α<VAR>h : IsCompl x y<VAR>hle : a ≤ b ⊔ y<GOAL>a ⊓ x ≤ b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y a b : α<VAR>h : IsCompl x y<GOAL>a ≤ b ⊔ y ↔ a ⊓ x ≤ b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl y z<GOAL>x ⊓ y = ⊥ ↔ x ≤ z
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl y z<GOAL>x ⊓ z = ⊥ ↔ x ≤ y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl y z<GOAL>Disjoint x y ↔ x ≤ z
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl y z<GOAL>Disjoint x z ↔ x ≤ y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl x y<GOAL>z ≤ x ↔ Disjoint z y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl x y<GOAL>z ≤ y ↔ Disjoint z x
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl x y<GOAL>x ≤ z ↔ Codisjoint z y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>h : IsCompl x y<GOAL>y ≤ z ↔ Codisjoint z x
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y x' y' : α<VAR>h : IsCompl x y<VAR>h' : IsCompl x' y'<VAR>hx : x ≤ x'<GOAL>y' ≤ y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>hxy : IsCompl x y<VAR>hxz : IsCompl x z<GOAL>y = z
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y z : α<VAR>hxz : IsCompl x z<VAR>hyz : IsCompl y z<GOAL>x = y
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y x' y' : α<VAR>h : IsCompl x y<VAR>h' : IsCompl x' y'<GOAL>IsCompl (x ⊔ x') (y ⊓ y')
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<VAR>x y x' y' : α<VAR>h : IsCompl x y<VAR>h' : IsCompl x' y'<GOAL>IsCompl (x ⊓ x') (y ⊔ y')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>x y : α × β<GOAL>Disjoint x y ↔ Disjoint x.1 y.1 ∧ Disjoint x.2 y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>x y : α × β<GOAL>Codisjoint x y ↔ Codisjoint x.1 y.1 ∧ Codisjoint x.2 y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>x y : α × β<GOAL>IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>a b : α<GOAL>IsCompl (OrderDual.toDual a) (OrderDual.toDual b) ↔ IsCompl a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>a b : αᵒᵈ<GOAL>IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ IsCompl a b
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>IsCompl ⊥ ⊤
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>IsCompl ⊤ ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x : α<VAR>h : IsCompl x ⊥<GOAL>x = ⊤
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x : α<VAR>h : IsCompl ⊥ x<GOAL>x = ⊤
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x : α<VAR>h : IsCompl x ⊤<GOAL>x = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<VAR>x : α<VAR>h : IsCompl ⊤ x<GOAL>x = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>IsComplemented ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>BoundedOrder α<GOAL>IsComplemented ⊤