ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<GOAL>(p.snoc newLast rel).toFun (Fin.last (p.length + 1)) = newLast
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>s : RelSeries r<VAR>a : α<VAR>connect : r s.last a<VAR>i : Fin (s.length + 1)<GOAL>(s.snoc a connect).toFun i.castSucc = s.toFun i
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>newLast : α<VAR>rel : r p.last newLast<VAR>x : α<GOAL>x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>(p.tail len_pos).length = p.length - 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>∀ (a : Fin (p.length - 1 + 1)), (p.tail len_pos).toFun a = (Fin.tail p.toFun ∘ Fin.cast ⋯) a
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>(p.tail len_pos).head = p.toFun 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>len_pos : p.length ≠ 0<GOAL>(p.tail len_pos).last = p.last
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<GOAL>p.eraseLast.length = p.length - 1
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<VAR>i : Fin (p.length - 1 + 1)<GOAL>p.eraseLast.toFun i = p.toFun ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<GOAL>p.eraseLast.head = p.head
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p : RelSeries r<GOAL>p.eraseLast.last = p.toFun ⟨p.length.pred, ⋯⟩
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<GOAL>(p.smash q connect).length = p.length + q.length
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin (p.length + q.length + 1)<GOAL>(p.smash q connect).toFun i = if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin p.length<GOAL>(p.smash q connect).toFun (Fin.castAdd q.length i).castSucc = p.toFun i.castSucc
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin p.length<GOAL>(p.smash q h).toFun (Fin.castAdd q.length i).succ = p.toFun i.succ
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>(p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>(p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>h : p.last = q.head<GOAL>(p.smash q h).head = p.head
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>p q : RelSeries r<VAR>h : p.last = q.head<GOAL>(p.smash q h).last = q.last
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfiniteDimensionalOrder α<VAR>n : ℕ<GOAL>(LTSeries.withLength α n).length = n
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfiniteDimensionalOrder α<GOAL>Nonempty α
<VAR>α : Type u_1<VAR>Preorder α<VAR>FiniteDimensionalOrder α<VAR>x : LTSeries α<GOAL>x.length ≤ (LTSeries.longestOf α).length
<VAR>α : Type u_1<VAR>Preorder α<VAR>FiniteDimensionalOrder α<VAR>p : LTSeries α<VAR>is_longest : ∀ (q : LTSeries α), q.length ≤ p.length<GOAL>p.length = (LTSeries.longestOf α).length
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : LTSeries α<GOAL>StrictMono x.toFun
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : LTSeries α<GOAL>Monotone x.toFun
<VAR>α : Type u_1<VAR>Preorder α<VAR>length : ℕ<VAR>toFun : Fin (length + 1) → α<VAR>strictMono : StrictMono toFun<GOAL>∀ (a : Fin (length + 1)), (LTSeries.mk length toFun strictMono).toFun a = toFun a
<VAR>α : Type u_1<VAR>Preorder α<VAR>length : ℕ<VAR>toFun : Fin (length + 1) → α<VAR>strictMono : StrictMono toFun<GOAL>(LTSeries.mk length toFun strictMono).length = length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>p : LTSeries α<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>∀ (a : Fin (p.length + 1)), (p.map f hf).toFun a = f (p.toFun a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>p : LTSeries α<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>(p.map f hf).length = p.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>p : LTSeries β<VAR>f : α → β<VAR>comap : ∀ ⦃x y : α⦄, f x < f y → x < y<VAR>surjective : Function.Surjective f<VAR>i : Fin (p.length + 1)<GOAL>(p.comap f comap surjective).toFun i = ⋯.choose
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>p : LTSeries β<VAR>f : α → β<VAR>comap : ∀ ⦃x y : α⦄, f x < f y → x < y<VAR>surjective : Function.Surjective f<GOAL>(p.comap f comap surjective).length = p.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>InfiniteDimensionalOrder α<GOAL>InfiniteDimensionalOrder β
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>BoundedOrder α<GOAL>↑(BddOrd.of α).toPartOrd = α
<VAR>X : BddOrd<GOAL>BddOrd.dual.obj X = BddOrd.of (↑X.toPartOrd)ᵒᵈ
<VAR>X Y : BddOrd<VAR>a : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd<GOAL>BddOrd.dual.map a = BoundedOrderHom.dual a
<VAR>α β : BddOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<GOAL>(BddOrd.Iso.mk e).hom = ↑e
<VAR>α β : BddOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<GOAL>(BddOrd.Iso.mk e).inv = ↑e.symm
<GOAL>BddOrd.dualEquiv.functor = BddOrd.dual
<GOAL>BddOrd.dualEquiv.inverse = BddOrd.dual
<GOAL>BddOrd.dual ⋙ CategoryTheory.forget₂ BddOrd PartOrd = CategoryTheory.forget₂ BddOrd PartOrd ⋙ PartOrd.dual
<GOAL>BddOrd.dual ⋙ CategoryTheory.forget₂ BddOrd Bipointed = CategoryTheory.forget₂ BddOrd Bipointed ⋙ Bipointed.swap
<VAR>α : Type u_1<VAR>Order.Frame α<GOAL>↑(Frm.of α) = α
<VAR>α β : Frm<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(Frm.Iso.mk e).hom a = e a
<VAR>α β : Frm<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(Frm.Iso.mk e).inv a = e.symm a
<VAR>X : TopCatᵒᵖ<GOAL>topCatOpToFrm.obj X = Frm.of (TopologicalSpace.Opens ↑(Opposite.unop X))
<GOAL>∀ {X Y : TopCatᵒᵖ} (f : X ⟶ Y), topCatOpToFrm.map f = TopologicalSpace.Opens.comap f.unop
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>↑(HeytAlg.of α) = α
<VAR>X : HeytAlg<GOAL>CategoryTheory.HasForget₂.forget₂.obj X = BddDistLat.of ↑X
<VAR>X Y : HeytAlg<VAR>f : X ⟶ Y<VAR>a : ↑X<GOAL>(CategoryTheory.HasForget₂.forget₂.map f).toSupHom a = f a
<VAR>α β : HeytAlg<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(HeytAlg.Iso.mk e).inv a = e.symm a
<VAR>α β : HeytAlg<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(HeytAlg.Iso.mk e).hom a = e a
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>↑(CompleteLat.of α) = α
<VAR>α β : CompleteLat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(CompleteLat.Iso.mk e).hom.toFun a = e a
<VAR>α β : CompleteLat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(CompleteLat.Iso.mk e).inv.toFun a = e.symm a
<VAR>X : CompleteLat<GOAL>CompleteLat.dual.obj X = CompleteLat.of (↑X)ᵒᵈ
<VAR>X Y : CompleteLat<VAR>a : CompleteLatticeHom ↑X ↑Y<GOAL>CompleteLat.dual.map a = CompleteLatticeHom.dual a
<GOAL>CompleteLat.dualEquiv.inverse = CompleteLat.dual
<GOAL>CompleteLat.dualEquiv.functor = CompleteLat.dual
<GOAL>CompleteLat.dual ⋙ CategoryTheory.forget₂ CompleteLat BddLat = CategoryTheory.forget₂ CompleteLat BddLat ⋙ BddLat.dual
<VAR>α β : FinBddDistLat<VAR>e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat<VAR>a : ↑α.toBddDistLat.toDistLat<GOAL>(FinBddDistLat.Iso.mk e).hom.toSupHom a = e a
<VAR>α β : FinBddDistLat<VAR>e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat<VAR>a : ↑β.toBddDistLat.toDistLat<GOAL>(FinBddDistLat.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>X : FinBddDistLat<GOAL>FinBddDistLat.dual.obj X = FinBddDistLat.of (↑X.toBddDistLat.toDistLat)ᵒᵈ
<VAR>X Y : FinBddDistLat<VAR>a : BoundedLatticeHom ↑X.toBddDistLat.toBddLat.toLat ↑Y.toBddDistLat.toBddLat.toLat<GOAL>FinBddDistLat.dual.map a = BoundedLatticeHom.dual a
<GOAL>FinBddDistLat.dualEquiv.inverse = FinBddDistLat.dual
<GOAL>FinBddDistLat.dualEquiv.functor = FinBddDistLat.dual
<GOAL>FinBddDistLat.dual ⋙ CategoryTheory.forget₂ FinBddDistLat BddDistLat = CategoryTheory.forget₂ FinBddDistLat BddDistLat ⋙ BddDistLat.dual
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>[] ∈ s.subchain
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>l : List α<VAR>a : α<GOAL>a :: l ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>a : α<GOAL>[a] ∈ s.subchain ↔ a ∈ s
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>s.chainHeight = ⨆ l, ↑(↑l).length
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>n : ℕ<VAR>hn : ↑n ≤ s.chainHeight<GOAL>∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>n : ℕ<GOAL>[↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>n : ℕ<GOAL>↑n ≤ s.chainHeight ↔ ∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>l : List α<VAR>hl : l ∈ s.subchain<GOAL>↑l.length ≤ s.chainHeight
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>s.chainHeight = ⊤ ↔ ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>1 ≤ s.chainHeight ↔ s.Nonempty
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>s.chainHeight = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>LT α<GOAL>∅.chainHeight = 0
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>IsEmpty α<GOAL>s.chainHeight = 0
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<VAR>n m : ℕ<GOAL>↑n ≤ s.chainHeight + ↑m ↔ ∃ l ∈ s.subchain, n ≤ l.length + m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>s : Set α<VAR>t : Set β<VAR>n m : ℕ<GOAL>s.chainHeight + ↑n ≤ t.chainHeight + ↑m ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length + n ≤ l'.length + m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>s : Set α<VAR>t : Set β<GOAL>[s.chainHeight ≤ t.chainHeight, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length, ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>s : Set α<VAR>t : Set β<GOAL>s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length = l'.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>s : Set α<VAR>t : Set β<GOAL>s.chainHeight ≤ t.chainHeight ↔ ∀ l ∈ s.subchain, ∃ l' ∈ t.subchain, l.length ≤ l'.length
<VAR>α : Type u_1<VAR>LT α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>s.chainHeight ≤ t.chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LT α<VAR>LT β<VAR>f : α → β<VAR>hf : ∀ {x y : α}, x < y ↔ f x < f y<VAR>s : Set α<GOAL>(f '' s).chainHeight = s.chainHeight
<VAR>α : Type u_1<VAR>LT α<VAR>s : Set α<GOAL>(⇑OrderDual.ofDual ⁻¹' s).chainHeight = s.chainHeight
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<GOAL>s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Ici i).chainHeight
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<GOAL>s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Iic i).chainHeight
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>a : α<VAR>hx : ∀ b ∈ s, a < b<GOAL>(insert a s).chainHeight = s.chainHeight + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>a : α<VAR>ha : ∀ b ∈ s, b < a<GOAL>(insert a s).chainHeight = s.chainHeight + 1
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Preorder α<GOAL>(s ∪ t).chainHeight ≤ s.chainHeight + t.chainHeight
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>H : ∀ a ∈ s, ∀ b ∈ t, a < b<GOAL>(s ∪ t).chainHeight = s.chainHeight + t.chainHeight
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<GOAL>WellFoundedGT ↑s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<GOAL>WellFoundedLT ↑s
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>Fintype α<GOAL>↑(FinBoolAlg.of α).toBoolAlg = α
<VAR>X Y : FinBoolAlg<VAR>f : X ⟶ Y<GOAL>CategoryTheory.HasForget₂.forget₂.map f = let_fun this := ↑(let_fun this := f; this); this
<VAR>X : FinBoolAlg<GOAL>CategoryTheory.HasForget₂.forget₂.obj X = FinPartOrd.of ↑X.toBoolAlg
<VAR>α β : FinBoolAlg<VAR>e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg<VAR>a : ↑α.toBoolAlg<GOAL>(FinBoolAlg.Iso.mk e).hom.toSupHom a = e a
<VAR>α β : FinBoolAlg<VAR>e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg<VAR>a : ↑β.toBoolAlg<GOAL>(FinBoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>X Y : FinBoolAlg<VAR>a : BoundedLatticeHom ↑X.toBoolAlg.toBddDistLat.toBddLat.toLat ↑Y.toBoolAlg.toBddDistLat.toBddLat.toLat<GOAL>FinBoolAlg.dual.map a = BoundedLatticeHom.dual a
<VAR>X : FinBoolAlg<GOAL>FinBoolAlg.dual.obj X = FinBoolAlg.of (↑X.toBoolAlg)ᵒᵈ
<GOAL>FinBoolAlg.dualEquiv.functor = FinBoolAlg.dual
<GOAL>FinBoolAlg.dualEquiv.inverse = FinBoolAlg.dual
<GOAL>FinBoolAlg.dual ⋙ CategoryTheory.forget₂ FinBoolAlg FinBddDistLat = CategoryTheory.forget₂ FinBoolAlg FinBddDistLat ⋙ FinBddDistLat.dual
<VAR>X : FintypeCat<GOAL>fintypeToFinBoolAlgOp.obj X = Opposite.op (FinBoolAlg.of (Set ↑X))
<VAR>X Y : FintypeCat<VAR>f : X ⟶ Y<GOAL>fintypeToFinBoolAlgOp.map f = Quiver.Hom.op (let __src := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
<VAR>α : Type u_1<VAR>Preorder α<GOAL>↑(Preord.of α) = α
<VAR>α β : Preord<VAR>e : ↑α ≃o ↑β<GOAL>(Preord.Iso.mk e).inv = ↑e.symm
<VAR>α β : Preord<VAR>e : ↑α ≃o ↑β<GOAL>(Preord.Iso.mk e).hom = ↑e
<GOAL>∀ {X Y : Preord} (a : ↑X →o ↑Y), Preord.dual.map a = OrderHom.dual a
<VAR>X : Preord<GOAL>Preord.dual.obj X = Preord.of (↑X)ᵒᵈ
<GOAL>Preord.dualEquiv.functor = Preord.dual
<GOAL>∀ {X Y : Preord} (f : X ⟶ Y), preordToCat.map f = ⋯.functor
<VAR>X : Preord<GOAL>preordToCat.obj X = CategoryTheory.Cat.of ↑X
<VAR>α : Type u_1<VAR>BooleanAlgebra α<GOAL>↑(BoolAlg.of α) = α
<VAR>X : BoolAlg<GOAL>↑X.toBddDistLat.toDistLat = ↑X
<VAR>X Y : BoolAlg<VAR>f : BoundedLatticeHom ↑X ↑Y<VAR>a : ↑X<GOAL>(CategoryTheory.HasForget₂.forget₂.map f) a = f a
<VAR>X : BoolAlg<GOAL>↑(CategoryTheory.HasForget₂.forget₂.obj X) = ↑X
<VAR>X : BoolAlg<GOAL>(CategoryTheory.HasForget₂.forget₂.obj X).str = inferInstance
<VAR>α β : BoolAlg<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(BoolAlg.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>α β : BoolAlg<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(BoolAlg.Iso.mk e).hom.toSupHom a = e a
<VAR>X : BoolAlg<GOAL>BoolAlg.dual.obj X = BoolAlg.of (↑X)ᵒᵈ
<VAR>X Y : BoolAlg<VAR>a : BoundedLatticeHom ↑X.toBddDistLat.toBddLat.toLat ↑Y.toBddDistLat.toBddLat.toLat<GOAL>BoolAlg.dual.map a = BoundedLatticeHom.dual a
<GOAL>BoolAlg.dualEquiv.functor = BoolAlg.dual
<GOAL>BoolAlg.dualEquiv.inverse = BoolAlg.dual
<GOAL>BoolAlg.dual ⋙ CategoryTheory.forget₂ BoolAlg BddDistLat = CategoryTheory.forget₂ BoolAlg BddDistLat ⋙ BddDistLat.dual
<VAR>X : Type u<GOAL>typeToBoolAlgOp.obj X = Opposite.op (BoolAlg.of (Set X))
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>typeToBoolAlgOp.map f = Quiver.Hom.op (let __src := { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑(CompleteLatticeHom.setPreimage f), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>↑(PartOrd.of α) = α
<VAR>α β : PartOrd<VAR>e : ↑α ≃o ↑β<GOAL>(PartOrd.Iso.mk e).inv = ↑e.symm
<VAR>α β : PartOrd<VAR>e : ↑α ≃o ↑β<GOAL>(PartOrd.Iso.mk e).hom = ↑e
<VAR>X : PartOrd<GOAL>PartOrd.dual.obj X = PartOrd.of (↑X)ᵒᵈ
<GOAL>∀ {X Y : PartOrd} (a : ↑X →o ↑Y), PartOrd.dual.map a = OrderHom.dual a
<GOAL>PartOrd.dualEquiv.functor = PartOrd.dual
<GOAL>PartOrd.dualEquiv.inverse = PartOrd.dual
<GOAL>PartOrd.dual ⋙ CategoryTheory.forget₂ PartOrd Preord = CategoryTheory.forget₂ PartOrd Preord ⋙ Preord.dual
<VAR>X : Preord<VAR>a : ↑((Preord.dual ⋙ preordToPartOrd).obj X)<GOAL>(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) a = (OrderIso.dualAntisymmetrization ↑X).symm a
<VAR>X : Preord<VAR>a : ↑((preordToPartOrd ⋙ PartOrd.dual).obj X)<GOAL>(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>BoundedOrder α<GOAL>↑(BddDistLat.of α).toDistLat = α
<VAR>X : BddDistLat<GOAL>↑X.toBddLat.toLat = ↑X.toDistLat
<GOAL>CategoryTheory.forget₂ BddDistLat BddLat ⋙ CategoryTheory.forget₂ BddLat Lat = CategoryTheory.forget₂ BddDistLat DistLat ⋙ CategoryTheory.forget₂ DistLat Lat
<VAR>α β : BddDistLat<VAR>e : ↑α.toDistLat ≃o ↑β.toDistLat<VAR>a : ↑β.toDistLat<GOAL>(BddDistLat.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>α β : BddDistLat<VAR>e : ↑α.toDistLat ≃o ↑β.toDistLat<VAR>a : ↑α.toDistLat<GOAL>(BddDistLat.Iso.mk e).hom.toSupHom a = e a
<VAR>X Y : BddDistLat<VAR>a : BoundedLatticeHom ↑X.toBddLat.toLat ↑Y.toBddLat.toLat<GOAL>BddDistLat.dual.map a = BoundedLatticeHom.dual a
<VAR>X : BddDistLat<GOAL>BddDistLat.dual.obj X = BddDistLat.of (↑X.toDistLat)ᵒᵈ
<GOAL>BddDistLat.dualEquiv.inverse = BddDistLat.dual
<GOAL>BddDistLat.dualEquiv.functor = BddDistLat.dual
<GOAL>BddDistLat.dual ⋙ CategoryTheory.forget₂ BddDistLat DistLat = CategoryTheory.forget₂ BddDistLat DistLat ⋙ DistLat.dual
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Fintype α<GOAL>↑(FinPartOrd.of α).toPartOrd = α
<VAR>α β : FinPartOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<GOAL>(FinPartOrd.Iso.mk e).inv = ↑e.symm
<VAR>α β : FinPartOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<GOAL>(FinPartOrd.Iso.mk e).hom = ↑e
<VAR>X : FinPartOrd<GOAL>FinPartOrd.dual.obj X = FinPartOrd.of (↑X.toPartOrd)ᵒᵈ
<VAR>X Y : FinPartOrd<VAR>a : ↑X.toPartOrd →o ↑Y.toPartOrd<GOAL>FinPartOrd.dual.map a = OrderHom.dual a
<GOAL>FinPartOrd.dualEquiv.functor = FinPartOrd.dual
<GOAL>FinPartOrd.dualEquiv.inverse = FinPartOrd.dual
<GOAL>FinPartOrd.dual ⋙ CategoryTheory.forget₂ FinPartOrd PartOrd = CategoryTheory.forget₂ FinPartOrd PartOrd ⋙ PartOrd.dual
<VAR>α : Type u_1<VAR>Lattice α<GOAL>↑(Lat.of α) = α
<VAR>α β : Lat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(Lat.Iso.mk e).hom.toSupHom a = e a
<VAR>α β : Lat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(Lat.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>X : Lat<GOAL>Lat.dual.obj X = Lat.of (↑X)ᵒᵈ
<GOAL>∀ {X Y : Lat} (a : LatticeHom ↑X ↑Y), Lat.dual.map a = LatticeHom.dual a
<GOAL>Lat.dual ⋙ CategoryTheory.forget₂ Lat PartOrd = CategoryTheory.forget₂ Lat PartOrd ⋙ PartOrd.dual
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>↑(LinOrd.of α) = α
<VAR>α β : LinOrd<VAR>e : ↑α ≃o ↑β<GOAL>(LinOrd.Iso.mk e).inv = ↑e.symm
<VAR>α β : LinOrd<VAR>e : ↑α ≃o ↑β<GOAL>(LinOrd.Iso.mk e).hom = ↑e
<GOAL>∀ {X Y : LinOrd} (a : ↑X →o ↑Y), LinOrd.dual.map a = OrderHom.dual a
<VAR>X : LinOrd<GOAL>LinOrd.dual.obj X = LinOrd.of (↑X)ᵒᵈ
<GOAL>LinOrd.dualEquiv.functor = LinOrd.dual
<GOAL>LinOrd.dual ⋙ CategoryTheory.forget₂ LinOrd Lat = CategoryTheory.forget₂ LinOrd Lat ⋙ Lat.dual
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : WellFounded r<GOAL>IsAsymm α r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : WellFounded r<GOAL>IsIrrefl α r
<VAR>α : Type u_1<VAR>r r' : α → α → Prop<VAR>hr : WellFounded r<VAR>h : ∀ (a b : α), r' a b → r a b<GOAL>WellFounded r'
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>r : β → β → Prop<VAR>f : α → β<GOAL>WellFounded r → WellFounded (r on f)
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>H : WellFounded r<VAR>s : Set α<GOAL>s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>H : WellFounded r<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>H.min s h ∈ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>H : WellFounded r<VAR>s : Set α<VAR>h : s.Nonempty<VAR>x : α<VAR>hx : x ∈ s<GOAL>¬r x (H.min s h)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>wf : WellFounded r<VAR>s : Set α<VAR>h : Set.Bounded r s<VAR>x : α<VAR>hx : x ∈ s<GOAL>r x (wf.sup s h)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>wf : WellFounded r<VAR>x : α<VAR>h : ∃ y, r x y<GOAL>r x (wf.succ x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>wo : IsWellOrder α r<VAR>x : α<VAR>h : ∃ y, r x y<VAR>y : α<GOAL>r y (⋯.succ x) ↔ r y x ∨ y = x
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>x : β<VAR>s : Set β<VAR>hx : x ∈ s<VAR>hne : s.Nonempty := ⋯<GOAL>h.min s hne ≤ x
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrder β<VAR>PartialOrder γ<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hfg : Set.range f = Set.range g<VAR>b : β<VAR>H : ∀ a < b, f a = g a<GOAL>f b ≤ g b
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrder β<VAR>PartialOrder γ<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<GOAL>Set.range f = Set.range g ↔ f = g
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>f : β → β<VAR>hf : StrictMono f<VAR>n : β<GOAL>n ≤ f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LT β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>Nonempty α<VAR>a : α<GOAL>¬f a < f (Function.argmin f h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LT β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>Function.argminOn f h s hs ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LT β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>hs : s.Nonempty := ⋯<GOAL>¬f a < f (Function.argminOn f h s hs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LinearOrder β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>a : α<VAR>Nonempty α<GOAL>f (Function.argmin f h) ≤ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LinearOrder β<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>hs : s.Nonempty := ⋯<GOAL>f (Function.argminOn f h s hs) ≤ f a
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>r : α → α → Prop<VAR>a bot : α<VAR>ha : Acc r a<VAR>C : β → Prop<VAR>f : α → β<VAR>ih : ∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)<GOAL>C (f a) → C (f bot)
<VAR>α : Sort u_4<VAR>r : α → α → Prop<VAR>a bot : α<VAR>ha : Acc r a<VAR>C : α → Prop<VAR>ih : ∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c<GOAL>C a → C bot
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<VAR>a bot : α<VAR>C : β → Prop<VAR>f : α → β<VAR>ih : ∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)<GOAL>C (f a) → C (f bot)
<VAR>α : Sort u_4<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<VAR>a bot : α<VAR>C : α → Prop<VAR>ih : ∀ (b : α), b ≠ bot → C b → ∃ c, r c b ∧ C c<GOAL>C a → C bot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>WellFoundedLT β<VAR>hf : StrictMono f<GOAL>WellFoundedLT α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>WellFoundedGT β<VAR>hf : StrictAnti f<GOAL>WellFoundedLT α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>WellFoundedGT β<VAR>hf : StrictMono f<GOAL>WellFoundedGT α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>WellFoundedLT β<VAR>hf : StrictAnti f<GOAL>WellFoundedGT α
<VAR>α : Type u_1<VAR>DistribLattice α<GOAL>↑(DistLat.of α) = α
<VAR>α β : DistLat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑α<GOAL>(DistLat.Iso.mk e).hom.toSupHom a = e a
<VAR>α β : DistLat<VAR>e : ↑α ≃o ↑β<VAR>a : ↑β<GOAL>(DistLat.Iso.mk e).inv.toSupHom a = e.symm a
<GOAL>∀ {X Y : DistLat} (a : LatticeHom ↑X ↑Y), DistLat.dual.map a = LatticeHom.dual a
<VAR>X : DistLat<GOAL>DistLat.dual.obj X = DistLat.of (↑X)ᵒᵈ
<GOAL>DistLat.dualEquiv.functor = DistLat.dual
<GOAL>DistLat.dualEquiv.inverse = DistLat.dual
<GOAL>DistLat.dual ⋙ CategoryTheory.forget₂ DistLat Lat = CategoryTheory.forget₂ DistLat Lat ⋙ Lat.dual
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>{b | a ≤ b} ∈ Filter.atTop
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>Set.Ici a ∈ Filter.atTop
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMaxOrder α<VAR>x : α<GOAL>Set.Ioi x ∈ Filter.atTop
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>{b | b ≤ a} ∈ Filter.atBot
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>Set.Iic a ∈ Filter.atBot
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMinOrder α<VAR>x : α<GOAL>Set.Iio x ∈ Filter.atBot
<VAR>α : Type u_3<VAR>Preorder α<VAR>x : α<GOAL>Disjoint Filter.atBot (𝓟 (Set.Ioi x))
<VAR>α : Type u_3<VAR>Preorder α<VAR>x : α<GOAL>Disjoint Filter.atTop (𝓟 (Set.Iio x))
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMaxOrder α<VAR>x : α<GOAL>Disjoint Filter.atTop (𝓟 (Set.Iic x))
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMinOrder α<VAR>x : α<GOAL>Disjoint Filter.atBot (𝓟 (Set.Ici x))
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMaxOrder α<VAR>x : α<GOAL>Disjoint (pure x) Filter.atTop
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMinOrder α<VAR>x : α<GOAL>Disjoint (pure x) Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>NoMaxOrder α<VAR>x : α<VAR>l : Filter β<VAR>l.NeBot<GOAL>¬Filter.Tendsto (fun x_1 => x) l Filter.atTop