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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<GOAL>{i | 0 < (sum (sFiniteSeq μ)) (As i)}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<GOAL>(⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<VAR>n : ℕ<GOAL>{i | 0 < (sFiniteSeq μ n) (As i)}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<VAR>n : ℕ<GOAL>∀ (i : ι), NullMeasurableSet (As i) (sFiniteSeq μ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<VAR>n : ℕ<GOAL>Pairwise (AEDisjoint (sFiniteSeq μ n) on As)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι✝ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>ι : Type u_5<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SFinite μ<VAR>As : ι → Set α<VAR>As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sFiniteSeq μ))<VAR>As_disj : Pairwise (AEDisjoint (sum (sFiniteSeq μ)) on As)<VAR>obs : {i | 0 < (sum (sFiniteSeq μ)) (As i)} ⊆ ⋃ n, {i | 0 < (sFiniteSeq μ n) (As i)}<VAR>n : ℕ<GOAL>(sFiniteSeq μ n) (⋃ i, As i) ≠ ⊤
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ -y ≠ 0<GOAL>angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>m n : ℕ<VAR>a : α<GOAL>replicate (m + n) a = replicate m a ++ replicate n a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>inst✝² : Module.Free R ↑S.X₁<VAR>inst✝¹ : Module.Free R ↑S.X₃<VAR>inst✝ : StrongRankCondition R<GOAL>Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>inst✝² : Module.Free R ↑S.X₁<VAR>inst✝¹ : Module.Free R ↑S.X₃<VAR>inst✝ : StrongRankCondition R<VAR>this : Module.Free R ↑S.X₂<GOAL>Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>inst✝² : Module.Free R ↑S.X₁<VAR>inst✝¹ : Module.Free R ↑S.X₃<VAR>inst✝ : StrongRankCondition R<VAR>this : Module.Free R ↑S.X₂<GOAL>Nonempty (Module.Free.ChooseBasisIndex R ↑S.X₂ ≃ Module.Free.ChooseBasisIndex R ↑S.X₁ ⊕ Module.Free.ChooseBasisIndex R ↑S.X₃)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>x ∈ comap i (separableClosure F K) ↔ x ∈ separableClosure F E
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<GOAL>(s.append t).destruct = s.destruct.bind (destruct_append.aux t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<GOAL>Computation.IsBisimulation fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ t✝ : WSeq α<VAR>c1 c2 : Computation (Option (α × WSeq α))<VAR>s t : WSeq α<VAR>h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)<GOAL>Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1.destruct c2.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ t✝ : WSeq α<VAR>c1 c2 : Computation (Option (α × WSeq α))<VAR>s t : WSeq α<VAR>h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)<GOAL>Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
<VAR>a b c : EReal<GOAL>a / b * c = a * c / b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<GOAL>((a ::ₘ s).pi t).Nodup
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<VAR>has : a ∉ s<GOAL>((a ::ₘ s).pi t).Nodup
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs✝ : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<VAR>has : a ∉ s<VAR>hs : s.Nodup<GOAL>((a ::ₘ s).pi t).Nodup
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs✝ : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<VAR>has : a ∉ s<VAR>hs : s.Nodup<GOAL>(∀ a_1 ∈ t a, (Multiset.map (Pi.cons s a a_1) (s.pi t)).Nodup) ∧ Pairwise (fun a_1 b => (Multiset.map (Pi.cons s a a_1) (s.pi t)).Disjoint (Multiset.map (Pi.cons s a b) (s.pi t))) (t a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs✝ : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<VAR>has : a ∉ s<VAR>hs : s.Nodup<GOAL>Pairwise (fun a_1 b => (Multiset.map (Pi.cons s a a_1) (s.pi t)).Disjoint (Multiset.map (Pi.cons s a b) (s.pi t))) (t a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>β : α → Type u_2<VAR>s✝ : Multiset α<VAR>t : (a : α) → Multiset (β a)<VAR>a : α<VAR>s : Multiset α<VAR>ih : s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup<VAR>hs✝ : (a ::ₘ s).Nodup<VAR>ht : ∀ a_1 ∈ a ::ₘ s, (t a_1).Nodup<VAR>has : a ∉ s<VAR>hs : s.Nodup<GOAL>∀ a_1 ∈ t a, ∀ b ∈ t a, a_1 ≠ b → (Multiset.map (Pi.cons s a a_1) (s.pi t)).Disjoint (Multiset.map (Pi.cons s a b) (s.pi t))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<VAR>h : ∀ (j : n), b j = A j i<GOAL>A.cramer b = Pi.single i A.det
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<VAR>h : ∀ (j : n), b j = A j i<GOAL>Aᵀᵀ.cramer b = Pi.single i Aᵀ.det
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>b : n → α<VAR>i : n<VAR>h : ∀ (j : n), b j = A j i<GOAL>b = Aᵀ i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommMonoid M<VAR>ψ : AddChar R M<VAR>x✝ : R<GOAL>ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<GOAL>a ≤ a + b - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Preorder α<VAR>inst✝² : AddCommSemigroup α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<GOAL>a ≤ b + a - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c d a : α<VAR>n : ℤ<GOAL>a⁻¹ ^ n = a ^ (-n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>𝕜₁ : Type u_4<VAR>𝕜₂ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>inst✝¹⁴ : Nonempty κ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹¹ : RingHomIsometric σ₁₂<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : Module 𝕜₂ F<VAR>inst✝⁶ : UniformSpace E<VAR>inst✝⁵ : UniformSpace F<VAR>inst✝⁴ : UniformAddGroup E<VAR>inst✝³ : UniformAddGroup F<VAR>inst✝² : ContinuousSMul 𝕜₁ E<VAR>inst✝¹ : ContinuousSMul 𝕜₂ F<VAR>inst✝ : BarrelledSpace 𝕜₁ E<VAR>𝓕 : ι → E →SL[σ₁₂] F<VAR>q : SeminormFamily 𝕜₂ F κ<VAR>hq : WithSeminorms q<VAR>H : ∀ (k : κ) (x : E), BddAbove (range fun i => (q k) ((𝓕 i) x))<GOAL>UniformEquicontinuous (DFunLike.coe ∘ 𝓕)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>𝕜₁ : Type u_4<VAR>𝕜₂ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>inst✝¹⁴ : Nonempty κ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹¹ : RingHomIsometric σ₁₂<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : Module 𝕜₂ F<VAR>inst✝⁶ : UniformSpace E<VAR>inst✝⁵ : UniformSpace F<VAR>inst✝⁴ : UniformAddGroup E<VAR>inst✝³ : UniformAddGroup F<VAR>inst✝² : ContinuousSMul 𝕜₁ E<VAR>inst✝¹ : ContinuousSMul 𝕜₂ F<VAR>inst✝ : BarrelledSpace 𝕜₁ E<VAR>𝓕 : ι → E →SL[σ₁₂] F<VAR>q : SeminormFamily 𝕜₂ F κ<VAR>hq : WithSeminorms q<VAR>H : ∀ (k : κ) (x : E), BddAbove (range fun i => (q k) ((𝓕 i) x))<GOAL>∀ (i : κ), BddAbove (range fun k => (q i).comp ((toLinearMap ∘ 𝓕) k)) ∧ Continuous (⨆ k, ⇑((q i).comp ((toLinearMap ∘ 𝓕) k)))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>𝕜₁ : Type u_4<VAR>𝕜₂ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>inst✝¹⁴ : Nonempty κ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹¹ : RingHomIsometric σ₁₂<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : Module 𝕜₂ F<VAR>inst✝⁶ : UniformSpace E<VAR>inst✝⁵ : UniformSpace F<VAR>inst✝⁴ : UniformAddGroup E<VAR>inst✝³ : UniformAddGroup F<VAR>inst✝² : ContinuousSMul 𝕜₁ E<VAR>inst✝¹ : ContinuousSMul 𝕜₂ F<VAR>inst✝ : BarrelledSpace 𝕜₁ E<VAR>𝓕 : ι → E →SL[σ₁₂] F<VAR>q : SeminormFamily 𝕜₂ F κ<VAR>hq : WithSeminorms q<VAR>H : ∀ (k : κ) (x : E), BddAbove (range fun i => (q k) ((𝓕 i) x))<VAR>k : κ<GOAL>BddAbove (range fun k_1 => (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧ Continuous (⨆ k_1, ⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>𝕜₁ : Type u_4<VAR>𝕜₂ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>inst✝¹⁴ : Nonempty κ<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₁<VAR>inst✝¹² : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>inst✝¹¹ : RingHomIsometric σ₁₂<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜₁ E<VAR>inst✝⁷ : Module 𝕜₂ F<VAR>inst✝⁶ : UniformSpace E<VAR>inst✝⁵ : UniformSpace F<VAR>inst✝⁴ : UniformAddGroup E<VAR>inst✝³ : UniformAddGroup F<VAR>inst✝² : ContinuousSMul 𝕜₁ E<VAR>inst✝¹ : ContinuousSMul 𝕜₂ F<VAR>inst✝ : BarrelledSpace 𝕜₁ E<VAR>𝓕 : ι → E →SL[σ₁₂] F<VAR>q : SeminormFamily 𝕜₂ F κ<VAR>hq : WithSeminorms q<VAR>H : ∀ (k : κ) (x : E), BddAbove (range fun i => (q k) ((𝓕 i) x))<VAR>k : κ<VAR>this : BddAbove (range fun i => (q k).comp ↑(𝓕 i))<GOAL>BddAbove (range fun k_1 => (q k).comp ((toLinearMap ∘ 𝓕) k_1)) ∧ Continuous (⨆ k_1, ⇑((q k).comp ((toLinearMap ∘ 𝓕) k_1)))
<VAR>s : ℂ<GOAL>expZeta 0 s = riemannZeta s
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(quotAdjoinRootEquivQuotPolynomialQuot I f).symm ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) = (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Algebra (ZMod p) K<VAR>f : K[X]<GOAL>(expand K q) f = f ^ q
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p✝ : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p✝)<VAR>inst✝ : Algebra (ZMod p✝) K<VAR>f : K[X]<VAR>p : ℕ<VAR>hp : CharP K p<GOAL>(expand K q) f = f ^ q
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p✝ : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p✝)<VAR>inst✝ : Algebra (ZMod p✝) K<VAR>f : K[X]<VAR>p : ℕ<VAR>hp : CharP K p<VAR>this : CharP K p := hp<GOAL>(expand K q) f = f ^ q
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p✝ : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p✝)<VAR>inst✝ : Algebra (ZMod p✝) K<VAR>f : K[X]<VAR>p : ℕ<VAR>hp✝ : CharP K p<VAR>this : CharP K p := hp✝<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hp : Nat.Prime p<VAR>hn : q = p ^ ↑⟨n, npos⟩<GOAL>(expand K q) f = f ^ q
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Fintype K<VAR>p✝ : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p✝)<VAR>inst✝ : Algebra (ZMod p✝) K<VAR>f : K[X]<VAR>p : ℕ<VAR>hp✝ : CharP K p<VAR>this✝ : CharP K p := hp✝<VAR>n : ℕ<VAR>npos : 0 < n<VAR>hp : Nat.Prime p<VAR>hn : q = p ^ n<VAR>this : Fact (Nat.Prime p)<GOAL>(expand K q) f = f ^ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>x : α<VAR>s : Set β<VAR>a✝ : MeasurableSet s<GOAL>((const α 0) x) s = (0 x) s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : x ∈ skewAdjoint R<GOAL>Commute (star x) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : StarRing R<VAR>x : R<VAR>hx : star x = -x<GOAL>Commute (star x) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<GOAL>inner_ 𝕜 (↑(-1) • x) y = (starRingEnd 𝕜) ↑(-1) * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<GOAL>4⁻¹ * (𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖) = -4⁻¹ * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<GOAL>4⁻¹ * (𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖) = 4⁻¹ * -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<GOAL>𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖ = -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<GOAL>𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖ = -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<GOAL>𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖ = -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<VAR>h₃ : ‖I • -x + y‖ = ‖I • x - y‖<GOAL>𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖ = -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x y : E<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<VAR>h₃ : ‖I • -x + y‖ = ‖I • x - y‖<VAR>h₄ : ‖I • -x - y‖ = ‖I • x + y‖<GOAL>𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ + I * 𝓚 ‖I • -x + y‖ * 𝓚 ‖I • -x + y‖ - I * 𝓚 ‖I • -x - y‖ * 𝓚 ‖I • -x - y‖ = -(𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<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>inst✝ : CompleteLattice α<VAR>f : ι → α<VAR>x✝ : α<GOAL>x✝ ∈ Ici (⨆ i, f i) ↔ x✝ ∈ ⋂ i, Ici (f i)
<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>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✝ : ℕ∞<VAR>inst✝¹ : T2Space M<VAR>inst✝ : One M'<VAR>n : ℕ∞<VAR>U : Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<VAR>x : M<GOAL>ContMDiffAt I I' n (extend Subtype.val f 1) x
<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>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✝ : ℕ∞<VAR>inst✝¹ : T2Space M<VAR>inst✝ : One M'<VAR>n : ℕ∞<VAR>U : Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<VAR>x✝ x : M<VAR>h : x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContMDiffAt I I' n (extend Subtype.val f 1) x
<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>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✝ : ℕ∞<VAR>inst✝¹ : T2Space M<VAR>inst✝ : One M'<VAR>n : ℕ∞<VAR>U : Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<VAR>x✝ : M<VAR>x : ↥U<VAR>h : ↑x ∈ mulTSupport (extend Subtype.val f 1)<GOAL>ContMDiffAt I I' n (extend Subtype.val f 1) ↑x