ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : InvolutiveStar α<GOAL>star '' s = s⋆
<VAR>α : Type u_1<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : InvolutiveStar α<GOAL>star '' s = star ⁻¹' s
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>h : EquicontinuousAt (fun f => ⇑↑f) 1<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>h : Equicontinuous (DFunLike.coe ∘ Subtype.val)<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>h : Equicontinuous (DFunLike.coe ∘ Subtype.val)<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>h : Equicontinuous (DFunLike.coe ∘ Subtype.val)<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>h : Equicontinuous fun x => ⇑↑x<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>h : Equicontinuous fun x => ⇑↑x<VAR>hS4 : S4 = DFunLike.coe '' S1<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>hS4 : S4 = DFunLike.coe '' S1<VAR>h : Equicontinuous fun x => ⇑↑x<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>h : Equicontinuous fun x => ⇑↑x<VAR>hS4 : S4 = (U.pi fun x => W) ∩ Set.range DFunLike.coe<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>h : Equicontinuous fun x => ⇑↑x<VAR>hS4 : IsClosed S4<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>F : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁸ : Monoid A<VAR>inst✝¹⁷ : Monoid B<VAR>inst✝¹⁶ : Monoid C<VAR>inst✝¹⁵ : Monoid D<VAR>inst✝¹⁴ : CommGroup E<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : TopologicalSpace C<VAR>inst✝¹⁰ : TopologicalSpace D<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalGroup E<VAR>X : Type u_7<VAR>Y : Type u_8<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : Group X<VAR>inst✝⁵ : TopologicalGroup X<VAR>inst✝⁴ : UniformSpace Y<VAR>inst✝³ : CommGroup Y<VAR>inst✝² : UniformGroup Y<VAR>inst✝¹ : T0Space Y<VAR>inst✝ : CompactSpace Y<VAR>U : Set X<VAR>V : Set Y<VAR>hU : IsCompact U<VAR>hV : V ∈ nhds 1<VAR>W : Set Y<VAR>hWo : W ∈ nhds 1<VAR>hWV : W ⊆ V<VAR>hWc : IsCompact W<VAR>S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo (⇑f) U W}<VAR>S3 : Set C(X, Y) := _root_.toContinuousMap '' S2<VAR>S4 : Set (X → Y) := DFunLike.coe '' S3<VAR>h : Equicontinuous fun x => ⇑↑x<VAR>hS4 : IsClosed S4<VAR>hS2 : (interior S2).Nonempty<GOAL>LocallyCompactSpace (ContinuousMonoidHom X Y)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>nndist x y = 0 → x = y
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>b : Prop<VAR>h₂ : ∃! x, ∃! h, q x h<VAR>h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b<GOAL>b
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>b : Prop<VAR>h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b<VAR>h₂ : ∃! x, ∃ h, q x h<GOAL>b
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q✝ : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Sort u_4<VAR>inst✝ : ∀ (x : α), Subsingleton (p x)<VAR>q : (x : α) → p x → Prop<VAR>b : Prop<VAR>h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b<VAR>h₂ : ∃! x, ∃ h, q x h<GOAL>∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>x : E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>hx : ¬x = 0<VAR>this✝ : ‖c‖ ≠ 0<VAR>this : ‖x‖ ≠ 0<GOAL>T.rayleighQuotient (c • x) = T.rayleighQuotient x
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>x : E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>hx : ¬x = 0<VAR>this✝ : ‖c‖ ≠ 0<VAR>this : ‖x‖ ≠ 0<GOAL>‖c‖ ^ 2 * T.reApplyInnerSelf x * ‖x‖ ^ 2 = T.reApplyInnerSelf x * (‖c‖ * ‖x‖) ^ 2
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν) s = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), μ (Prod.mk x ⁻¹' (Prod.swap ⁻¹' s)) ∂ν = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν
<VAR>V : Type u<VAR>inst✝² : Quiver V<VAR>V' : Type u'<VAR>inst✝¹ : Quiver V'<VAR>V'' : Type u''<VAR>inst✝ : Quiver V''<GOAL>𝟭 (FreeGroupoid V) = lift (𝟭q V ⋙q of V)
<VAR>V : Type u<VAR>inst✝² : Quiver V<VAR>V' : Type u'<VAR>inst✝¹ : Quiver V'<VAR>V'' : Type u''<VAR>inst✝ : Quiver V''<GOAL>of V ⋙q (𝟭 (FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<GOAL>IsCompact (↑↑U ∩ ↑↑V)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<GOAL>IsCompact (↑↑U ∩ ↑↑V)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<GOAL>IsCompact (⋃ i, ↑↑U ∩ ↑↑V ∩ ↑(X.basicOpen ↑i))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<GOAL>∀ (i : ↑↑s'), IsCompact (↑↑U ∩ ↑↑V ∩ ↑(X.basicOpen ↑i))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<VAR>i : ↑↑s'<GOAL>IsCompact (↑↑U ∩ ↑↑V ∩ ↑(X.basicOpen ↑i))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<VAR>i : ↑↑s'<GOAL>IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i) ∩ (↑↑V ∩ ↑(X.basicOpen ↑i)))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<VAR>i : ↑↑s'<GOAL>IsCompact (↑↑U ∩ ↑(X.basicOpen ↑i))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>U V : ↑X.affineOpens<VAR>s' : Finset ↑Γ(X, ⊤)<VAR>hs' : ↑s' ⊆ s<VAR>e : Ideal.span ↑s' = ⊤<VAR>i : ↑↑s'<GOAL>IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<VAR>f g : C(X, ℝ)₀<VAR>this : SemilinearMapClass (C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] C(X, ℝ≥0)) (RingHom.id ℝ≥0) C(X, ℝ≥0)₀ C(X, ℝ≥0)<GOAL>(f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal = (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Zero X<VAR>f g : C(X, ℝ)₀<VAR>this : SemilinearMapClass (C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] C(X, ℝ≥0)) (RingHom.id ℝ≥0) C(X, ℝ≥0)₀ C(X, ℝ≥0)<GOAL>↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) = ↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g : M ⊗[R] N →ₗ[R] P<VAR>H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y<VAR>m : M<VAR>n : N<GOAL>g (m ⊗ₜ[R] n) = (lift f) (m ⊗ₜ[R] n)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>r : R<VAR>φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i<VAR>x✝¹ : (i : ι) → s i<VAR>x✝ : (i : ι) → t i<GOAL>((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ)))).compMultilinearMap (tprod R)) x✝¹).compMultilinearMap (tprod R)) x✝ = ((((r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))).compMultilinearMap (tprod R)) x✝¹).compMultilinearMap (tprod R)) x✝
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>a b : ι<GOAL>K.d a b = 𝟙 (X K (some a)) ≫ K.d a b ≫ 𝟙 (X K (some b))
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(GoodProducts (π C fun x => ord I x < o))<VAR>x✝ : ↑C<GOAL>(Products.eval C ↑l) x✝ = (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(GoodProducts (π C fun x => ord I x < o))<VAR>x✝ : ↑C<GOAL>((πs C o) (Products.eval (π C fun x => ord I x < o) ↑l)) x✝ = (eval (π C fun x => ord I x < o) l) (ProjRestrict C (fun x => ord I x < o) x✝)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s : Finset α<GOAL>∃ f, f.IsCycleOn ↑s ∧ f.support ⊆ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s : Finset α<GOAL>s.toList.formPerm.IsCycleOn ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>s : Finset α<GOAL>↑s = {a | a ∈ s.toList}
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) → ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<GOAL>(∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))) → ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<GOAL>Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f.nnrealPart x) ∂↑(μs i) - ∫ (x : Ω), ↑((-f).nnrealPart x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f.nnrealPart x) ∂↑μ - ∫ (x : Ω), ↑((-f).nnrealPart x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<VAR>f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart<VAR>_def_f_pos : f_pos = f.nnrealPart<VAR>f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart<VAR>_def_f_neg : f_neg = (-f).nnrealPart<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<VAR>f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart<VAR>_def_f_pos : f_pos = f.nnrealPart<VAR>f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart<VAR>_def_f_neg : f_neg = (-f).nnrealPart<VAR>tends_pos : Tendsto (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))