ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u<VAR>AddCommGroup A<VAR>n : ℤ<GOAL>QuotientAddGroup.homQuotientZSMulOfHom (AddMonoidHom.id A) n = AddMonoidHom.id (A ⧸ (zsmulAddGroupHom n).range)
<VAR>A B : Type u<VAR>CommGroup A<VAR>CommGroup B<VAR>f : A →* B<VAR>g : B →* A<VAR>n : ℤ<GOAL>QuotientGroup.homQuotientZPowOfHom (f.comp g) n = (QuotientGroup.homQuotientZPowOfHom f n).comp (QuotientGroup.homQuotientZPowOfHom g n)
<VAR>A B : Type u<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>f : A →+ B<VAR>g : B →+ A<VAR>n : ℤ<GOAL>QuotientAddGroup.homQuotientZSMulOfHom (f.comp g) n = (QuotientAddGroup.homQuotientZSMulOfHom f n).comp (QuotientAddGroup.homQuotientZSMulOfHom g n)
<VAR>A B : Type u<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>f : A →+ B<VAR>g : B →+ A<VAR>n : ℤ<VAR>i : Function.RightInverse ⇑g ⇑f<GOAL>(QuotientAddGroup.homQuotientZSMulOfHom f n).comp (QuotientAddGroup.homQuotientZSMulOfHom g n) = AddMonoidHom.id (B ⧸ (zsmulAddGroupHom n).range)
<VAR>A B : Type u<VAR>CommGroup A<VAR>CommGroup B<VAR>f : A →* B<VAR>g : B →* A<VAR>n : ℤ<VAR>i : Function.RightInverse ⇑g ⇑f<GOAL>(QuotientGroup.homQuotientZPowOfHom f n).comp (QuotientGroup.homQuotientZPowOfHom g n) = MonoidHom.id (B ⧸ (zpowGroupHom n).range)
<VAR>A : Type u<VAR>CommGroup A<VAR>n : ℤ<GOAL>MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = QuotientGroup.equivQuotientZPowOfEquiv (MulEquiv.refl A) n
<VAR>A : Type u<VAR>AddCommGroup A<VAR>n : ℤ<GOAL>AddEquiv.refl (A ⧸ (zsmulAddGroupHom n).range) = QuotientAddGroup.equivQuotientZSMulOfEquiv (AddEquiv.refl A) n
<VAR>A B : Type u<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>e : A ≃+ B<VAR>n : ℤ<GOAL>(QuotientAddGroup.equivQuotientZSMulOfEquiv e n).symm = QuotientAddGroup.equivQuotientZSMulOfEquiv e.symm n
<VAR>A B : Type u<VAR>CommGroup A<VAR>CommGroup B<VAR>e : A ≃* B<VAR>n : ℤ<GOAL>(QuotientGroup.equivQuotientZPowOfEquiv e n).symm = QuotientGroup.equivQuotientZPowOfEquiv e.symm n
<VAR>A B C : Type u<VAR>CommGroup A<VAR>CommGroup B<VAR>CommGroup C<VAR>e : A ≃* B<VAR>d : B ≃* C<VAR>n : ℤ<GOAL>(QuotientGroup.equivQuotientZPowOfEquiv e n).trans (QuotientGroup.equivQuotientZPowOfEquiv d n) = QuotientGroup.equivQuotientZPowOfEquiv (e.trans d) n
<VAR>A B C : Type u<VAR>AddCommGroup A<VAR>AddCommGroup B<VAR>AddCommGroup C<VAR>e : A ≃+ B<VAR>d : B ≃+ C<VAR>n : ℤ<GOAL>(QuotientAddGroup.equivQuotientZSMulOfEquiv e n).trans (QuotientAddGroup.equivQuotientZSMulOfEquiv d n) = QuotientAddGroup.equivQuotientZSMulOfEquiv (e.trans d) n
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>M : AddSubgroup G<VAR>nM : M.Normal<VAR>h : N ≤ M<VAR>x : G ⧸ N<GOAL>(QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientAddGroup.map N M (AddMonoidHom.id G) h) x
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>M : Subgroup G<VAR>nM : M.Normal<VAR>h : N ≤ M<VAR>x : G ⧸ N<GOAL>(QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) x
<VAR>G : Type u<VAR>AddGroup G<VAR>N : AddSubgroup G<VAR>nN : N.Normal<VAR>M : AddSubgroup G<VAR>nM : M.Normal<VAR>h : N ≤ M<VAR>x : G<GOAL>(QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>M : Subgroup G<VAR>nM : M.Normal<VAR>h : N ≤ M<VAR>x : G<GOAL>(QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
<VAR>G : Type u<VAR>AddGroup G<GOAL>Subsingleton (G ⧸ ⊤)
<VAR>G : Type u<VAR>Group G<GOAL>Subsingleton (G ⧸ ⊤)
<VAR>G : Type u<VAR>Group G<VAR>H : Subgroup G<VAR>h : Subsingleton (G ⧸ H)<GOAL>H = ⊤
<VAR>G : Type u<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>h : Subsingleton (G ⧸ H)<GOAL>H = ⊤
<VAR>G : Type u<VAR>Group G<VAR>H₁ : Subgroup G<VAR>H₁.Normal<VAR>H₂ : Subgroup (G ⧸ H₁)<VAR>H₂.Normal<GOAL>Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) = Subgroup.comap (QuotientGroup.mk' (Subgroup.comap (QuotientGroup.mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (QuotientGroup.mk' H₁) H₂))
<VAR>G : Type u<VAR>AddGroup G<VAR>H₁ : AddSubgroup G<VAR>H₁.Normal<VAR>H₂ : AddSubgroup (G ⧸ H₁)<VAR>H₂.Normal<GOAL>AddSubgroup.comap (QuotientAddGroup.mk' H₁) (AddSubgroup.comap (QuotientAddGroup.mk' H₂) (AddSubgroup.center ((G ⧸ H₁) ⧸ H₂))) = AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂)) (AddSubgroup.center (G ⧸ AddSubgroup.comap (QuotientAddGroup.mk' H₁) H₂))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>Set.range ⇑e = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>⇑e.symm '' (⇑e '' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>⇑e '' (⇑e.symm '' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>⇑e '' (⇑e ⁻¹' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>⇑e ⁻¹' (⇑e '' s) = s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>f : α ↪o β<VAR>a : α<GOAL>OrderEmbedding.orderIso a = ⟨f a, ⋯⟩
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>a : α<GOAL>(StrictMono.orderIso f h_mono) a = ⟨f a, ⋯⟩
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>h_surj : Function.Surjective f<GOAL>⇑(StrictMono.orderIsoOfSurjective f h_mono h_surj) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>h_surj : Function.Surjective f<VAR>a : α<GOAL>(StrictMono.orderIsoOfSurjective f h_mono h_surj).symm (f a) = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>h_surj : Function.Surjective f<VAR>b : β<GOAL>f ((StrictMono.orderIsoOfSurjective f h_mono h_surj).symm b) = b
<VAR>α : Type u_2<VAR>BooleanAlgebra α<GOAL>∀ (a : α), (OrderIso.compl α) a = (OrderDual.toDual a)ᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<GOAL>∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.compl α)) a = (OrderDual.ofDual a)ᶜ
<VAR>α : Type u_2<VAR>BooleanAlgebra α<GOAL>StrictAnti compl
<VAR>α : Type u_2<VAR>BooleanAlgebra α<GOAL>Antitone compl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>SemilatticeSup β<VAR>f g : α →o β<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>SemilatticeInf β<VAR>f g : α →o β<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderBot β<GOAL>⊥ = (OrderHom.const α) ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>OrderTop β<GOAL>⊤ = (OrderHom.const α) ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α →o β)<VAR>x : α<GOAL>(sInf s) x = ⨅ f ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ι : Sort u_3<VAR>CompleteLattice β<VAR>f : ι → α →o β<VAR>x : α<GOAL>(⨅ i, f i) x = ⨅ i, (f i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ι : Sort u_3<VAR>CompleteLattice β<VAR>f : ι → α →o β<GOAL>⇑(⨅ i, f i) = ⨅ i, ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>CompleteLattice β<VAR>s : Set (α →o β)<VAR>x : α<GOAL>(sSup s) x = ⨆ f ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ι : Sort u_3<VAR>CompleteLattice β<VAR>f : ι → α →o β<VAR>x : α<GOAL>(⨆ i, f i) x = ⨆ i, (f i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>ι : Sort u_3<VAR>CompleteLattice β<VAR>f : ι → α →o β<GOAL>⇑(⨆ i, f i) = ⨆ i, ⇑(f i)
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>f : α →o α<GOAL>(∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) ↔ ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>a : α<GOAL>a ≤ wellOrderSucc a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < b<GOAL>wellOrderSucc a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < b<GOAL>a < wellOrderSucc a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < wellOrderSucc b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>self : IsWellOrderLimitElement a<VAR>b : α<VAR>hb : b < a<GOAL>∃ c, b < c ∧ c < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>self : IsWellOrderLimitElement a<GOAL>∃ b, b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>OrderBot α<GOAL>a ≠ ⊥
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>OrderBot α<GOAL>⊥ < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>ha : IsWellOrderLimitElement a<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>b : α<VAR>hb : b < a<GOAL>wellOrderSucc b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>OrderBot α<VAR>a : α<GOAL>a = ⊥ ∨ (∃ b, a = wellOrderSucc b ∧ b < a) ∨ IsWellOrderLimitElement a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>IsWellOrder α fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a < wellOrderSucc a<VAR>IsWellOrderLimitElement (wellOrderSucc a)<GOAL>False
<VAR>a : ℕ<GOAL>wellOrderSucc a = a.succ
<VAR>a : ℕ<VAR>IsWellOrderLimitElement a<GOAL>False
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Top α<VAR>Top β<VAR>self : TopHom α β<GOAL>self.toFun ⊤ = ⊤
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Bot α<VAR>Bot β<VAR>self : BotHom α β<GOAL>self.toFun ⊥ = ⊥
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>self : BoundedOrderHom α β<GOAL>self.toFun ⊥ = ⊥
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>self : BoundedOrderHom α β<GOAL>self.toFun ⊤ = ⊤
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Top α<VAR>Top β<VAR>FunLike F α β<VAR>self : TopHomClass F α β<VAR>f : F<GOAL>f ⊤ = ⊤
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Bot α<VAR>Bot β<VAR>FunLike F α β<VAR>self : BotHomClass F α β<VAR>f : F<GOAL>f ⊥ = ⊥
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>LE α<VAR>LE β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>self : BoundedOrderHomClass F α β<VAR>f : F<GOAL>f ⊤ = ⊤
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>LE α<VAR>LE β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>FunLike F α β<VAR>self : BoundedOrderHomClass F α β<VAR>f : F<GOAL>f ⊥ = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EquivLike F α β<VAR>LE α<VAR>OrderTop α<VAR>PartialOrder β<VAR>OrderTop β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<GOAL>f a = ⊤ ↔ a = ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>EquivLike F α β<VAR>LE α<VAR>OrderBot α<VAR>PartialOrder β<VAR>OrderBot β<VAR>OrderIsoClass F α β<VAR>f : F<VAR>a : α<GOAL>f a = ⊥ ↔ a = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>Top β<VAR>f g : TopHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>Top β<VAR>f : TopHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>Top β<VAR>f : TopHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>Top α<GOAL>⇑(TopHom.id α) = id
<VAR>α : Type u_2<VAR>Top α<VAR>a : α<GOAL>(TopHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Top α<VAR>Top β<VAR>Top γ<VAR>f : TopHom β γ<VAR>g : TopHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Top α<VAR>Top β<VAR>Top γ<VAR>f : TopHom β γ<VAR>g : TopHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Top α<VAR>Top β<VAR>Top γ<VAR>Top δ<VAR>f : TopHom γ δ<VAR>g : TopHom β γ<VAR>h : TopHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>Top β<VAR>f : TopHom α β<GOAL>f.comp (TopHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>Top β<VAR>f : TopHom α β<GOAL>(TopHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Top α<VAR>Top β<VAR>Top γ<VAR>g₁ g₂ : TopHom β γ<VAR>f : TopHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Top α<VAR>Top β<VAR>Top γ<VAR>g : TopHom β γ<VAR>f₁ f₂ : TopHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>LE β<VAR>OrderTop β<GOAL>⇑⊤ = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>LE β<VAR>OrderTop β<VAR>a : α<GOAL>⊤ a = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f g : TopHom α β<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f g : TopHom α β<VAR>a : α<GOAL>(f ⊓ g) a = f a ⊓ g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>SemilatticeSup β<VAR>OrderTop β<VAR>f g : TopHom α β<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Top α<VAR>SemilatticeSup β<VAR>OrderTop β<VAR>f g : TopHom α β<VAR>a : α<GOAL>(f ⊔ g) a = f a ⊔ g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>Bot β<VAR>f g : BotHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>Bot β<VAR>f : BotHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>Bot β<VAR>f : BotHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>Bot α<GOAL>⇑(BotHom.id α) = id
<VAR>α : Type u_2<VAR>Bot α<VAR>a : α<GOAL>(BotHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bot α<VAR>Bot β<VAR>Bot γ<VAR>f : BotHom β γ<VAR>g : BotHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bot α<VAR>Bot β<VAR>Bot γ<VAR>f : BotHom β γ<VAR>g : BotHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Bot α<VAR>Bot β<VAR>Bot γ<VAR>Bot δ<VAR>f : BotHom γ δ<VAR>g : BotHom β γ<VAR>h : BotHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>Bot β<VAR>f : BotHom α β<GOAL>f.comp (BotHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>Bot β<VAR>f : BotHom α β<GOAL>(BotHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bot α<VAR>Bot β<VAR>Bot γ<VAR>g₁ g₂ : BotHom β γ<VAR>f : BotHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bot α<VAR>Bot β<VAR>Bot γ<VAR>g : BotHom β γ<VAR>f₁ f₂ : BotHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>LE β<VAR>OrderBot β<GOAL>⇑⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>LE β<VAR>OrderBot β<VAR>a : α<GOAL>⊥ a = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>SemilatticeInf β<VAR>OrderBot β<VAR>f g : BotHom α β<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>SemilatticeInf β<VAR>OrderBot β<VAR>f g : BotHom α β<VAR>a : α<GOAL>(f ⊓ g) a = f a ⊓ g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f g : BotHom α β<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bot α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f g : BotHom α β<VAR>a : α<GOAL>(f ⊔ g) a = f a ⊔ g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f g : BoundedOrderHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedOrderHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedOrderHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<GOAL>⇑(BoundedOrderHom.id α) = id
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<VAR>a : α<GOAL>(BoundedOrderHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedOrderHom β γ<VAR>g : BoundedOrderHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedOrderHom β γ<VAR>g : BoundedOrderHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>f : BoundedOrderHom β γ<VAR>g : BoundedOrderHom α β<GOAL>↑(f.comp g) = (↑f).comp ↑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>BoundedOrder δ<VAR>f : BoundedOrderHom γ δ<VAR>g : BoundedOrderHom β γ<VAR>h : BoundedOrderHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedOrderHom α β<GOAL>f.comp (BoundedOrderHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : BoundedOrderHom α β<GOAL>(BoundedOrderHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>g₁ g₂ : BoundedOrderHom β γ<VAR>f : BoundedOrderHom α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>BoundedOrder γ<VAR>g : BoundedOrderHom β γ<VAR>f₁ f₂ : BoundedOrderHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>OrderTop α<VAR>LE β<VAR>OrderTop β<VAR>f : TopHom α β<VAR>a : α<GOAL>(TopHom.dual f) a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>OrderTop α<VAR>LE β<VAR>OrderTop β<VAR>f : BotHom αᵒᵈ βᵒᵈ<VAR>a : αᵒᵈ<GOAL>(TopHom.dual.symm f) a = f a
<VAR>α : Type u_2<VAR>LE α<VAR>OrderTop α<GOAL>TopHom.dual (TopHom.id α) = BotHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>OrderTop α<VAR>LE β<VAR>OrderTop β<VAR>LE γ<VAR>OrderTop γ<VAR>g : TopHom β γ<VAR>f : TopHom α β<GOAL>TopHom.dual (g.comp f) = (TopHom.dual g).comp (TopHom.dual f)
<VAR>α : Type u_2<VAR>LE α<VAR>OrderTop α<GOAL>TopHom.dual.symm (BotHom.id αᵒᵈ) = TopHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>OrderTop α<VAR>LE β<VAR>OrderTop β<VAR>LE γ<VAR>OrderTop γ<VAR>g : BotHom βᵒᵈ γᵒᵈ<VAR>f : BotHom αᵒᵈ βᵒᵈ<GOAL>TopHom.dual.symm (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>OrderBot α<VAR>LE β<VAR>OrderBot β<VAR>f : BotHom α β<VAR>a : α<GOAL>(BotHom.dual f) a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>OrderBot α<VAR>LE β<VAR>OrderBot β<VAR>f : TopHom αᵒᵈ βᵒᵈ<VAR>a : αᵒᵈ<GOAL>(BotHom.dual.symm f) a = f a
<VAR>α : Type u_2<VAR>LE α<VAR>OrderBot α<GOAL>BotHom.dual (BotHom.id α) = TopHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>OrderBot α<VAR>LE β<VAR>OrderBot β<VAR>LE γ<VAR>OrderBot γ<VAR>g : BotHom β γ<VAR>f : BotHom α β<GOAL>BotHom.dual (g.comp f) = (BotHom.dual g).comp (BotHom.dual f)
<VAR>α : Type u_2<VAR>LE α<VAR>OrderBot α<GOAL>BotHom.dual.symm (TopHom.id αᵒᵈ) = BotHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>OrderBot α<VAR>LE β<VAR>OrderBot β<VAR>LE γ<VAR>OrderBot γ<VAR>g : TopHom βᵒᵈ γᵒᵈ<VAR>f : TopHom αᵒᵈ βᵒᵈ<GOAL>BotHom.dual.symm (g.comp f) = (BotHom.dual.symm g).comp (BotHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>BoundedOrder α<VAR>Preorder β<VAR>BoundedOrder β<VAR>f : BoundedOrderHom α β<GOAL>(BoundedOrderHom.dual f).toOrderHom = OrderHom.dual f.toOrderHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>BoundedOrder α<VAR>Preorder β<VAR>BoundedOrder β<VAR>f : BoundedOrderHom αᵒᵈ βᵒᵈ<GOAL>(BoundedOrderHom.dual.symm f).toOrderHom = OrderHom.dual.symm f.toOrderHom
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<GOAL>BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>BoundedOrder α<VAR>Preorder β<VAR>BoundedOrder β<VAR>Preorder γ<VAR>BoundedOrder γ<VAR>g : BoundedOrderHom β γ<VAR>f : BoundedOrderHom α β<GOAL>BoundedOrderHom.dual (g.comp f) = (BoundedOrderHom.dual g).comp (BoundedOrderHom.dual f)
<VAR>α : Type u_2<VAR>Preorder α<VAR>BoundedOrder α<GOAL>BoundedOrderHom.dual.symm (BoundedOrderHom.id αᵒᵈ) = BoundedOrderHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>BoundedOrder α<VAR>Preorder β<VAR>BoundedOrder β<VAR>Preorder γ<VAR>BoundedOrder γ<VAR>g : BoundedOrderHom βᵒᵈ γᵒᵈ<VAR>f : BoundedOrderHom αᵒᵈ βᵒᵈ<GOAL>BoundedOrderHom.dual.symm (g.comp f) = (BoundedOrderHom.dual.symm g).comp (BoundedOrderHom.dual.symm f)
<VAR>α : Type u_4<VAR>self : CompletePartialOrder α<VAR>d : Set α<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB d (sSup d)
<VAR>α : Type u_2<VAR>CompletePartialOrder α<VAR>d : Set α<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB d (sSup d)
<VAR>α : Type u_2<VAR>CompletePartialOrder α<VAR>d : Set α<VAR>a : α<VAR>hd : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>ha : a ∈ d<GOAL>a ≤ sSup d
<VAR>α : Type u_2<VAR>CompletePartialOrder α<VAR>d : Set α<VAR>a : α<VAR>hd : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>ha : ∀ b ∈ d, b ≤ a<GOAL>sSup d ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompletePartialOrder α<VAR>f : ι → α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>i : ι<GOAL>f i ≤ ⨆ j, f j
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompletePartialOrder α<VAR>f : ι → α<VAR>a : α<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>ha : ∀ (i : ι), f i ≤ a<GOAL>⨆ i, f i ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompletePartialOrder α<VAR>Preorder β<VAR>f : α → β<GOAL>ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB (f '' d) (f (sSup d))
<VAR>α : Type u_1<VAR>a : α<VAR>SemilatticeInf α<VAR>x y : ↑(Set.Iic a)<GOAL>↑(x ⊓ y) = ↑x ⊓ ↑y
<VAR>α : Type u_1<VAR>a : α<VAR>SemilatticeSup α<VAR>x y : ↑(Set.Iic a)<GOAL>↑(x ⊔ y) = ↑x ⊔ ↑y
<VAR>α : Type u_1<VAR>a : α<VAR>Preorder α<GOAL>↑⊤ = a
<VAR>α : Type u_1<VAR>a : α<VAR>Preorder α<VAR>x : ↑(Set.Iic a)<GOAL>x = ⊤ ↔ ↑x = a
<VAR>α : Type u_1<VAR>a : α<VAR>Preorder α<VAR>OrderBot α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>a : α<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>x y : ↑(Set.Iic a)<GOAL>Disjoint x y ↔ Disjoint ↑x ↑y
<VAR>α : Type u_1<VAR>a : α<VAR>SemilatticeSup α<VAR>x y : ↑(Set.Iic a)<GOAL>Codisjoint x y ↔ ↑x ⊔ ↑y = a
<VAR>α : Type u_1<VAR>a : α<VAR>Lattice α<VAR>BoundedOrder α<VAR>x y : ↑(Set.Iic a)<GOAL>IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑⊥ = a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<VAR>a : α<GOAL>↑⊤ = ⊤
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>P : ⦃i : Fin2 n⦄ → α i → Prop<VAR>h : MvFunctor.LiftP P x<VAR>i : Fin2 n<VAR>y : α i<GOAL>y ∈ MvFunctor.supp x i → P y
<VAR>n : ℕ<VAR>F : TypeVec.{u_2} n → Type u_1<VAR>MvFunctor F<VAR>self : LawfulMvFunctor F<VAR>α : TypeVec.{u_2} n<VAR>x : F α<GOAL>TypeVec.id <$$> x = x
<VAR>n : ℕ<VAR>F : TypeVec.{u_2} n → Type u_1<VAR>MvFunctor F<VAR>self : LawfulMvFunctor F<VAR>α β γ : TypeVec.{u_2} n<VAR>g : α ⟹ β<VAR>h : β ⟹ γ<VAR>x : F α<GOAL>(h ⊚ g) <$$> x = h <$$> g <$$> x
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>x : F α<GOAL>TypeVec.id <$$> x = x
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>x : F α<GOAL>(fun _i a => a) <$$> x = x