ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α →o β × γ<GOAL>OrderHom.prodIso f = (OrderHom.fst.comp f, OrderHom.snd.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : (α →o β) × (α →o γ)<GOAL>(RelIso.symm OrderHom.prodIso) f = f.1.prod f.2
<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>f : α →o β<VAR>g : γ →o δ<GOAL>∀ (a : α × γ), (f.prodMap g) a = Prod.map (⇑f) (⇑g) a
<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>(i : ι) → Preorder (π i)<VAR>i : ι<GOAL>⇑(Pi.evalOrderHom i) = Function.eval i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<GOAL>⇑OrderHom.coeFnHom = fun f => ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>x : α<GOAL>⇑(OrderHom.apply x) = Function.eval x ∘ fun f => ⇑f
<VAR>α : Type u_2<VAR>Preorder α<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>(i : ι) → Preorder (π i)<VAR>f : (i : ι) → α →o π i<VAR>x : α<VAR>i : ι<GOAL>(OrderHom.pi f) x i = (f i) x
<VAR>α : Type u_2<VAR>Preorder α<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>(i : ι) → Preorder (π i)<VAR>f : α →o (i : ι) → π i<VAR>i : ι<GOAL>OrderHom.piIso f i = (Pi.evalOrderHom i).comp f
<VAR>α : Type u_2<VAR>Preorder α<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>(i : ι) → Preorder (π i)<VAR>f : (i : ι) → α →o π i<GOAL>(RelIso.symm OrderHom.piIso) f = OrderHom.pi f
<VAR>α : Type u_2<VAR>Preorder α<VAR>p : α → Prop<GOAL>⇑(OrderHom.Subtype.val p) = Subtype.val
<VAR>α : Type u_2<VAR>Preorder α<VAR>p q : α → Prop<VAR>h : ∀ (a : α), p a → q a<VAR>x : { x // p x }<GOAL>↑((Subtype.orderEmbedding h) x) = ↑x
<VAR>α : Type u_2<VAR>Preorder α<VAR>Subsingleton α<VAR>g : α →o α<GOAL>g = OrderHom.id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : αᵒᵈ →o βᵒᵈ<GOAL>∀ (a : α), (OrderHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>∀ (a : αᵒᵈ), (OrderHom.dual f) a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u_2<VAR>Preorder α<GOAL>OrderHom.dual OrderHom.id = OrderHom.id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<GOAL>OrderHom.dual (g.comp f) = (OrderHom.dual g).comp (OrderHom.dual f)
<VAR>α : Type u_2<VAR>Preorder α<GOAL>OrderHom.dual.symm OrderHom.id = OrderHom.id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : βᵒᵈ →o γᵒᵈ<VAR>f : αᵒᵈ →o βᵒᵈ<GOAL>OrderHom.dual.symm (g.comp f) = (OrderHom.dual.symm g).comp (OrderHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α →o β<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : (fun x x_1 => x < x_1) ↪r fun x x_1 => x < x_1<VAR>x : α<GOAL>f.orderEmbeddingOfLTEmbedding x = f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<VAR>x : α<GOAL>f.ltEmbedding x = f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<VAR>a b : α<GOAL>f a ≤ f b ↔ a ≤ b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<VAR>a b : α<GOAL>f a < f b ↔ a < b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<VAR>a b : α<GOAL>f a = f b ↔ a = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<GOAL>Monotone ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<GOAL>StrictMono ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<VAR>a : α<GOAL>Acc (fun x x_1 => x < x_1) (f a) → Acc (fun x x_1 => x < x_1) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<GOAL>(WellFounded fun x x_1 => x < x_1) → WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>IsWellOrder β fun x x_1 => x < x_1<VAR>f : α ↪o β<GOAL>IsWellOrder α fun x x_1 => x < x_1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>WellFoundedLT β<VAR>f : α ↪o β<GOAL>WellFoundedLT α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>WellFoundedGT β<VAR>f : α ↪o β<GOAL>WellFoundedGT α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<GOAL>⇑f.withBotMap = WithBot.map ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>f : α ↪o β<GOAL>⇑f.withTopMap = WithTop.map ⇑f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h : ∀ (a b : α), f a ≤ f b ↔ a ≤ b<GOAL>⇑(OrderEmbedding.ofMapLEIff f h) = f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h : StrictMono f<GOAL>⇑(OrderEmbedding.ofStrictMono f h) = f
<VAR>α : Type u_2<VAR>Preorder α<VAR>p : α → Prop<GOAL>⇑(OrderEmbedding.subtype p) = Subtype.val
<VAR>X : Type u_6<VAR>Y : Type u_7<VAR>Preorder X<VAR>Preorder Y<VAR>f : X ↪o Y<GOAL>⇑f.toOrderHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>IsEmpty α<VAR>a : α<GOAL>OrderEmbedding.ofIsEmpty a = isEmptyElim a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>IsEmpty α<GOAL>⇑OrderEmbedding.ofIsEmpty = fun a => isEmptyElim a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α ↪o β<VAR>OrderBot α<VAR>OrderBot β<VAR>a₁ a₂ : α<GOAL>Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α ↪o β<VAR>OrderTop α<VAR>OrderTop β<VAR>a₁ a₂ : α<GOAL>Codisjoint (f a₁) (f a₂) → Codisjoint a₁ a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>f : α ↪o β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>a₁ a₂ : α<GOAL>IsCompl (f a₁) (f a₂) → IsCompl a₁ a₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>f : (fun x x_1 => x < x_1) →r fun x x_1 => x < x_1<GOAL>⇑f.toOrderHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>f : (fun x x_1 => x < x_1) ↪r fun x x_1 => x < x_1<GOAL>Function.Injective ⇑f.toRelHom.toOrderHom
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>f : α ≃o β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>f g : α ≃o β<VAR>h : ⇑f = ⇑g<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>⇑e.toOrderEmbedding = ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>Function.Bijective ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>Function.Injective ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>Function.Surjective ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x y : α<GOAL>e x = e y ↔ x = y
<VAR>α : Type u_2<VAR>LE α<GOAL>⇑(OrderIso.refl α) = id
<VAR>α : Type u_2<VAR>LE α<VAR>x : α<GOAL>(OrderIso.refl α) x = x
<VAR>α : Type u_2<VAR>LE α<GOAL>(OrderIso.refl α).toEquiv = Equiv.refl α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : β<GOAL>e (e.symm x) = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : α<GOAL>e.symm (e x) = x
<VAR>α : Type u_6<VAR>LE α<GOAL>(OrderIso.refl α).symm = OrderIso.refl α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : α<VAR>y : β<GOAL>e x = y ↔ x = e.symm y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : α<VAR>y : β<GOAL>e.symm y = x ↔ y = e x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>e.symm.symm = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<GOAL>Function.Bijective OrderIso.symm
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<GOAL>Function.Injective OrderIso.symm
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>e.symm = e.symm.toEquiv
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>e : α ≃o β<VAR>e' : β ≃o γ<GOAL>⇑(e.trans e') = ⇑e' ∘ ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>e : α ≃o β<VAR>e' : β ≃o γ<VAR>x : α<GOAL>(e.trans e') x = e' (e x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>(OrderIso.refl α).trans e = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>e.trans (OrderIso.refl β) = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>e₁ : α ≃o β<VAR>e₂ : β ≃o γ<VAR>c : γ<GOAL>(e₁.trans e₂).symm c = e₁.symm (e₂.symm c)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>LE α<VAR>LE β<VAR>LE γ<VAR>e₁ : α ≃o β<VAR>e₂ : β ≃o γ<GOAL>(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>e.trans e.symm = OrderIso.refl α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<GOAL>e.symm.trans e = OrderIso.refl β
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>δ : Type u_9<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p : γ →o δ<GOAL>(RelIso.symm (f.arrowCongr g)) p = (↑g.symm).comp (p.comp ↑f)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>δ : Type u_9<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>Preorder δ<VAR>f : α ≃o γ<VAR>g : β ≃o δ<VAR>p : α →o β<GOAL>(f.arrowCongr g) p = (↑g).comp (p.comp ↑f.symm)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>a : α →o α<GOAL>f.conj a = (↑f).comp (a.comp ↑f.symm)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<GOAL>∀ (a : β →o β), f.conj.symm a = EquivLike.inv (f.arrowCongr f) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<GOAL>⇑OrderIso.prodComm = Prod.swap
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<GOAL>OrderIso.prodComm.symm = OrderIso.prodComm
<VAR>α : Type u_2<VAR>LE α<GOAL>⇑(OrderIso.dualDual α) = ⇑OrderDual.toDual ∘ ⇑OrderDual.toDual
<VAR>α : Type u_2<VAR>LE α<GOAL>⇑(OrderIso.dualDual α).symm = ⇑OrderDual.ofDual ∘ ⇑OrderDual.ofDual
<VAR>α : Type u_2<VAR>LE α<VAR>a : α<GOAL>(OrderIso.dualDual α) a = OrderDual.toDual (OrderDual.toDual a)
<VAR>α : Type u_2<VAR>LE α<VAR>a : αᵒᵈᵒᵈ<GOAL>(OrderIso.dualDual α).symm a = OrderDual.ofDual (OrderDual.ofDual a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x y : α<GOAL>e x ≤ e y ↔ x ≤ y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : α<VAR>y : β<GOAL>x ≤ e.symm y ↔ e x ≤ y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>LE β<VAR>e : α ≃o β<VAR>x : α<VAR>y : β<GOAL>e.symm y ≤ x ↔ y ≤ e x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Monotone ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>StrictMono ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>x y : α<GOAL>e x < e y ↔ x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>x : α<GOAL>e.toRelIsoLT x = e x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>e.toRelIsoLT.symm = e.symm.toRelIsoLT
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1<VAR>x : α<GOAL>(OrderIso.ofRelIsoLT e) x = e x
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1<GOAL>(OrderIso.ofRelIsoLT e).symm = OrderIso.ofRelIsoLT e.symm
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : α ≃o β<GOAL>OrderIso.ofRelIsoLT e.toRelIsoLT = e
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : (fun x x_1 => x < x_1) ≃r fun x x_1 => x < x_1<GOAL>(OrderIso.ofRelIsoLT e).toRelIsoLT = e
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Unique α<VAR>Preorder β<GOAL>(OrderIso.funUnique α β).toEquiv = Equiv.funUnique α β
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Unique α<VAR>Preorder β<VAR>f : (i : α) → (fun a => β) i<GOAL>(OrderIso.funUnique α β) f = f default
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Unique α<VAR>Preorder β<GOAL>⇑(OrderIso.funUnique α β).symm = Function.const α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃ β<VAR>h₁ : Monotone ⇑e<VAR>h₂ : Monotone ⇑e.symm<GOAL>⇑(e.toOrderIso h₁ h₂) = ⇑e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃ β<VAR>h₁ : Monotone ⇑e<VAR>h₂ : Monotone ⇑e.symm<GOAL>(e.toOrderIso h₁ h₂).toEquiv = e
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>g : β → α<VAR>hg : Function.RightInverse g f<GOAL>⇑(StrictMono.orderIsoOfRightInverse f h_mono g hg) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>h_mono : StrictMono f<VAR>g : β → α<VAR>hg : Function.RightInverse g f<GOAL>⇑(RelIso.symm (StrictMono.orderIsoOfRightInverse f h_mono g hg)) = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>PartialOrder β<VAR>f : α ≃o β<VAR>x : α<VAR>y : β<VAR>hx : ∀ (x' : α), x ≤ x'<VAR>hy : ∀ (y' : β), y ≤ y'<GOAL>f x = y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>PartialOrder β<VAR>OrderBot α<VAR>OrderBot β<VAR>f : α ≃o β<GOAL>f ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>PartialOrder β<VAR>f : α ≃o β<VAR>x : α<VAR>y : β<VAR>hx : ∀ (x' : α), x' ≤ x<VAR>hy : ∀ (y' : β), y' ≤ y<GOAL>f x = y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LE α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>f : α ≃o β<GOAL>f ⊤ = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α ↪o β<VAR>x y : α<GOAL>f (x ⊓ y) ≤ f x ⊓ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α ↪o β<VAR>x y : α<GOAL>f x ⊔ f y ≤ f (x ⊔ y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>f : α ≃o β<VAR>x y : α<GOAL>f (x ⊓ y) = f x ⊓ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>f : α ≃o β<VAR>x y : α<GOAL>f (x ⊔ y) = f x ⊔ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>SemilatticeInf β<VAR>OrderBot β<VAR>a b : α<VAR>f : α ≃o β<VAR>ha : Disjoint a b<GOAL>Disjoint (f a) (f b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>SemilatticeSup β<VAR>OrderTop β<VAR>a b : α<VAR>f : α ≃o β<VAR>ha : Codisjoint a b<GOAL>Codisjoint (f a) (f b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>OrderBot α<VAR>SemilatticeInf β<VAR>OrderBot β<VAR>a b : α<VAR>f : α ≃o β<GOAL>Disjoint (f a) (f b) ↔ Disjoint a b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>OrderTop α<VAR>SemilatticeSup β<VAR>OrderTop β<VAR>a b : α<VAR>f : α ≃o β<GOAL>Codisjoint (f a) (f b) ↔ Codisjoint a b
<VAR>α : Type u_2<VAR>LE α<VAR>a : α<GOAL>WithBot.toDualTopEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a
<VAR>α : Type u_2<VAR>LE α<VAR>a : α<GOAL>WithBot.toDualTopEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)
<VAR>α : Type u_2<VAR>LE α<GOAL>WithBot.toDualTopEquiv ⊥ = ⊥
<VAR>α : Type u_2<VAR>LE α<GOAL>WithBot.toDualTopEquiv.symm ⊥ = ⊥
<VAR>α : Type u_2<VAR>LE α<GOAL>⇑WithBot.toDualTopEquiv = ⇑OrderDual.toDual ∘ ⇑WithBot.ofDual
<VAR>α : Type u_2<VAR>LE α<VAR>a : α<GOAL>WithTop.toDualBotEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a
<VAR>α : Type u_2<VAR>LE α<VAR>a : α<GOAL>WithTop.toDualBotEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)
<VAR>α : Type u_2<VAR>LE α<GOAL>WithTop.toDualBotEquiv ⊤ = ⊤
<VAR>α : Type u_2<VAR>LE α<GOAL>WithTop.toDualBotEquiv.symm ⊤ = ⊤
<VAR>α : Type u_2<VAR>LE α<GOAL>⇑WithTop.toDualBotEquiv = ⇑OrderDual.toDual ∘ ⇑WithTop.ofDual
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : α ≃o β<GOAL>∀ (a : Option α), e.withTopCongr a = Option.map (⇑e) a
<VAR>α : Type u_2<VAR>PartialOrder α<GOAL>(OrderIso.refl α).withTopCongr = OrderIso.refl (WithTop α)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : α ≃o β<GOAL>e.withTopCongr.symm = e.symm.withTopCongr
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>PartialOrder γ<VAR>e₁ : α ≃o β<VAR>e₂ : β ≃o γ<GOAL>e₁.withTopCongr.trans e₂.withTopCongr = (e₁.trans e₂).withTopCongr
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : α ≃o β<GOAL>∀ (a : Option α), e.withBotCongr a = Option.map (⇑e) a
<VAR>α : Type u_2<VAR>PartialOrder α<GOAL>(OrderIso.refl α).withBotCongr = OrderIso.refl (WithBot α)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>PartialOrder β<VAR>e : α ≃o β<GOAL>e.withBotCongr.symm = e.symm.withBotCongr
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>PartialOrder γ<VAR>e₁ : α ≃o β<VAR>e₂ : β ≃o γ<GOAL>e₁.withBotCongr.trans e₂.withBotCongr = (e₁.trans e₂).withBotCongr
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : α ≃o β<VAR>x y : α<VAR>h : IsCompl x y<GOAL>IsCompl (f x) (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : α ≃o β<VAR>x y : α<GOAL>IsCompl x y ↔ IsCompl (f x) (f y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>ComplementedLattice α<VAR>f : α ≃o β<GOAL>ComplementedLattice β
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder α<VAR>BoundedOrder β<VAR>f : α ≃o β<GOAL>ComplementedLattice α ↔ ComplementedLattice β
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>u : Set γ<GOAL>u ∈ Filter.map₂ m f g ↔ ∃ s ∈ f, ∃ t ∈ g, Set.image2 m s t ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>Set.image2 m s t ∈ Filter.map₂ m f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map (fun p => m p.1 p.2) (f ×ˢ g) = Filter.map₂ m f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α × β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map m (f ×ˢ g) = Filter.map₂ (fun a b => m (a, b)) f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ Prod.mk f g = f ×ˢ g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ g₂<GOAL>Filter.map₂ m f₁ g₁ ≤ Filter.map₂ m f₂ g₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<VAR>h : g₁ ≤ g₂<GOAL>Filter.map₂ m f g₁ ≤ Filter.map₂ m f g₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<VAR>h : f₁ ≤ f₂<GOAL>Filter.map₂ m f₁ g ≤ Filter.map₂ m f₂ g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<GOAL>h ≤ Filter.map₂ m f g ↔ ∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → Set.image2 m s t ∈ h
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>g : Filter β<GOAL>Filter.map₂ m ⊥ g = ⊥
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<GOAL>Filter.map₂ m f ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>(Filter.map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : f.NeBot<VAR>hg : g.NeBot<GOAL>(Filter.map₂ m f g).NeBot
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>h : (Filter.map₂ m f g).NeBot<GOAL>f.NeBot
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>h : (Filter.map₂ m f g).NeBot<GOAL>g.NeBot
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ m (f₁ ⊔ f₂) g = Filter.map₂ m f₁ g ⊔ Filter.map₂ m f₂ g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>Filter.map₂ m f (g₁ ⊔ g₂) = Filter.map₂ m f g₁ ⊔ Filter.map₂ m f g₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f₁ f₂ : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ m (f₁ ⊓ f₂) g ≤ Filter.map₂ m f₁ g ⊓ Filter.map₂ m f₂ g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g₁ g₂ : Filter β<GOAL>Filter.map₂ m f (g₁ ⊓ g₂) ≤ Filter.map₂ m f g₁ ⊓ Filter.map₂ m f g₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>g : Filter β<VAR>a : α<GOAL>Filter.map₂ m (pure a) g = Filter.map (m a) g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>b : β<GOAL>Filter.map₂ m f (pure b) = Filter.map (fun x => m x b) f
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>a : α<VAR>b : β<GOAL>Filter.map₂ m (pure a) (pure b) = pure (m a b)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ m f g = Filter.map₂ (fun a b => m b a) g f
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>g.NeBot<GOAL>Filter.map₂ (fun x x_1 => x) f g = f
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : Filter α<VAR>g : Filter β<VAR>f.NeBot<GOAL>Filter.map₂ (fun x y => y) f g = g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β → γ<VAR>n : γ → δ<GOAL>Filter.map n (Filter.map₂ m f g) = Filter.map₂ (fun a b => n (m a b)) f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : γ → β → δ<VAR>n : α → γ<GOAL>Filter.map₂ m (Filter.map n f) g = Filter.map₂ (fun a b => m (n a) b) f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → γ → δ<VAR>n : β → γ<GOAL>Filter.map₂ m f (Filter.map n g) = Filter.map₂ (fun a b => m a (n b)) f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α × β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map₂ (Function.curry m) f g = Filter.map m (f ×ˢ g)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<GOAL>Filter.map (Function.uncurry m) (f ×ˢ g) = Filter.map₂ m f g
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>f : Filter α<VAR>g : Filter β<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → ε' → ε<VAR>n' : β → γ → ε'<VAR>h : Filter γ<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)<GOAL>Filter.map₂ m (Filter.map₂ n f g) h = Filter.map₂ m' f (Filter.map₂ n' g h)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>m : α → β → γ<VAR>f : Filter α<VAR>g : Filter β<VAR>n : β → α → γ<VAR>h_comm : ∀ (a : α) (b : β), m a b = n b a<GOAL>Filter.map₂ m f g = Filter.map₂ n g f
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : α → δ → ε<VAR>n : β → γ → δ<VAR>m' : α → γ → δ'<VAR>n' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' b (m' a c)<GOAL>Filter.map₂ m f (Filter.map₂ n g h) = Filter.map₂ n' g (Filter.map₂ m' f h)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>f : Filter α<VAR>g : Filter β<VAR>h : Filter γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m' : α → γ → δ'<VAR>n' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b<GOAL>Filter.map₂ m (Filter.map₂ n f g) h = Filter.map₂ n' (Filter.map₂ m' f h) g