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>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<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>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e'✝ : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ contDiffGroupoid ⊤ I'<VAR>hs : s ⊆ f ⁻¹' e'.source<VAR>hx : f x ∈ e'.source<VAR>h : ContDiffWithinAt 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)<VAR>A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'<VAR>this : ContDiffWithinAt 𝕜 ⊤ (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))<GOAL>↑I.symm ⁻¹' s ∩ range ↑I ⊆ ↑I' ∘ f ∘ ↑I.symm ⁻¹' (↑I'.symm ⁻¹' e'.source ∩ range ↑I')
<VAR>x : ℝ<GOAL>deriv^[2] (fun x => √x * log x) x = -log x / (4 * √x ^ 3)
<VAR>x : ℝ<GOAL>deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)
<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)
<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>n : ℕ<GOAL>((addBottom L).nth (n + 1)).1 = false
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>x : X<VAR>hx : x ∈ s<GOAL>1 ≤ μH[0] s
<VAR>a b : ℕ+<GOAL>(a.xgcd b).wp + (a.xgcd b).x + 1 = (a.xgcd b).wp + 1 + (a.xgcd b).x
<VAR>m n a b c d : ℕ<VAR>h : a / c ≡ b / c [MOD m / c]<VAR>ha✝¹ : c ∣ a<VAR>ha✝ : c ∣ b<VAR>ha : c ∣ m<GOAL>a ≡ b [MOD m]
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.181396, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>h : n + 1 = m<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + n = p₂<VAR>h₂₃ : p₂ + 1 = p₃<GOAL>(liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (↑(fst φ)).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<GOAL>(map f μ).singularPart (map f ν) = map f (μ.singularPart ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))<GOAL>(map f μ).singularPart (map f ν) = map f (μ.singularPart ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>h_add : map f μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))<GOAL>map f (μ.singularPart ν) ⟂ₘ map f ν
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>h : B.orthogonal W = ⊤<GOAL>W = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>h : B.orthogonal W = ⊤<VAR>this : W ⊓ B.orthogonal W = ⊥<GOAL>W = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a c : α<VAR>d : αˣ<GOAL>a * c ~ᵤ a * ↑d * c
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>A : ∀ (n : ℕ), ∃ f, EqOn (⇑f) 1 s ∧ EqOn (⇑f) 0 (U n ∩ interior m)ᶜ ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<GOAL>Continuous g
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<GOAL>s = ⇑{ toFun := g, continuous_toFun := ?intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1 } ⁻¹' {1}
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<GOAL>HasCompactSupport ⇑{ toFun := g, continuous_toFun := ?intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1 }
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<VAR>x : X<GOAL>0 ≤ { toFun := g, continuous_toFun := ?intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1 } x
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>U : ℕ → Set X<VAR>U_open : ∀ (n : ℕ), IsOpen (U n)<VAR>hU : s = ⋂ n, U n<VAR>m : Set X<VAR>m_comp : IsCompact m<VAR>sm : s ⊆ interior m<VAR>mt : m ⊆ tᶜ<VAR>f : ℕ → C(X, ℝ)<VAR>fs : ∀ (n : ℕ), EqOn (⇑(f n)) 1 s<VAR>fm : ∀ (n : ℕ), EqOn (⇑(f n)) 0 (U n ∩ interior m)ᶜ<VAR>_hf : ∀ (n : ℕ), HasCompactSupport ⇑(f n)<VAR>f_range : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (i : ℕ), 0 < u i<VAR>u_sum : Summable u<VAR>hu : ∑' (i : ℕ), u i = 1<VAR>g : X → ℝ := fun x => ∑' (n : ℕ), u n * (f n) x<VAR>hgmc : EqOn g 0 mᶜ<VAR>I : ∀ (n : ℕ) (x : X), u n * (f n) x ≤ u n<VAR>S : ∀ (x : X), Summable fun n => u n * (f n) x<VAR>x : X<GOAL>{ toFun := g, continuous_toFun := ?intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1 } x ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.783706) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ 1<VAR>hf : ContinuousOn f (spectrum R a)<VAR>ha : p a<GOAL>(cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.783706) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ 1<VAR>hf : ContinuousOn f (spectrum R a)<VAR>ha : p a<GOAL>(cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ≤ (cfcHom ha) 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, f x ≤ 1<VAR>hf : ContinuousOn f (spectrum R a)<VAR>ha : p a<GOAL>{ toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } ≤ 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>γ : Type u_8<VAR>δ : Type u_9<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : DistribMulAction M A<VAR>r : M<VAR>x : A<GOAL>r • -x + r • x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set α<GOAL>⋃ (_ : s.Nonempty), s = s
<VAR>s : Set Game<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>0 ≤ star x ↔ 0 ≤ x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>Y' : ?m.129704<VAR>j : J<GOAL>φ j ≫ (mapBifunctorRightUnitor F Y e p hp X').inv j = (mapBifunctorRightUnitor F Y e p hp X).inv j ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>Y' : ?m.129704<VAR>j : J<GOAL>φ j ≫ e.inv.app (X' j) ≫ (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ = e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ (F.map (φ j)).app ((single₀ I).obj Y 0) ≫ (F.obj (X' j)).map (𝟙 ((single₀ I).obj Y) 0) ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>Y' : ?m.129704<VAR>j : J<GOAL>φ j ≫ e.inv.app (X' j) ≫ (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ = e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ (F.map (φ j)).app ((single₀ I).obj Y 0) ≫ (F.obj (X' j)).map (𝟙 ((single₀ I).obj Y 0)) ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>I : Type u_3<VAR>J : Type u_4<VAR>inst✝⁷ : Category.{u_6, u_1} C<VAR>inst✝⁶ : Category.{u_5, u_2} D<VAR>inst✝⁵ : Zero I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : HasInitial C<VAR>F : D ⥤ C ⥤ D<VAR>Y : C<VAR>e : F.flip.obj Y ≅ 𝟭 D<VAR>inst✝² : (X : D) → PreservesColimit (Functor.empty C) (F.obj X)<VAR>p : J × I → J<VAR>hp : ∀ (j : J), p (j, 0) = j<VAR>X X' : GradedObject J D<VAR>φ : X ⟶ X'<VAR>inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p<VAR>inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p<VAR>Y' : ?m.129704<VAR>j : J<GOAL>φ j ≫ e.inv.app (X' j) ≫ (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ = e.inv.app (X j) ≫ (F.map (φ j)).app Y ≫ (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>angle x y = |(x / y).arg|
<VAR>a x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|