ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>e_1✝ : α = αᵒᵈ<VAR>x✝ : α<GOAL>x✝ ⋖ a ↔ toDual a ⋖ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>q : PMF (α → β)<VAR>p : PMF α<VAR>b✝ b : β<GOAL>b ∈ (q.seq p).support ↔ b ∈ ⋃ f ∈ q.support, f '' p.support
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<VAR>D : LieDerivation R L L<GOAL>D ∈ (ad R L).range
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<VAR>D : LieDerivation R L L<GOAL>D ∈ ⊤
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>HasSum (fun b => term (b + 1) s) (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>Tendsto (fun N => term_sum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>Tendsto (fun N => 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>Tendsto (fun x => 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>Tendsto (fun x => 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* MvPolynomial σ S<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(bind₂ f) ((monomial d) r) = f r * (monomial d) 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : (map f s).Nonempty<GOAL>(map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : SemilatticeSup α<VAR>s✝ : Finset β<VAR>H : s✝.Nonempty<VAR>f✝ : β → α<VAR>s : Finset γ<VAR>f : γ ↪ β<VAR>g : β → α<VAR>hs : (map f s).Nonempty<GOAL>s.sup ((WithBot.some ∘ g) ∘ ⇑f) = s.sup (WithBot.some ∘ g ∘ ⇑f)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>BddBelow s
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : Nonempty α<VAR>hs : IsCompact ∅<GOAL>BddBelow ∅
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>hne : s.Nonempty<GOAL>BddBelow s
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ ρ a<GOAL>HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ ρ a<VAR>H₁ : HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹) (↑ₐ k - a)<GOAL>HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ ρ a<VAR>H₁ : HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 A) ↑(IsUnit.unit hk)⁻¹) ↑(IsUnit.unit hk)⁻¹) (↑ₐ k - a)<VAR>H₂ : HasDerivAt (fun k => ↑ₐ k - a) 1 k<GOAL>HasDerivAt (resolvent a) (-resolvent a k ^ 2) k
<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>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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h₀ : HasMFDerivAt I I' f x f₀'<VAR>h₁ : HasMFDerivAt I I' f x f₁'<GOAL>f₀' = f₁'
<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>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>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h₀ : HasMFDerivWithinAt I I' f univ x f₀'<VAR>h₁ : HasMFDerivWithinAt I I' f univ x f₁'<GOAL>f₀' = f₁'
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>ha : ContinuousAt f a<GOAL>HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<GOAL>q.partialSum N (∑ i ∈ Finset.Ico 1 N, (p i) fun _j => z) = ∑ i ∈ compPartialSumTarget 0 N N, (q.compAlongComposition p i.snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<GOAL>(∑ n ∈ Finset.range N, ∑ r ∈ Fintype.piFinset fun i => Finset.Ico 1 N, (q n) fun i => (p (r i)) fun _j => z) = ∑ i ∈ compPartialSumTarget 0 N N, (q.compAlongComposition p i.snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<GOAL>(∑ x ∈ (Finset.Ico 0 N).sigma fun n => Fintype.piFinset fun i => Finset.Ico 1 N, (q x.fst) fun i => (p (x.snd i)) fun _j => z) = ∑ i ∈ compPartialSumTarget 0 N N, (q.compAlongComposition p i.snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<GOAL>∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource 0 N N), ((q e.fst) fun i => (p (e.snd i)) fun _j => z) = (q.compAlongComposition p (compChangeOfVariables 0 N N e he).snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 N N<GOAL>((q ⟨k, blocks_fun⟩.fst) fun i => (p (⟨k, blocks_fun⟩.snd i)) fun _j => z) = (q.compAlongComposition p (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd) fun _j => z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 N N<GOAL>∀ (i : ℕ) (him : i < ⟨k, blocks_fun⟩.fst) (hin : i < (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd.length), ((p (⟨k, blocks_fun⟩.snd ⟨i, him⟩)) fun _j => z) = p.applyComposition (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i, hin⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 N N<VAR>i✝ : ℕ<VAR>him✝ : i✝ < ⟨k, blocks_fun⟩.fst<VAR>hin✝ : i✝ < (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd.length<GOAL>((p (⟨k, blocks_fun⟩.snd ⟨i✝, him✝⟩)) fun _j => z) = p.applyComposition (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i✝, hin✝⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H✝ : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H✝<VAR>inst✝ : NormedSpace 𝕜 H✝<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>N : ℕ<VAR>z : E<VAR>k : ℕ<VAR>blocks_fun : Fin k → ℕ<VAR>H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 N N<VAR>i✝ : ℕ<VAR>him✝ : i✝ < ⟨k, blocks_fun⟩.fst<VAR>hin✝ : i✝ < (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd.length<GOAL>((p ((compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd.blocksFun ⟨↑⟨i✝, him✝⟩, ⋯⟩)) fun _j => z) = p.applyComposition (compChangeOfVariables 0 N N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i✝, hin✝⟩
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Semiring T<VAR>g : S →+* T<VAR>p : R[X]<GOAL>∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>s : Submodule R M<GOAL>Module.rank R ↥s ≤ Module.rank R M
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<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>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>s : Submodule R M<GOAL>Module.rank R ↥s ≤ Module.rank R ↥⊤
<VAR>θ ψ : ℝ<GOAL>↑(toIcoMod two_pi_pos ψ θ) = ↑θ
<VAR>θ ψ : ℝ<GOAL>∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k
<VAR>θ ψ : ℝ<GOAL>toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>i j k : ι<GOAL>K.ExactAt i ↔ (K.sc i).Exact
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b c : α<VAR>h : a ≤ c ⊔ b<VAR>hd : Disjoint a c<GOAL>a ≤ b ⊔ c
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁✝ a₂✝ a₃ b b' b₁ b₂ b₃ c c₁ c₂✝ : R<VAR>c₂ k a₁ a₂ : ℕ<GOAL>a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalCommSemiring α<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<VAR>x : n → α<VAR>x✝ : m<GOAL>(x ᵥ* Aᵀ) x✝ = (A *ᵥ x) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>x y : α<GOAL>const x ≤ const y ↔ x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>x y : α<GOAL>const x ≤ const y ↔ x < y ∨ x = y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume<VAR>ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)<GOAL>HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume<VAR>ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) - ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)] fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖<GOAL>HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume<VAR>ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) - ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)] fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖<GOAL>∀ (x : (ℝ × ℝ) × ℝ × ℝ), ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) - ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) = (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) x.1 - (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) x.2 - ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝¹ : FTCFilter a la la'<VAR>inst✝ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume<VAR>ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)<VAR>hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)<VAR>this : (fun t => ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) - ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)] fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖<GOAL>(fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p => p.1 - p.2
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝¹⁰ : Ring K<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K V₁<VAR>inst✝⁵ : AddCommGroup V'<VAR>inst✝⁴ : Module K V'<VAR>inst✝³ : AddCommGroup V''<VAR>inst✝² : Module K V''<VAR>inst✝¹ : AddCommGroup V'₁<VAR>inst✝ : Module K V'₁<VAR>g : V →ₗ[K] V'<VAR>f : V' →ₗ[K] V'₁<GOAL>(f ∘ₗ g).rank ≤ min f.rank g.rank
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Submodule.span S (Set.range ⇑(D R S)) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>⊤ ≤ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : Ω[S⁄R]<GOAL>x ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<GOAL>(ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.restrictScalars S (ideal R S)<GOAL>(ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>(ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>∀ x ∈ Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>∃ (hx : 0 ∈ ideal R S), (ideal R S).toCotangent ⟨0, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x : S ⊗[R] S<VAR>hx : x ∈ ideal R S<VAR>this : x ∈ Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)<GOAL>∀ (x y : S ⊗[R] S), (∃ (hx : x ∈ ideal R S), (ideal R S).toCotangent ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) → (∃ (hx : y ∈ ideal R S), (ideal R S).toCotangent ⟨y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))) → ∃ (hx : x + y ∈ ideal R S), (ideal R S).toCotangent ⟨x + y, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))