ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x<GOAL>ContDiff 𝕜 n fun x => x.1 x.2
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x<GOAL>s ⊆ (fun x => (g x, f x)) ⁻¹' univ
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>ofSym (Sym.map (⇑e) s) = ofSym s
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>map (fun x => count x (map ⇑e ↑s)) (map ⇑e ↑s).dedup = map (fun x => count x ↑s) (↑s).dedup
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>map (fun x => count x (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun x => count x ↑s) (↑s).dedup
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>map (fun x => count (e x) (map ⇑e ↑s)) (↑s).dedup = map (fun x => count x ↑s) (↑s).dedup
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<GOAL>(fun x => count (e x) (map ⇑e ↑s)) = fun x => count x ↑s
<VAR>n : ℕ<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>inst✝¹ : DecidableEq σ<VAR>inst✝ : DecidableEq τ<VAR>e : σ ≃ τ<VAR>s : Sym σ n<VAR>i : σ<GOAL>count (e i) (map ⇑e ↑s) = count i ↑s
<VAR>X : Type u_1<VAR>x : X<GOAL>(of x).support = {x}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>τ : Ω → ℕ<VAR>hτ : IsStoppingTime f τ<VAR>i : ℕ<GOAL>IsStoppingTime f fun ω => τ ω + i
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>τ : Ω → ℕ<VAR>hτ : IsStoppingTime f τ<VAR>i j : ℕ<GOAL>MeasurableSet {ω | τ ω + i = j}
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>t : Set E<VAR>ht : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p t<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>t : Set E<VAR>ht : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p t<VAR>u : Set E<VAR>huo : IsOpen u<VAR>hxu : x ∈ u<VAR>hut : u ∩ insert x s ⊆ t<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>t : Set E<VAR>ht : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p t<VAR>u : Set E<VAR>huo : IsOpen u<VAR>hxu : x ∈ u<VAR>hut : insert x s ∩ u ⊆ t<GOAL>∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>-1 ≤ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>x : M<GOAL>∃ n y, r ^ n.succ • y = r ^ n • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>x : M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)<GOAL>∃ n y, r ^ n.succ • y = r ^ n • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>r : R<VAR>x : M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → ∀ (x : M), x ∈ LinearMap.range (r ^ n • LinearMap.id) ↔ x ∈ LinearMap.range (r ^ m • LinearMap.id)<GOAL>∃ n y, r ^ n.succ • y = r ^ n • x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : SeminormedAddCommGroup E<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℤ<VAR>x : E<GOAL>‖n • x‖ = ‖↑n‖ * ‖x‖
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(volume (univ.pi fun i => Ioc (a i) (b i))).toReal = ∏ i : ι, (b i - a i)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : K<GOAL>(∀ (i : PrimeSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔ x ∈ ⊥
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c a : α<VAR>u : αˣ<GOAL>a /ₚ u * ↑u = 1 * ↑u ↔ a = ↑u
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<GOAL>X.str F ∈ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<GOAL>X.str F ∈ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<GOAL>X.str F ∈ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<GOAL>X.str F ∈ Compactum.cl A
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<GOAL>∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<VAR>claim4 : FiniteInter (finiteInterClosure C1)<GOAL>∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<VAR>claim4 : FiniteInter (finiteInterClosure C1)<VAR>claim5 : FiniteInter C0<GOAL>∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<VAR>claim4 : FiniteInter (finiteInterClosure C1)<VAR>claim5 : FiniteInter C0<VAR>claim6 : ∀ P ∈ C2, P.Nonempty<VAR>T : fsu<VAR>hT : ι T ⊆ C1<GOAL>⋂₀ ι T ∈ C2
<VAR>X : Compactum<VAR>A : Set X.A<VAR>F : Ultrafilter X.A<VAR>hF : F ∈ Compactum.basic (Compactum.cl A)<VAR>fsu : Type u_1 := Finset (Set (Ultrafilter X.A))<VAR>ssu : Type u_1 := Set (Set (Ultrafilter X.A))<VAR>ι : fsu → ssu := fun x => ↑x<VAR>C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}<VAR>AA : Set (Ultrafilter X.A) := {G | A ∈ G}<VAR>C1 : ssu := insert AA C0<VAR>C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1<VAR>claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0<VAR>claim2 : ∀ B ∈ C0, B.Nonempty<VAR>claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty<VAR>claim4 : FiniteInter (finiteInterClosure C1)<VAR>claim5 : FiniteInter C0<VAR>claim6 : ∀ P ∈ C2, P.Nonempty<VAR>T : fsu<VAR>hT : ι T ⊆ C1<GOAL>↑T ⊆ finiteInterClosure C1
<VAR>m : ℕ+<VAR>v : PrimeMultiset<GOAL>m.factorMultiset ≤ v ↔ m ∣ v.prod
<VAR>m : ℕ+<VAR>v : PrimeMultiset<VAR>h : m.factorMultiset ≤ v.prod.factorMultiset ↔ m ∣ v.prod := factorMultiset_le_iff<GOAL>m.factorMultiset ≤ v ↔ m ∣ v.prod
<VAR>m : ℕ+<VAR>v : PrimeMultiset<VAR>h : m.factorMultiset ≤ v ↔ m ∣ v.prod<GOAL>m.factorMultiset ≤ v ↔ m ∣ v.prod
<VAR>α : Type u<VAR>L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)<VAR>x✝ : α<VAR>b✝ : Bool<VAR>h' : [] = L₁ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂<GOAL>False
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>hf : MellinConvergent f s<VAR>𝕜 : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : SMulCommClass ℂ 𝕜 E<VAR>c : 𝕜<GOAL>MellinConvergent (fun t => c • f t) s
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(emptyOn α)✶ = emptyOn α
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(emptyOn α)✶.E = ∅
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>ζ ξ : R<VAR>h : IsPrimitiveRoot ζ k<VAR>hξ : ξ ^ k = 1<VAR>h0 : 0 < k<GOAL>∃ i < k, ζ ^ i = ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>ξ : R<VAR>hξ : ξ ^ k = 1<VAR>h0 : 0 < k<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot (↑ζ) k<GOAL>∃ i < k, ↑ζ ^ i = ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>k : ℕ<VAR>h0 : 0 < k<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot (↑ζ) k<VAR>ξ : Rˣ<VAR>hξ : ↑ξ ^ k = 1<GOAL>∃ i < k, ↑ζ ^ i = ↑ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ ξ : Rˣ<VAR>k : ℕ+<VAR>h : IsPrimitiveRoot ↑ζ ↑k<VAR>hξ : ↑ξ ^ ↑k = 1<GOAL>∃ i < ↑k, ↑ζ ^ i = ↑ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ ξ : Rˣ<VAR>k : ℕ+<VAR>h : IsPrimitiveRoot ↑ζ ↑k<VAR>hξ : ↑ξ ^ ↑k = 1<GOAL>∃ i < ↑k, ζ ^ i = ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ ξ : Rˣ<VAR>k : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>hξ : ↑ξ ^ ↑k = 1<GOAL>∃ i < ↑k, ζ ^ i = ξ
<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>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k✝<VAR>inst✝ : IsDomain R<VAR>ζ ξ : Rˣ<VAR>k : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>hξ : ↑ξ ^ ↑k = 1<GOAL>ξ ∈ rootsOfUnity k R
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hgl : Tendsto (↑g) atBot (𝓝 l)<VAR>x : ℝ<GOAL>↑f x = ↑g x
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hgl : Tendsto (↑g) atBot (𝓝 l)<VAR>x : ℝ<VAR>hf : f.measure (Iic x) = ofReal (↑f x - l)<GOAL>↑f x = ↑g x
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hgl : Tendsto (↑g) atBot (𝓝 l)<VAR>x : ℝ<VAR>hf : ↑f x - l = ↑g x - l<GOAL>↑f x = ↑g x
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hgl : Tendsto (↑g) atBot (𝓝 l)<VAR>x : ℝ<VAR>hf : ofReal (↑g x - l) = ofReal (↑f x - l)<GOAL>0 ≤ ↑g x - l
<VAR>f g : StieltjesFunction<VAR>l : ℝ<VAR>hfg : f.measure = g.measure<VAR>hfl : Tendsto (↑f) atBot (𝓝 l)<VAR>hgl : Tendsto (↑g) atBot (𝓝 l)<VAR>x : ℝ<VAR>hf : ofReal (↑g x - l) = ofReal (↑f x - l)<GOAL>0 ≤ ↑f x - l
<VAR>a b : Ordinal.{u_1}<GOAL>a.toPGame ≤ b.toPGame ∧ b.toPGame ≤ a.toPGame ↔ a = b
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : CompactSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>IsCompact univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : CompactSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>IsCompact (range f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230577, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>p : ℤ<GOAL>(lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 rotateHomotopyEquiv.proof_3) (-(inl φ).leftShift 1 0 rotateHomotopyEquiv.proof_4) ⋯).f p ≫ (triangle (inr φ)).mor₃.f p = -φ.f (p + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0<GOAL>M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0<GOAL>(M.toSquareBlockProp fun i => ¬¬p i).det * (M.toSquareBlockProp fun i => ¬p i).det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁵ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>M : Matrix m m R<VAR>p : m → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0<GOAL>∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<GOAL>FiniteDimensional.finrank K L = φ ↑n
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra A B<VAR>inst✝⁵ : IsCyclotomicExtension {n} A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<GOAL>FiniteDimensional.finrank K L = φ ↑n
<VAR>J : Type w<VAR>f : J → AddCommGrp<VAR>s : Cone (Discrete.functor f)<VAR>m : s.pt ⟶ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.pt<VAR>w : ∀ (j : Discrete J), m ≫ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.π.app j = s.π.app j<VAR>x : ↑s.pt<GOAL>m x = (lift f s) x
<VAR>J : Type w<VAR>f : J → AddCommGrp<VAR>s : Cone (Discrete.functor f)<VAR>m : s.pt ⟶ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.pt<VAR>w : ∀ (j : Discrete J), m ≫ { pt := of ((j : J) → ↑(f j)), π := Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as }.π.app j = s.π.app j<VAR>x : ↑s.pt<VAR>j : J<GOAL>m x j = (lift f s) x j