ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>inst✝² : SemilatticeInf α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : atBot.IsCountablyGenerated<VAR>μ : Measure α<VAR>a : α<VAR>this : Nonempty α<VAR>h_mono : Antitone fun x => μ (Ioc x a)<VAR>xs : ℕ → α<VAR>hxs_mono : Antitone xs<VAR>hxs_tendsto : Tendsto xs atTop atBot<VAR>h_Iic : Iic a = ⋃ n, Ioc (xs n) a<GOAL>Directed (fun x x_1 => x ⊆ x_1) fun n => Ioc (xs n) a
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : Norm α<VAR>inst✝ : Norm β<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : WithLp p (α × β)<GOAL>‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : Norm α<VAR>inst✝ : Norm β<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : WithLp p (α × β)<VAR>this : 0 < p.toReal<GOAL>‖f‖ = (‖f.1‖ ^ n + ‖f.2‖ ^ n) ^ (1 / ↑n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type w<VAR>f : ι → Set α<VAR>s : Finset ι<GOAL>⨅ i ∈ ↑s, 𝓟 (f i) = 𝓟 (⋂ i ∈ ↑s, f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a ≤ a ∆ b ⊔ b
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>logb b x < y ↔ b ^ y < x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>IsUnit ↑↑n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>Ideal.span {↑↑n} = ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>¬CharZero (R ⧸ Ideal.span {↑↑n})
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<VAR>h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<VAR>h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})<GOAL>↑↑n = ↑0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<VAR>h_char_zero : CharZero (R ⧸ Ideal.span {↑↑n})<GOAL>↑↑n ∈ Ideal.span {↑↑n}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝² : HasMulticoequalizer I<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>b : I.R<GOAL>Sigma.ι I.right b ≫ sigmaπ I = π I b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝² : HasMulticoequalizer I<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>b : I.R<GOAL>Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap = π I b ≫ (colimit.isoColimitCocone { cocone := I.multicoforkEquivSigmaCofork.inverse.obj (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap)), isColimit := IsColimit.ofPreservesCoconeInitial I.multicoforkEquivSigmaCofork.inverse (colimit.isColimit (parallelPair I.fstSigmaMap I.sndSigmaMap)) }).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝² : HasMulticoequalizer I<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>b : I.R<GOAL>Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap = (Multicofork.ofSigmaCofork I (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap))).π b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>a : α<VAR>b : β<VAR>s : WSeq α<VAR>t : WSeq β<GOAL>Computation.LiftRel (LiftRelO R (LiftRel R)) (cons a s).destruct (cons b t).destruct ↔ R a b ∧ LiftRel R s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure α<VAR>f : α → Measure β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<GOAL>(m.bind f) s = ∫⁻ (a : α), (f a) s ∂m
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G_obj Y<GOAL>F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G_obj Y<GOAL>f ≫ (e X Y) ((e X Y).symm g) = f ≫ g
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x x_1 => x * x_1) (1 * 1) (fun x => f x) (s₁.disjUnion s₂ h)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝ : CommMonoid β<VAR>h : Disjoint s₁ s₂<GOAL>∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x x_1 => x * x_1) 1 (fun x => f x) (s₁.disjUnion s₂ h)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>g : E → F<VAR>c✝ : ℝ≥0<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : Fact (1 ≤ p)<VAR>𝕜' : Type u_6<VAR>inst✝³ : NormedRing 𝕜'<VAR>inst✝² : Module 𝕜' F<VAR>inst✝¹ : BoundedSMul 𝕜' F<VAR>inst✝ : SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(Lp E p μ)<GOAL>(compLpL p μ (c • L)) f = (c • compLpL p μ L) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t✝ : Set α<VAR>inst✝ : Fintype ↑s<VAR>t : Finset α<GOAL>s.toFinset ⊂ t ↔ s ⊂ ↑t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : OrderedCommRing R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.869645) [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>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc f a ≤ 0 ↔ ∀ x ∈ spectrum R a, f x ≤ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : OrderedCommRing R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalRing R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.869645) [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>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ cfc (fun x => -f x) a ↔ ∀ x ∈ spectrum R a, 0 ≤ -f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : ContDiffOn ℝ (↑n) f s<GOAL>ContinuousOn (fun t => taylorWithinEval f n s t x) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : ContDiffOn ℝ (↑n) f s<GOAL>ContinuousOn (fun t => ∑ k ∈ Finset.range (n + 1), ((↑k !)⁻¹ * (x - t) ^ k) • iteratedDerivWithin k f s t) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : ContDiffOn ℝ (↑n) f s<VAR>i : ℕ<VAR>hi : i ∈ Finset.range (n + 1)<GOAL>ContinuousOn (fun t => ((↑i !)⁻¹ * (x - t) ^ i) • iteratedDerivWithin i f s t) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : ContDiffOn ℝ (↑n) f s<VAR>i : ℕ<VAR>hi : i ∈ Finset.range (n + 1)<GOAL>ContinuousOn (iteratedDerivWithin i f s) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>hf : (∀ (m : ℕ), ↑m ≤ ↑n → ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s<VAR>i : ℕ<VAR>hi : i ∈ Finset.range (n + 1)<GOAL>ContinuousOn (iteratedDerivWithin i f s) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>i : ℕ<VAR>hi : i ∈ Finset.range (n + 1)<VAR>right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s<VAR>hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s<GOAL>ContinuousOn (iteratedDerivWithin i f s) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>i : ℕ<VAR>right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s<VAR>hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s<VAR>hi : i < n + 1<GOAL>ContinuousOn (iteratedDerivWithin i f s) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>x : ℝ<VAR>n : ℕ<VAR>s : Set ℝ<VAR>hs : UniqueDiffOn ℝ s<VAR>i : ℕ<VAR>right✝ : ∀ (m : ℕ), ↑m < ↑n → DifferentiableOn ℝ (iteratedDerivWithin m f s) s<VAR>hf_left : ↑i ≤ ↑n → ContinuousOn (iteratedDerivWithin i f s) s<VAR>hi : i < n + 1<GOAL>↑i ≤ ↑n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M''<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>G : Type u_8<VAR>hG : Group G<VAR>inst✝³ : DistribMulAction G R<VAR>inst✝² : DistribMulAction G M<VAR>inst✝¹ : IsScalarTower G R M<VAR>inst✝ : SMulCommClass G R M<VAR>v : ι → M<VAR>hv : LinearIndependent R v<VAR>w : ι → G<GOAL>LinearIndependent R (w • v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M''<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>G : Type u_8<VAR>hG : Group G<VAR>inst✝³ : DistribMulAction G R<VAR>inst✝² : DistribMulAction G M<VAR>inst✝¹ : IsScalarTower G R M<VAR>inst✝ : SMulCommClass G R M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → G<GOAL>∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M''<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>G : Type u_8<VAR>hG : Group G<VAR>inst✝³ : DistribMulAction G R<VAR>inst✝² : DistribMulAction G M<VAR>inst✝¹ : IsScalarTower G R M<VAR>inst✝ : SMulCommClass G R M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → G<VAR>s : Finset ι<VAR>g : ι → R<VAR>hgs : ∀ i ∉ s, g i = 0<VAR>hsum : ∑ i ∈ s, g i • (w • v) i = 0<VAR>i : ι<GOAL>g i = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M''<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>G : Type u_8<VAR>hG : Group G<VAR>inst✝³ : DistribMulAction G R<VAR>inst✝² : DistribMulAction G M<VAR>inst✝¹ : IsScalarTower G R M<VAR>inst✝ : SMulCommClass G R M<VAR>v : ι → M<VAR>hv : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>w : ι → G<VAR>s : Finset ι<VAR>g : ι → R<VAR>hgs : ∀ i ∉ s, g i = 0<VAR>hsum : ∑ i ∈ s, g i • (w • v) i = 0<VAR>i : ι<GOAL>w i • g i = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<GOAL>f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>(fun s => ↑((haarContent K₀).toFun s)) K₀.toCompacts = 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>⟨1, ⋯⟩ = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Set.range ⇑(pullback.fst g f ≫ g).val.base = Set.range ⇑g.val.base ∩ Set.range ⇑f.val.base
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<GOAL>(λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>f g : α → ℝ≥0∞<VAR>Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i<GOAL>∃ i ∈ s, f i ≤ g i
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>f g : α → ℝ≥0∞<VAR>Hle : ∀ i ∈ s, g i < f i<GOAL>∑ i ∈ s, g i < ∑ i ∈ s, f i
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom = (singleObjCyclesSelfIso c j A).hom ≫ f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A B : C<VAR>f : A ⟶ B<GOAL>cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).iCycles j = ((singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv) ≫ ((single C c j).obj B).iCycles j
<VAR>H : Type u<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℂ H<VAR>inst✝ : CompleteSpace H<VAR>S : VonNeumannAlgebra H<VAR>z : H →L[ℂ] H<GOAL>z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g
<VAR>H : Type u<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℂ H<VAR>inst✝ : CompleteSpace H<VAR>S : VonNeumannAlgebra H<VAR>z : H →L[ℂ] H<GOAL>z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<GOAL>∀ (x_1 : ι'), ((b.reindex e).repr x) x_1 = (Finsupp.mapDomain (⇑e) (b.repr x)) x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, a ≤ b → b = a<GOAL>Iic a ⊔ s.erase a = s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Semigroup R<VAR>inst✝ : StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<VAR>z : R<GOAL>IsSelfAdjoint (star z * x * z)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin (n + 1)<VAR>l : Fin n<VAR>h : k ≤ l.castSucc<VAR>a✝ : Nontrivial R<GOAL>b.flag k ≤ LinearMap.ker (b.coord l)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (uIcc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Zero α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(uIcc f g).card = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, (uIcc (f i) (g i)).card
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>f =O[atTop] fun n => ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re<GOAL>f =O[atTop] fun n => ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re<VAR>n : ℕ<VAR>hn : n ≥ 1<GOAL>‖f n‖ ≤ C * ‖↑n ^ s.re‖
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re<VAR>n : ℕ<VAR>hn : n ≥ 1<GOAL>‖↑n ^ s.re‖ = ↑n ^ s.re
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>h_injOn : ∀ (i : ι), InjOn (f i) (s i)<VAR>h_disjoint : univ.PairwiseDisjoint fun i => f i '' s i<VAR>x y : α<VAR>h : hs.piecewise f x = hs.piecewise f y<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>h_injOn : ∀ (i : ι), InjOn (f i) (s i)<VAR>h_disjoint : univ.PairwiseDisjoint fun i => f i '' s i<VAR>x y : α<VAR>h : hs.piecewise f x = hs.piecewise f y<GOAL>hs.index x = hs.index y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>h_injOn : ∀ (i : ι), InjOn (f i) (s i)<VAR>h_disjoint : univ.PairwiseDisjoint fun i => f i '' s i<VAR>x y : α<VAR>h : hs.piecewise f x = hs.piecewise f y<GOAL>¬Disjoint (f (hs.index x) '' s (hs.index x)) (f (hs.index y) '' s (hs.index y))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>β : Type u_3<VAR>f : ι → α → β<VAR>h_injOn : ∀ (i : ι), InjOn (f i) (s i)<VAR>h_disjoint : univ.PairwiseDisjoint fun i => f i '' s i<VAR>x y : α<VAR>h : Disjoint (f (hs.index x) '' s (hs.index x)) (f (hs.index y) '' s (hs.index y))<GOAL>hs.piecewise f x ≠ hs.piecewise f y
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z w : ℂ<GOAL>dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : MulZeroClass α<VAR>s t : Set α<VAR>hs : s.Nonempty<GOAL>0 ⊆ s * 0
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N₁ N₂ : L.Substructure M<VAR>hN₁ : N₁.FG<VAR>hN₂ : N₂.FG<VAR>t₁ : Set M<VAR>ht₁ : t₁.Finite ∧ (closure L).toFun t₁ = N₁<VAR>t₂ : Set M<VAR>ht₂ : t₂.Finite ∧ (closure L).toFun t₂ = N₂<GOAL>(closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'
<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✝¹ : Preorder α<VAR>inst✝ : DecidableEq m<VAR>i j : m<VAR>hij : b j ≤ b i<VAR>c : R<GOAL>(⇑toDual ∘ b) i ≤ (⇑toDual ∘ b) j
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>y : α<VAR>hy : edist y (f y) ≠ ⊤<VAR>h : edist x y ≠ ⊤<GOAL>efixedPoint f hf x hx = efixedPoint f hf y hy
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>y : α<VAR>hy : edist y (f y) ≠ ⊤<VAR>h : edist x y ≠ ⊤<VAR>h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤<GOAL>edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>y : α<VAR>hy : edist y (f y) ≠ ⊤<VAR>h : edist x y ≠ ⊤<VAR>h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤<GOAL>edistLtTopSetoid.Rel x y
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>y : α<VAR>hy : edist y (f y) ≠ ⊤<VAR>h : edist x y ≠ ⊤<VAR>h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤<GOAL>edistLtTopSetoid.Rel y (efixedPoint f hf y hy)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : OuterMeasure α<VAR>R : Type u_3<VAR>inst✝¹ : SMul R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>ι : Sort u_4<VAR>f : ι → OuterMeasure α<VAR>c : R<VAR>s : Set α<GOAL>(c • ⨆ i, f i) s = (⨆ i, c • f i) s
<VAR>α : Type u_1<VAR>inst✝⁷ : AddCommSemigroup α<VAR>inst✝⁶ : PartialOrder α<VAR>inst✝⁵ : ExistsAddOfLE α<VAR>inst✝⁴ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a b c d : α<VAR>inst✝¹ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α HAdd.hAdd LE.le<VAR>h : c ≤ b<GOAL>a - (b - c) = a + c - b