ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord • HNNExtension.NormalWord.empty = w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<GOAL>Function.Injective fun w => HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<GOAL>Function.Injective ⇑HNNExtension.of
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w : HNNExtension.NormalWord.ReducedWord G A B<GOAL>∃ w', HNNExtension.NormalWord.ReducedWord.prod φ w'.toReducedWord = HNNExtension.NormalWord.ReducedWord.prod φ w ∧ List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧ ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ HNNExtension.toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>w₁ w₂ : HNNExtension.NormalWord.ReducedWord G A B<VAR>hprod : HNNExtension.NormalWord.ReducedWord.prod φ w₁ = HNNExtension.NormalWord.ReducedWord.prod φ w₂<GOAL>List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ HNNExtension.toSubgroup A B (-u)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>w : HNNExtension.NormalWord.ReducedWord G A B<VAR>hw : HNNExtension.NormalWord.ReducedWord.prod φ w ∈ HNNExtension.of.range<GOAL>w.toList = []
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>One M<VAR>s t : Set α<VAR>f g : α → M<VAR>l : Filter α<VAR>hf : f =ᶠ[l ⊓ 𝓟 s] g<VAR>hs : s =ᶠ[l] t<GOAL>s.mulIndicator f =ᶠ[l] t.mulIndicator g
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Zero M<VAR>s t : Set α<VAR>f g : α → M<VAR>l : Filter α<VAR>hf : f =ᶠ[l ⊓ 𝓟 s] g<VAR>hs : s =ᶠ[l] t<GOAL>s.indicator f =ᶠ[l] t.indicator g
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>Monoid M<VAR>s t : Set α<VAR>f : α → M<VAR>l : Filter α<VAR>h : ∀ᶠ (a : α) in l, a ∉ s ∩ t<GOAL>(s ∪ t).mulIndicator f =ᶠ[l] s.mulIndicator f * t.mulIndicator f
<VAR>α : Type u_1<VAR>M : Type u_3<VAR>AddMonoid M<VAR>s t : Set α<VAR>f : α → M<VAR>l : Filter α<VAR>h : ∀ᶠ (a : α) in l, a ∉ s ∩ t<GOAL>(s ∪ t).indicator f =ᶠ[l] s.indicator f + t.indicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f ≤ᶠ[l ⊓ 𝓟 s] g<GOAL>s.mulIndicator f ≤ᶠ[l] s.mulIndicator g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f ≤ᶠ[l ⊓ 𝓟 s] g<GOAL>s.indicator f ≤ᶠ[l] s.indicator g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>Zero β<VAR>s : ι → Set α<VAR>hs : Monotone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).indicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).indicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>One β<VAR>s : ι → Set α<VAR>hs : Monotone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>Zero β<VAR>s : ι → Set α<VAR>hs : Monotone s<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun i => (s i).indicator f a) Filter.atTop (pure ((⋃ i, s i).indicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>One β<VAR>s : ι → Set α<VAR>hs : Monotone s<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun i => (s i).mulIndicator f a) Filter.atTop (pure ((⋃ i, s i).mulIndicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>One β<VAR>s : ι → Set α<VAR>hs : Antitone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (⋂ i, s i).mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>Zero β<VAR>s : ι → Set α<VAR>hs : Antitone s<VAR>f : α → β<VAR>a : α<GOAL>(fun i => (s i).indicator f a) =ᶠ[Filter.atTop] fun x => (⋂ i, s i).indicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>One β<VAR>s : ι → Set α<VAR>hs : Antitone s<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun i => (s i).mulIndicator f a) Filter.atTop (pure ((⋂ i, s i).mulIndicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Preorder ι<VAR>Zero β<VAR>s : ι → Set α<VAR>hs : Antitone s<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun i => (s i).indicator f a) Filter.atTop (pure ((⋂ i, s i).indicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>One β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>(fun n => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (Set.iUnion s).mulIndicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Zero β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>(fun n => (⋃ i ∈ n, s i).indicator f a) =ᶠ[Filter.atTop] fun x => (Set.iUnion s).indicator f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>One β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun n => (⋃ i ∈ n, s i).mulIndicator f a) Filter.atTop (pure ((Set.iUnion s).mulIndicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_5<VAR>Zero β<VAR>s : ι → Set α<VAR>f : α → β<VAR>a : α<GOAL>Filter.Tendsto (fun n => (⋃ i ∈ n, s i).indicator f a) Filter.atTop (pure ((Set.iUnion s).indicator f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>Function.support f =ᶠ[l] Function.support g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>Function.mulSupport f =ᶠ[l] Function.mulSupport g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>l : Filter α<VAR>f g : α → β<VAR>s : Set α<VAR>hfg : f =ᶠ[l] g<GOAL>s.mulIndicator f =ᶠ[l] s.mulIndicator g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>l : Filter α<VAR>f g : α → β<VAR>s : Set α<VAR>hfg : f =ᶠ[l] g<GOAL>s.indicator f =ᶠ[l] s.indicator g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>l : Filter α<VAR>f : α → β<VAR>s : Set α<VAR>hf : f =ᶠ[l] 0<GOAL>s.indicator f =ᶠ[l] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>l : Filter α<VAR>f : α → β<VAR>s : Set α<VAR>hf : f =ᶠ[l] 1<GOAL>s.mulIndicator f =ᶠ[l] 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : ∀ᶠ (x : α) in l, f x ≠ 1<VAR>s t : Set α<VAR>h : s.mulIndicator f =ᶠ[l] t.mulIndicator f<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : ∀ᶠ (x : α) in l, f x ≠ 0<VAR>s t : Set α<VAR>h : s.indicator f =ᶠ[l] t.indicator f<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>l : Filter α<VAR>c : β<VAR>hc : c ≠ 0<VAR>s t : Set α<VAR>h : (s.indicator fun x => c) =ᶠ[l] t.indicator fun x => c<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>l : Filter α<VAR>c : β<VAR>hc : c ≠ 1<VAR>s t : Set α<VAR>h : (s.mulIndicator fun x => c) =ᶠ[l] t.mulIndicator fun x => c<GOAL>s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<VAR>l : Filter α<VAR>c : β<VAR>hc : c ≠ 1<VAR>s t : Set α<GOAL>((s.mulIndicator fun x => c) =ᶠ[l] t.mulIndicator fun x => c) ↔ s =ᶠ[l] t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>l : Filter α<VAR>c : β<VAR>hc : c ≠ 0<VAR>s t : Set α<GOAL>((s.indicator fun x => c) =ᶠ[l] t.indicator fun x => c) ↔ s =ᶠ[l] t
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>SupSet α<VAR>SupSet β<VAR>self : sSupHom α β<VAR>s : Set α<GOAL>self.toFun (sSup s) = sSup (self.toFun '' s)
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>InfSet α<VAR>InfSet β<VAR>self : sInfHom α β<VAR>s : Set α<GOAL>self.toFun (sInf s) = sInf (self.toFun '' s)
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>self : FrameHom α β<VAR>s : Set α<GOAL>self.toFun (sSup s) = sSup (self.toFun '' s)
<VAR>α : Type u_8<VAR>β : Type u_9<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>self : CompleteLatticeHom α β<VAR>s : Set α<GOAL>self.toFun (sSup s) = sSup (self.toFun '' s)
<VAR>F : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>SupSet α<VAR>SupSet β<VAR>FunLike F α β<VAR>self : sSupHomClass F α β<VAR>f : F<VAR>s : Set α<GOAL>f (sSup s) = sSup (⇑f '' s)
<VAR>F : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>InfSet α<VAR>InfSet β<VAR>FunLike F α β<VAR>self : sInfHomClass F α β<VAR>f : F<VAR>s : Set α<GOAL>f (sInf s) = sInf (⇑f '' s)
<VAR>F : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>FunLike F α β<VAR>self : FrameHomClass F α β<VAR>f : F<VAR>s : Set α<GOAL>f (sSup s) = sSup (⇑f '' s)
<VAR>F : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>FunLike F α β<VAR>self : CompleteLatticeHomClass F α β<VAR>f : F<VAR>s : Set α<GOAL>f (sSup s) = sSup (⇑f '' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_6<VAR>FunLike F α β<VAR>SupSet α<VAR>SupSet β<VAR>sSupHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>FunLike F α β<VAR>SupSet α<VAR>SupSet β<VAR>sSupHomClass F α β<VAR>f : F<VAR>g : (i : ι) → κ i → α<GOAL>f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_6<VAR>FunLike F α β<VAR>InfSet α<VAR>InfSet β<VAR>sInfHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>FunLike F α β<VAR>InfSet α<VAR>InfSet β<VAR>sInfHomClass F α β<VAR>f : F<VAR>g : (i : ι) → κ i → α<GOAL>f (⨅ i, ⨅ j, g i j) = ⨅ i, ⨅ j, f (g i j)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>a : α<GOAL>f.toCompleteLatticeHom.toFun a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : α → β<VAR>hf : ∀ (s : Set α), f (sSup s) = sSup (f '' s)<GOAL>⇑{ toFun := f, map_sSup' := hf } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f g : sSupHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>SupSet α<GOAL>⇑(sSupHom.id α) = id
<VAR>α : Type u_2<VAR>SupSet α<VAR>a : α<GOAL>(sSupHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>f : sSupHom β γ<VAR>g : sSupHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>f : sSupHom β γ<VAR>g : sSupHom α β<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>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>SupSet δ<VAR>f : sSupHom γ δ<VAR>g : sSupHom β γ<VAR>h : sSupHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<GOAL>f.comp (sSupHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<GOAL>(sSupHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>g₁ g₂ : sSupHom β γ<VAR>f : sSupHom α β<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>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>g : sSupHom β γ<VAR>f₁ f₂ : sSupHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<GOAL>∀ {x : CompleteLattice β}, ⇑⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<GOAL>∀ {x : CompleteLattice β} (a : α), ⊥ a = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : α → β<VAR>hf : ∀ (s : Set α), f (sInf s) = sInf (f '' s)<GOAL>⇑{ toFun := f, map_sInf' := hf } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f g : sInfHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>InfSet α<GOAL>⇑(sInfHom.id α) = id
<VAR>α : Type u_2<VAR>InfSet α<VAR>a : α<GOAL>(sInfHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>f : sInfHom β γ<VAR>g : sInfHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>f : sInfHom β γ<VAR>g : sInfHom α β<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>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>InfSet δ<VAR>f : sInfHom γ δ<VAR>g : sInfHom β γ<VAR>h : sInfHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<GOAL>f.comp (sInfHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<GOAL>(sInfHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>g₁ g₂ : sInfHom β γ<VAR>f : sInfHom α β<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>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>g : sInfHom β γ<VAR>f₁ f₂ : sInfHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>CompleteLattice β<GOAL>⇑⊤ = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>CompleteLattice β<VAR>a : α<GOAL>⊤ a = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<GOAL>⇑f.toInfTopHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<GOAL>⇑f.toLatticeHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : InfTopHom α β<VAR>hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)<GOAL>⇑{ toInfTopHom := f, map_sSup' := hf } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f g : FrameHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>⇑(FrameHom.id α) = id
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<GOAL>(FrameHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>f : FrameHom β γ<VAR>g : FrameHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>f : FrameHom β γ<VAR>g : FrameHom α β<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>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>CompleteLattice δ<VAR>f : FrameHom γ δ<VAR>g : FrameHom β γ<VAR>h : FrameHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<GOAL>f.comp (FrameHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : FrameHom α β<GOAL>(FrameHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g₁ g₂ : FrameHom β γ<VAR>f : FrameHom α β<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>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g : FrameHom β γ<VAR>f₁ f₂ : FrameHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>⇑f.tosInfHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>⇑f.tosSupHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>⇑f.toBoundedLatticeHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : sInfHom α β<VAR>hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)<GOAL>⇑{ tosInfHom := f, map_sSup' := hf } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f g : CompleteLatticeHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>⇑(CompleteLatticeHom.id α) = id
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<GOAL>(CompleteLatticeHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>f : CompleteLatticeHom β γ<VAR>g : CompleteLatticeHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>f : CompleteLatticeHom β γ<VAR>g : CompleteLatticeHom α β<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>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>CompleteLattice δ<VAR>f : CompleteLatticeHom γ δ<VAR>g : CompleteLatticeHom β γ<VAR>h : CompleteLatticeHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>f.comp (CompleteLatticeHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>(CompleteLatticeHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g₁ g₂ : CompleteLatticeHom β γ<VAR>f : CompleteLatticeHom α β<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>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g : CompleteLatticeHom β γ<VAR>f₁ f₂ : CompleteLatticeHom α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sInfHom αᵒᵈ βᵒᵈ<GOAL>∀ (a : α), (sSupHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SupSet α<VAR>SupSet β<VAR>f : sSupHom α β<GOAL>∀ (a : αᵒᵈ), (sSupHom.dual f).toFun a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u_2<VAR>SupSet α<GOAL>sSupHom.dual (sSupHom.id α) = sInfHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>g : sSupHom β γ<VAR>f : sSupHom α β<GOAL>sSupHom.dual (g.comp f) = (sSupHom.dual g).comp (sSupHom.dual f)
<VAR>α : Type u_2<VAR>SupSet α<GOAL>sSupHom.dual.symm (sInfHom.id αᵒᵈ) = sSupHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>SupSet α<VAR>SupSet β<VAR>SupSet γ<VAR>g : sInfHom βᵒᵈ γᵒᵈ<VAR>f : sInfHom αᵒᵈ βᵒᵈ<GOAL>sSupHom.dual.symm (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sInfHom α β<GOAL>∀ (a : αᵒᵈ), (sInfHom.dual f) a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>InfSet α<VAR>InfSet β<VAR>f : sSupHom αᵒᵈ βᵒᵈ<GOAL>∀ (a : α), (sInfHom.dual.symm f).toFun a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
<VAR>α : Type u_2<VAR>InfSet α<GOAL>sInfHom.dual (sInfHom.id α) = sSupHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>g : sInfHom β γ<VAR>f : sInfHom α β<GOAL>sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f)
<VAR>α : Type u_2<VAR>InfSet α<GOAL>sInfHom.dual.symm (sSupHom.id αᵒᵈ) = sInfHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>InfSet α<VAR>InfSet β<VAR>InfSet γ<VAR>g : sSupHom βᵒᵈ γᵒᵈ<VAR>f : sSupHom αᵒᵈ βᵒᵈ<GOAL>sInfHom.dual.symm (g.comp f) = (sInfHom.dual.symm g).comp (sInfHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom αᵒᵈ βᵒᵈ<GOAL>∀ (a : αᵒᵈᵒᵈ), (CompleteLatticeHom.dual.symm f).toFun a = OrderDual.toDual (f (OrderDual.ofDual a))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>∀ (a : αᵒᵈ), (CompleteLatticeHom.dual f).toFun a = OrderDual.toDual (f (OrderDual.ofDual a))
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id αᵒᵈ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g : CompleteLatticeHom β γ<VAR>f : CompleteLatticeHom α β<GOAL>CompleteLatticeHom.dual (g.comp f) = (CompleteLatticeHom.dual g).comp (CompleteLatticeHom.dual f)
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>CompleteLatticeHom.dual.symm (CompleteLatticeHom.id αᵒᵈ) = CompleteLatticeHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>CompleteLattice γ<VAR>g : CompleteLatticeHom βᵒᵈ γᵒᵈ<VAR>f : CompleteLatticeHom αᵒᵈ βᵒᵈ<GOAL>CompleteLatticeHom.dual.symm (g.comp f) = (CompleteLatticeHom.dual.symm g).comp (CompleteLatticeHom.dual.symm f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<GOAL>⇑(CompleteLatticeHom.setPreimage f) = Set.preimage f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>s : Set β<GOAL>(CompleteLatticeHom.setPreimage f) s = f ⁻¹' s
<VAR>α : Type u_2<GOAL>CompleteLatticeHom.setPreimage id = CompleteLatticeHom.id (Set α)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>g : β → γ<VAR>f : α → β<GOAL>CompleteLatticeHom.setPreimage (g ∘ f) = (CompleteLatticeHom.setPreimage f).comp (CompleteLatticeHom.setPreimage g)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>s : Set (Set α)<GOAL>f '' sSup s = sSup (Set.image f '' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>s : Set α<GOAL>(sSupHom.setImage f) s = f '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>e : α ≃ β<VAR>s : Set α<GOAL>e.toOrderIsoSet s = ⇑e '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>e : α ≃ β<VAR>s : Set β<GOAL>(RelIso.symm e.toOrderIsoSet) s = ⇑e.symm '' s
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>x : α × α<GOAL>supsSupHom x = x.1 ⊔ x.2
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>x : α × α<GOAL>infsInfHom x = x.1 ⊓ x.2
<VAR>α : Type u<VAR>Preorder α<VAR>c : OmegaCompletePartialOrder.Chain α<GOAL>IsChain (fun x x_1 => x ≤ x_1) (Set.range ⇑c)
<VAR>α : Type u<VAR>Preorder α<VAR>c : OmegaCompletePartialOrder.Chain α<GOAL>Directed (fun x x_1 => x ≤ x_1) ⇑c
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o β<GOAL>⇑(c.map f) = ⇑f ∘ ⇑c
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>c : OmegaCompletePartialOrder.Chain α<VAR>f : α →o β<VAR>x : α<GOAL>x ∈ c → f x ∈ c.map f