ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<VAR>B : s = ⋃ n, t n<GOAL>Monotone t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : BorelSpace β<VAR>inst✝¹ : SigmaCompactSpace β<VAR>inst✝ : R1Space β<VAR>μ : Measure β<VAR>f : β → E<VAR>hf : Integrable f μ<VAR>h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0<VAR>s : Set β<VAR>hs : IsClosed s<VAR>t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s<VAR>B : s = ⋃ n, t n<GOAL>IntegrableOn f (⋃ n, t n) μ
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β✝ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α α' β : Type u<VAR>f : α → α'<VAR>x : t α β<GOAL>tfst (pure ∘ f) x = pure (fst f x)
<VAR>α β : FinBddDistLat<VAR>e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat<VAR>x✝ : (forget FinBddDistLat).obj α<GOAL>((let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : FinBddDistLat<VAR>e : ↑α.toBddDistLat.toDistLat ≃o ↑β.toBddDistLat.toDistLat<VAR>x✝ : (forget FinBddDistLat).obj β<GOAL>((let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (x - d) = ∫ (x : ℝ) in a - d..b - d, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<GOAL>∃ a ∈ decodeList v.succ, encodeList a = v.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<VAR>h : (unpair v).2 ≤ v<GOAL>∃ a ∈ decodeList v.succ, encodeList a = v.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<VAR>h : (v₁, v₂).2 ≤ v<GOAL>∃ a ∈ decodeList v.succ, encodeList a = v.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<VAR>h : (v₁, v₂).2 ≤ v<VAR>a : List α<VAR>h₁ : a ∈ decodeList v₂<VAR>h₂ : encodeList a = v₂<GOAL>∃ a ∈ decodeList v.succ, encodeList a = v.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<VAR>h : (v₁, v₂).2 ≤ v<VAR>a : List α<VAR>h₁ : decodeList v₂ = some a<VAR>h₂ : encodeList a = v₂<GOAL>∃ a ∈ decodeList v.succ, encodeList a = v.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>v v₁ v₂ : ℕ<VAR>e : unpair v = (v₁, v₂)<VAR>h : (v₁, v₂).2 ≤ v<VAR>a : List α<VAR>h₁ : decodeList v₂ = some a<VAR>h₂ : encodeList a = v₂<GOAL>ofNat α v₁ :: a ∈ decodeList v.succ ∧ encodeList (ofNat α v₁ :: a) = v.succ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : DecidableEq ι<VAR>p : ι → Submodule R N<VAR>inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)<VAR>x : N<GOAL>x ∈ iSup p ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : DecidableEq ι<VAR>p : ι → Submodule R N<VAR>inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)<VAR>x : N<GOAL>(∃ f, ((lsum ℕ) fun i => (p i).subtype) f = x) ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁷ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜₂ G'<VAR>inst✝⁴ : NormedSpace 𝕜' G'<VAR>inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x x' : M<VAR>y : F<GOAL>(f (x - x')) y = (f x) y - (f x') y
<VAR>m n✝ n : ℕ<GOAL>-last n = 1
<VAR>K : Type u_1<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>ζ : K<VAR>n : ℕ<VAR>hz : IsPrimitiveRoot ζ n<GOAL>cyclotomic n K = cyclotomic' n K
<VAR>K : Type u_1<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K<VAR>ζ : K<VAR>hz : IsPrimitiveRoot ζ k<GOAL>cyclotomic k K = cyclotomic' k K
<VAR>K : Type u_1<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K<VAR>ζ : K<VAR>hz : IsPrimitiveRoot ζ k<VAR>hzero : k = 0<GOAL>cyclotomic k K = cyclotomic' k K
<VAR>K : Type u_1<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K<VAR>ζ : K<VAR>hz : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<GOAL>cyclotomic k K = cyclotomic' k K
<VAR>K : Type u_1<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>k : ℕ<VAR>hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K<VAR>ζ : K<VAR>hz : IsPrimitiveRoot ζ k<VAR>hpos : k > 0<VAR>h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K<GOAL>cyclotomic k K = cyclotomic' k K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Option α ≃ Option β<VAR>h : e.symm none = none<GOAL>e none = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Option α ≃ Option β<VAR>h : e none = none<GOAL>e.symm none = none
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ k<VAR>hk : 0 < k<GOAL>IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>hk : 0 < k<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl' : 0 < l<VAR>hl : l < k<GOAL>ζ ^ l ≠ 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>hk : 0 < k<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<VAR>hl' : 0 < l<VAR>hl : l < orderOf ζ<GOAL>ζ ^ l ≠ 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ lowerCentralSeries R L L k<GOAL>(trace R M) (φ x) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ lowerCentralSeries R L L 1<GOAL>(trace R M) (φ x) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}<GOAL>(trace R M) (φ x) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}<VAR>y : L<VAR>x✝ : y ∈ {m | ∃ u v, ⁅u, v⁆ = m}<VAR>u v : L<VAR>huv : ⁅u, v⁆ = y<GOAL>(fun x => (trace R M) (φ x) = 0) y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}<GOAL>(fun x => (trace R M) (φ x) = 0) 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}<VAR>u v : L<VAR>hu : (fun x => (trace R M) (φ x) = 0) u<VAR>hv : (fun x => (trace R M) (φ x) = 0) v<GOAL>(fun x => (trace R M) (φ x) = 0) (u + v)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>k : ℕ<VAR>x : L<VAR>hk : 1 ≤ k<VAR>hx : x ∈ Submodule.span R {m | ∃ u v, ⁅u, v⁆ = m}<VAR>t : R<VAR>u : L<VAR>hu : (fun x => (trace R M) (φ x) = 0) u<GOAL>(fun x => (trace R M) (φ x) = 0) (t • u)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<GOAL>Continuous (coev X Y)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U<GOAL>Continuous (coev X Y)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U<GOAL>∀ (x : Y) (K : Set X), IsCompact K → ∀ (U : Set (Y × X)), IsOpen U → {x} ×ˢ K ⊆ U → ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U<VAR>x : Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set (Y × X)<VAR>hU : IsOpen U<VAR>hKU : {x} ×ˢ K ⊆ U<GOAL>∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U<VAR>x : Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set (Y × X)<VAR>hU : IsOpen U<VAR>hKU : {x} ×ˢ K ⊆ U<VAR>V : Set Y<VAR>W : Set X<VAR>hV : IsOpen V<VAR>hxV : {x} ⊆ V<VAR>hKW : K ⊆ W<VAR>hVWU : V ×ˢ W ⊆ U<GOAL>∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U<VAR>x : Y<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set (Y × X)<VAR>hU : IsOpen U<VAR>hKU : {x} ×ˢ K ⊆ U<VAR>V : Set Y<VAR>W : Set X<VAR>hV : IsOpen V<VAR>hxV : {x} ⊆ V<VAR>hKW : K ⊆ W<VAR>hVWU : V ×ˢ W ⊆ U<VAR>a : Y<VAR>ha : a ∈ V<GOAL>{a} ×ˢ K ⊆ U
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>∀ (a b c : Finset α), a ○ b ○ c ≤ a ○ (b ○ c)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>∀ (a b c : Finset α) (a_1 : α), (∃ a_2 ∈ a, ∃ b_1 ∈ b, Disjoint a_2 b_1 ∧ a_2 ⊔ b_1 = a_1) → ∀ b_1 ∈ c, Disjoint a_1 b_1 → ∃ a_5 ∈ a, ∃ b_2, (∃ a ∈ b, ∃ b ∈ c, Disjoint a b ∧ a ⊔ b = b_2) ∧ Disjoint a_5 b_2 ∧ a_5 ⊔ b_2 = a_1 ⊔ b_1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s✝ t✝ u✝ v s t u : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ t<VAR>hab : Disjoint a b<VAR>c : α<VAR>hc : c ∈ u<VAR>habc : Disjoint (a ⊔ b) c<GOAL>∃ a_1 ∈ s, ∃ b_1, (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s✝ t✝ u✝ v s t u : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ t<VAR>hab : Disjoint a b<VAR>c : α<VAR>hc : c ∈ u<VAR>habc : Disjoint a c ∧ Disjoint b c<GOAL>∃ a_1 ∈ s, ∃ b_1, (∃ a ∈ t, ∃ b ∈ u, Disjoint a b ∧ a ⊔ b = b_1) ∧ Disjoint a_1 b_1 ∧ a_1 ⊔ b_1 = a ⊔ b ⊔ c
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasStrictDerivAt h₂ h₂' (h x)<VAR>hh : HasStrictDerivAt h h' x<VAR>hy : y = h x<GOAL>HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀✝ : ∀ (b : β), Monotone (swap f b)<VAR>h₁✝ : ∀ (a : α), Monotone (f a)<VAR>h₀ : ∀ (b : β), Monotone (swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>a : α<VAR>ha : a ∈ upperBounds s<VAR>b : β<VAR>hb : b ∈ upperBounds t<GOAL>BddAbove (image2 f s t)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable F y<GOAL>Algebra.IsSeparable F ↥F⟮x, y⟯
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable F y<GOAL>Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable (↥F⟮x⟯) y<GOAL>Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x y : E<VAR>hx : Algebra.IsSeparable F ↥F⟮x⟯<VAR>hy : Algebra.IsSeparable ↥F⟮x⟯ ↥(↥F⟮x⟯)⟮y⟯<GOAL>Algebra.IsSeparable F ↥(restrictScalars F (↥F⟮x⟯)⟮y⟯)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>K L : Subgroup N<VAR>hf : Surjective ⇑f<GOAL>comap f K < comap f L ↔ K < L
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>c : ℤ →+* R<VAR>g : τ → R<VAR>p : MvPolynomial σ ℤ<GOAL>eval₂ c (g ∘ f) p = eval₂ c g ((rename f) p)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>egauge 𝕜 s x / ↑‖c‖₊ ≤ egauge 𝕜 (c • s) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>x : E<GOAL>∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ↑‖c‖₊ ≤ ↑‖c_1‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>a : 𝕜<VAR>x : E<VAR>hx : x ∈ s<GOAL>egauge 𝕜 s ((fun x => (a * c) • x) x) / ↑‖c‖₊ ≤ ↑‖a‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>a : 𝕜<VAR>x : E<VAR>hx : x ∈ s<GOAL>egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ↑‖a‖₊ * ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>c✝ : 𝕜<VAR>s✝ t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0∞<VAR>c : 𝕜<VAR>s : Set E<VAR>a : 𝕜<VAR>x : E<VAR>hx : x ∈ s<GOAL>egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ↑‖a * c‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ = ⊤<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < μ {x | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ}<GOAL>0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < μ {x | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ}<GOAL>0 < (μ.restrict s) {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤})<GOAL>0 < (μ.restrict s) {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤})<GOAL>{a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤} ⊆ {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}