ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.57069, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F ≅ ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ Tendsto (fun x => (f b, f x)) (𝓝 b) (𝓤 α)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<GOAL>μ[f|m] =ᶠ[ae (μ.restrict s)] μ[f|m₂]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<GOAL>s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[f|m₂])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<GOAL>s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[f|m₂])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<GOAL>s.indicator (μ[f|m]) =ᶠ[ae μ] s.indicator (μ[f|m₂])
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<GOAL>μ[s.indicator f|m] =ᶠ[ae μ] μ[s.indicator f|m₂]
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → ∫ (x : α) in s_1, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in s_1, (μ[s.indicator f|m₂]) x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<GOAL>AEStronglyMeasurable' m₂ (μ[s.indicator f|m]) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>a✝ : μ t < ⊤<GOAL>∫ (x : α) in t, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in t, (μ[s.indicator f|m₂]) x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>a✝ : μ t < ⊤<VAR>this : ∫ (x : α) in t, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in s ∩ t, (μ[s.indicator f|m]) x ∂μ<GOAL>∫ (x : α) in t, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in t, (μ[s.indicator f|m₂]) x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>m✝ m0✝ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>μ✝ : Measure α<VAR>f : α → E<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m0<VAR>inst✝¹ : SigmaFinite (μ.trim hm)<VAR>inst✝ : SigmaFinite (μ.trim hm₂)<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)<VAR>hs_m₂ : MeasurableSet s<VAR>hf_int : Integrable f μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>a✝ : μ t < ⊤<VAR>this : ∫ (x : α) in t, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in s ∩ t, (μ[s.indicator f|m]) x ∂μ<VAR>hst_m : MeasurableSet (s ∩ t)<GOAL>∫ (x : α) in t, (μ[s.indicator f|m]) x ∂μ = ∫ (x : α) in t, (μ[s.indicator f|m₂]) x ∂μ
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>inst✝ : SecondCountableTopology α<VAR>ρ : Measure α<VAR>hρ : ρ ≪ μ<GOAL>s ⊆ (s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p
<VAR>α : Type u_1<VAR>inst✝¹ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : v.FineSubfamilyOn f s<VAR>inst✝ : SecondCountableTopology α<VAR>ρ : Measure α<VAR>hρ : ρ ≪ μ<GOAL>ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : x ∈ Ioo ↑a ↑b<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : ↑a < x ∧ x < ↑b<GOAL>p x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : ContinuousOn (g ∘ f) (σₙ R a)<GOAL>cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : ContinuousOn (g ∘ f) (σₙ R a)<VAR>sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a<GOAL>cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : ContinuousOn (g ∘ f) (σₙ R a)<VAR>sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a<GOAL>(cfcₙHom ha) { toFun := (σₙ R a).restrict (g ∘ f), continuous_toFun := ⋯, map_zero' := ⋯ } = (cfcₙHom ⋯) ({ toFun := (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp ?f')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : ContinuousOn (g ∘ f) (σₙ R a)<VAR>sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a<GOAL>C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })))₀
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : MetricSpace R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R A A<VAR>inst✝² : SMulCommClass R A A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>ha : autoParam (p a) _auto✝<VAR>this : ContinuousOn (g ∘ f) (σₙ R a)<VAR>sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a<GOAL>∀ (x : ↑(σₙ R a)), { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x = ↑(?f' x)
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : RightRigidCategory V<VAR>h : ↑H<GOAL>Xᘁ.ρ h = X.ρ h⁻¹ᘁ
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : RightRigidCategory V<VAR>h : ↑H<GOAL>Xᘁ.ρ h = X.ρ (inv h)ᘁ
<VAR>V : Type (u + 1)<VAR>inst✝² : LargeCategory V<VAR>G : MonCat<VAR>inst✝¹ : MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((forget₂ Grp MonCat).obj H)<VAR>inst✝ : RightRigidCategory V<VAR>h : ↑H<GOAL>SingleObj H.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>fa : α ≃o α<VAR>fb : β ↪o β<VAR>g : α → β<VAR>h : Semiconj g ⇑fa ⇑fb<VAR>g' : β → α<VAR>hg' : IsOrderRightAdjoint g g'<GOAL>Semiconj g' ⇑fb ⇑fa
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>fa : α ≃o α<VAR>fb : β ↪o β<VAR>g : α → β<VAR>h : Semiconj g ⇑fa ⇑fb<VAR>g' : β → α<VAR>hg' : IsOrderRightAdjoint g g'<VAR>y : β<GOAL>IsLUB {x | g x ≤ fb y} (fa (g' y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : Preorder β<VAR>fa : α ≃o α<VAR>fb : β ↪o β<VAR>g : α → β<VAR>h : Semiconj g ⇑fa ⇑fb<VAR>g' : β → α<VAR>hg' : IsOrderRightAdjoint g g'<VAR>y : β<GOAL>IsLUB (⇑fa '' {a | g (fa a) ≤ fb y}) (fa (g' y))
<VAR>θ : Angle<GOAL>θ.toReal = π ↔ θ = ↑π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>t : TopologicalSpace α<VAR>h : t ≤ ⨆ s ∈ 𝔖, TopologicalSpace.coinduced Subtype.val inferInstance<VAR>u : Set α<VAR>hu : ∀ s ∈ 𝔖, IsOpen (Subtype.val ⁻¹' u)<GOAL>IsOpen u
<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<GOAL>NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>e : S ≃ₐ[R] T<GOAL>RingHom.ker ((↑↑e).comp h.map) = Ideal.span {f}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>inst✝ : Algebra R T<VAR>h : IsAdjoinRoot S f<VAR>e : S ≃ₐ[R] T<VAR>x✝ : R<GOAL>(algebraMap R T) x✝ = (((↑↑e).comp h.map).comp C) x✝
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 (toIcoMod hp a x)<GOAL>s ∈ Filter.map (toIcoMod hp a) (𝓝[≥] x)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 (toIcoMod hp a x)<GOAL>∃ u ∈ 𝓝 x, u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 (toIcoMod hp a x)<VAR>this : Nontrivial 𝕜<GOAL>∃ u ∈ 𝓝 x, u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>h : ∃ l u, toIcoMod hp a x ∈ Ioo l u ∧ Ioo l u ⊆ s<GOAL>∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>l u : 𝕜<VAR>hxI : toIcoMod hp a x ∈ Ioo l u<VAR>hIs : Ioo l u ⊆ s<VAR>d : 𝕜 := toIcoDiv hp a x • p<GOAL>∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>l u : 𝕜<VAR>hxI : toIcoMod hp a x ∈ Ioo l u<VAR>hIs : Ioo l u ⊆ s<VAR>d : 𝕜 := toIcoDiv hp a x • p<VAR>hd : toIcoMod hp a x ∈ Ico a (a + p)<GOAL>∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ Ioo l u_1 ⊆ u) ∧ u ∩ Ici x ⊆ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>l u : 𝕜<VAR>hxI : toIcoMod hp a x ∈ Ioo l u<VAR>hIs : Ioo l u ⊆ s<VAR>d : 𝕜 := toIcoDiv hp a x • p<VAR>hd : toIcoMod hp a x ∈ Ico a (a + p)<GOAL>∃ u, (∃ l u_1, x ∈ Ioo l u_1 ∧ ∀ x ∈ Ioo l u_1, x ∈ u) ∧ ∀ (x_1 : 𝕜), x_1 ∈ u ∧ x_1 ∈ Ici x → x_1 ∈ toIcoMod hp a ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>l u : 𝕜<VAR>hxI : toIcoMod hp a x ∈ Ioo l u<VAR>hIs : Ioo l u ⊆ s<VAR>d : 𝕜 := toIcoDiv hp a x • p<VAR>hd : toIcoMod hp a x ∈ Ico a (a + p)<GOAL>l < x - d ∧ x - d < a + p ∧ x - d < u
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>s : Set 𝕜<VAR>this : Nontrivial 𝕜<VAR>l u : 𝕜<VAR>hxI : toIcoMod hp a x ∈ Ioo l u<VAR>hIs : Ioo l u ⊆ s<VAR>d : 𝕜 := toIcoDiv hp a x • p<VAR>hd : toIcoMod hp a x ∈ Ico a (a + p)<VAR>y : 𝕜<GOAL>(l < y - d ∧ y - d < a + p ∧ y - d < u) ∧ y ∈ Ici x → y ∈ toIcoMod hp a ⁻¹' s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure s ⊆ s ↔ ∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<GOAL>x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₁ : P<VAR>h : p₁ ∈ s<VAR>hx : x ∉ s<GOAL>y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
<VAR>α : Type u_1<VAR>p q : ℚ≥0<VAR>n : ℕ<GOAL>↑(↑n).toNNRat = ↑↑n