ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<VAR>h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)<VAR>hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)<GOAL>(cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) 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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<VAR>h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)<VAR>hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)<VAR>hg0 : Function.extend Subtype.val (⇑f) g 0 = 0<GOAL>(cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) 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>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<VAR>h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)<VAR>hg : ContinuousOn (Function.extend Subtype.val (⇑f) g) (σₙ R a)<VAR>hg0 : Function.extend Subtype.val (⇑f) g 0 = 0<GOAL>(cfcₙHom ha) f = (cfcₙHom ha) { toFun := (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g), continuous_toFun := ⋯, map_zero' := hg0 }
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>s t : Set α<VAR>f✝ g : α → G<VAR>a : α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>(t \ s).mulIndicator f * s.mulIndicator f = t.mulIndicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>inst✝ : Group G<VAR>s t : Set α<VAR>f✝ g : α → G<VAR>a : α<VAR>h : s ⊆ t<VAR>f : α → G<GOAL>Disjoint (t \ s) s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>a : α<GOAL>(insert a s).IsPWO ↔ s.IsPWO
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>hf : Integrable f μ<GOAL>Tendsto (fun A => ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun x => |f x|) a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => |f x|) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>hf : Integrable f μ<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => truncation f n a) atTop (𝓝 (f a))
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<GOAL>C x₁ hx₁
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<GOAL>∃ (x : x₁ ∈ ⨆ i, S i), C x₁ x
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<VAR>i : ι<VAR>x₂ : M<VAR>hx₂ : x₂ ∈ S i<GOAL>(fun x' => ∃ (hx'' : x' ∈ ⨆ i, S i), C x' hx'') x₂
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<VAR>x₃ y : M<GOAL>(fun x' => ∃ (hx'' : x' ∈ ⨆ i, S i), C x' hx'') x₃ → (fun x' => ∃ (hx'' : x' ∈ ⨆ i, S i), C x' hx'') y → (fun x' => ∃ (hx'' : x' ∈ ⨆ i, S i), C x' hx'') (x₃ * y)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>m n : ℕ<VAR>ha : a ^ m ∈ I<VAR>hb : b ^ n ∈ I<GOAL>m + n ≤ m + n - 1 + 1
<VAR>k : ℕ<VAR>ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup<VAR>n : ℕ<GOAL>(antidiagonalTuple (k + 1) n).Nodup
<VAR>k : ℕ<VAR>ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup<VAR>n : ℕ<GOAL>(∀ x ∈ antidiagonal n, (map (fun x_1 => Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup) ∧ Pairwise (fun a b => (map (fun x => Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint (map (fun x => Fin.cons b.1 x) (antidiagonalTuple k b.2))) (antidiagonal n)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α✝ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : TopologicalSpace X<VAR>inst✝¹¹ : TopologicalSpace Y<VAR>inst✝¹⁰ : SMul M X<VAR>inst✝⁹ : ContinuousSMul M X<VAR>R : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : AddCommMonoid β<VAR>inst✝⁴ : Module R α<VAR>inst✝³ : Module R β<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : LinearMapClass F R α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousSMul R β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>ContinuousSMul R α
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α✝ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : TopologicalSpace X<VAR>inst✝¹¹ : TopologicalSpace Y<VAR>inst✝¹⁰ : SMul M X<VAR>inst✝⁹ : ContinuousSMul M X<VAR>R : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : AddCommMonoid β<VAR>inst✝⁴ : Module R α<VAR>inst✝³ : Module R β<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : LinearMapClass F R α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousSMul R β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous (⇑f ∘ fun p => p.1 • p.2)
<VAR>M : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α✝ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : TopologicalSpace X<VAR>inst✝¹¹ : TopologicalSpace Y<VAR>inst✝¹⁰ : SMul M X<VAR>inst✝⁹ : ContinuousSMul M X<VAR>R : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : AddCommMonoid β<VAR>inst✝⁴ : Module R α<VAR>inst✝³ : Module R β<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : LinearMapClass F R α β<VAR>tβ : TopologicalSpace β<VAR>inst✝ : ContinuousSMul R β<VAR>f : F<VAR>tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ<GOAL>Continuous fun x => x.1 • f x.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>x ⤳ y ∧ y ⤳ x ↔ x ∈ closure {y} ∧ y ∈ closure {x}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S✝ : Subsemigroup M<VAR>ι : Sort u_4<VAR>S : ι → Subsemigroup M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>α : Type u<VAR>R : α → α → Prop<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s : SignedMeasure α<VAR>μ : Measure α<GOAL>(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s : SignedMeasure α<VAR>μ : Measure α<VAR>this : (s.singularPart μ).toJordanDecomposition = JordanDecomposition.mk (s.toJordanDecomposition.posPart.singularPart μ) (s.toJordanDecomposition.negPart.singularPart μ) ⋯<GOAL>(s.singularPart μ).totalVariation = s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : delta * ls < rs<VAR>v : Valid' o₁ t ↑rx<VAR>e : t.size = ls + rl.size<GOAL>Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : delta * ls < rs<VAR>v : Valid' o₁ t ↑rx<VAR>e : t.size = ll.size + lr.size + 1 + rl.size<GOAL>Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1<VAR>v : Valid' o₁ t ↑rx<VAR>e : t.size = ll.size + lr.size + 1 + rl.size<GOAL>Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1<VAR>v : Valid' o₁ t ↑rx<VAR>e : t.size = ll.size + lr.size + 1 + rl.size<VAR>H : rl.size + rr.size ≤ 1<GOAL>Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ls : ℕ<VAR>ll : Ordnode α<VAR>lx : α<VAR>lr : Ordnode α<VAR>rs : ℕ<VAR>rl : Ordnode α<VAR>rx : α<VAR>rr t : Ordnode α<VAR>hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂<VAR>hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂<VAR>h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1<VAR>v : Valid' o₁ t ↑rx<VAR>e : t.size = ll.size + lr.size + 1 + rl.size<VAR>hr₁ : rl.size ≤ delta * rr.size<VAR>hr₂ : rr.size ≤ delta * rl.size<GOAL>Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>Y Z : C<VAR>g : Y ⟶ Z<VAR>X' : C<VAR>f' : Z ⟶ X'<VAR>g' : X' ⟶ (shiftFunctor C 1).obj Y<VAR>mem : Triangle.mk g f' g' ∈ distinguishedTriangles<GOAL>∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>‖(algebraMap ℝ A) ↑‖a‖₊ - a + ((algebraMap ℝ A) ↑‖b‖₊ - b)‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>‖(algebraMap ℝ A) ↑‖a‖₊ - a‖₊ + ‖(algebraMap ℝ A) ↑‖b‖₊ - b‖₊ ≤ ‖a‖₊ + ‖b‖₊
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>‖(algebraMap ℝ A) ↑‖a‖₊ - a‖₊ ≤ ‖a‖₊
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>a b : A<VAR>ha₁ : IsSelfAdjoint a<VAR>hb₁ : IsSelfAdjoint b<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<VAR>hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal<GOAL>‖(algebraMap ℝ A) ↑‖b‖₊ - b‖₊ ≤ ‖b‖₊
<VAR>A : Type u_1<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra ℝ A<VAR>F : ℂ →ₐ[ℝ] A<GOAL>F I * F I = -1
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>v : Fin n → α<VAR>x✝ : Fin n<GOAL>vecAppend ⋯ ![] v x✝ = v x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>m : Multiset α<VAR>a : α<VAR>l : List α<GOAL>prod ⟦l⟧ = 1 ↔ ∀ x ∈ ⟦l⟧, x = 1
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>f : Filtration ℕ m<VAR>u : ℕ → Ω → β<VAR>τ π : Ω → ℕ<VAR>inst✝ : AddCommMonoid β<VAR>n : ℕ<VAR>this : {a | n ≤ τ a}.indicator (u n) = {a | n + 1 ≤ τ a}.indicator (u n) + {a | τ a = n}.indicator (u n)<GOAL>stoppedProcess u τ n = {a | n + 1 ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range (n + 1), {a | τ a = i}.indicator (u i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>hx : ‖x‖ = 1<VAR>hy : ‖y‖ = 1<GOAL>⟪x, y⟫_ℝ < 1 ↔ x ≠ y
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s✝ t : Set α<VAR>a : α<VAR>s : LowerSet α<GOAL>Set.Iic 1 * ↑s ⊆ ↑s
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s✝ t : Set α<VAR>a : α<VAR>s : LowerSet α<GOAL>⋃ a ∈ Set.Iic 1, a • ↑s ⊆ ↑s
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>m + n = 0
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>(shiftFunctor C n).map ((shiftFunctorAdd' C n m 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) = (shiftFunctorAdd' C m n 0 ⋯).inv.app ((shiftFunctor C n).obj X) ≫ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X)
<VAR>f g : MulRingNorm ℚ<GOAL>(∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g
<VAR>f g : MulRingNorm ℚ<VAR>h : ∀ (n : ℕ), f ↑n = g ↑n<GOAL>f = g
<VAR>f g : MulRingNorm ℚ<VAR>h : ∀ (n : ℕ), f ↑n = g ↑n<VAR>z : ℚ<GOAL>f z = g z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<GOAL>g ∈ closure (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>g : { g // 0 ≤ g }<VAR>this✝¹ : MeasurableSpace G := borel G<VAR>this✝ : BorelSpace G<VAR>hg_memℒp : Memℒp (↑↑↑g) p μ<VAR>zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}<VAR>this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})<VAR>g_meas : Measurable ↑↑↑g<VAR>x : ℕ → α →ₛ G := fun n => SimpleFunc.approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n<VAR>hx_nonneg : ∀ (n : ℕ), 0 ≤ x n<GOAL>∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)