ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContinuousOn (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)) (↑I '' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>x : H := ↑I.symm 0<VAR>y : H' := ↑I'.symm 0<GOAL>ContinuousOn (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)) (↑I '' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>x : H := ↑I.symm 0<VAR>y : H' := ↑I'.symm 0<VAR>A : ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<GOAL>ContinuousOn (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)) (↑I '' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>x : H := ↑I.symm 0<VAR>y : H' := ↑I'.symm 0<VAR>A : ContDiffOn 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)<GOAL>ContinuousOn (fderivWithin 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)) (↑I.symm ⁻¹' s ∩ range ↑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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>x : H := ↑I.symm 0<VAR>y : H' := ↑I'.symm 0<VAR>A : ContDiffOn 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)<GOAL>UniqueDiffOn 𝕜 (↑I.symm ⁻¹' s ∩ range ↑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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝⁶ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝⁵ : TopologicalSpace N'<VAR>inst✝⁴ : ChartedSpace G' N'<VAR>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : H → H'<VAR>s : Set H<VAR>hf : ContinuousOn f s ∧ ∀ (x : H) (y : H'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hn : 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>x : H := ↑I.symm 0<VAR>y : H' := ↑I'.symm 0<VAR>A : ContDiffOn 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I)<GOAL>↑I.symm ⁻¹' s ∩ range ↑I = (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx : x ≠ 1<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
<VAR>α : Type u<VAR>inst✝ : DivisionRing α<VAR>x : α<VAR>hx : x ≠ 1<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(x ^ n - x ^ m) / (x - 1) = (x ^ m - x ^ n) / (1 - x)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>B : Set X<VAR>hfB : IsBlock G B<GOAL>IsBlock (↥H) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>B : Set X<VAR>hfB : IsBlock G B<GOAL>∀ (g : ↥H), g • B = B ∨ Disjoint (g • B) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>H : Subgroup G<VAR>B : Set X<VAR>hfB : IsBlock G B<VAR>g : G<VAR>property✝ : g ∈ H<GOAL>⟨g, property✝⟩ • B = B ∨ Disjoint (⟨g, property✝⟩ • B) B
<VAR>a b c d m n✝ k : ℕ<VAR>p q P Q : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y<GOAL>colimitSMulAux F r x = colimitSMulAux F r y
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y<GOAL>∃ k f g, (F.map f) ⟨x.fst, r • x.snd⟩.snd = (F.map g) ⟨y.fst, r • y.snd⟩.snd
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd<GOAL>∃ k f g, (F.map f) ⟨x.fst, r • x.snd⟩.snd = (F.map g) ⟨y.fst, r • y.snd⟩.snd
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F ⋙ forget (ModuleCat R)).map f x.snd = (F ⋙ forget (ModuleCat R)).map g y.snd<GOAL>(F.map f) ⟨x.fst, r • x.snd⟩.snd = (F.map g) ⟨y.fst, r • y.snd⟩.snd
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<VAR>hfg : (F.map f) x.snd = (F.map g) y.snd<GOAL>(F.map f) ⟨x.fst, r • x.snd⟩.snd = (F.map g) ⟨y.fst, r • y.snd⟩.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<GOAL>μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>(μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = μ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>m : ℝ≥0<VAR>hm : ↑m = μ i<GOAL>(μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯) i = ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>i : Set α<VAR>hi : MeasurableSet i<VAR>m : ℝ≥0<VAR>hm : ↑m = μ i<GOAL>⟨↑μ.toSignedMeasure (univ ∩ i), ⋯⟩ = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>inst✝¹ : Fintype ↑s<VAR>inst✝ : Fintype ↑t<GOAL>Disjoint s.toFinset t.toFinset ↔ Disjoint s t
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<GOAL>HasIntegral I GP (fun x => ∑ i : Fin (n + 1), (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume (∑ i : Fin (n + 1), (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>x✝ : i ∈ Finset.univ<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>i : Fin (n + 1)<VAR>x✝ : i ∈ Finset.univ<VAR>Hd : ∀ x ∈ Box.Icc I \ s, ∀ (i : Fin (n + 1)), HasFDerivWithinAt (fun x => f x i) ((ContinuousLinearMap.proj i).comp (f' x)) (Box.Icc I) x<VAR>Hs : ∀ x ∈ s, ∀ (i : Fin (n + 1)), ContinuousWithinAt (fun y => f y i) (Box.Icc I) x<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1) i) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>kreplace a b l = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>∀ a_1 ∈ l, (if a = a_1.fst then some ⟨a, b⟩ else none) = Option.guard (fun s => a = s.fst) a_1
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<VAR>h : ⟨a, b⟩ ∈ l<GOAL>∀ (a_1 b : Sigma β), b ∈ Option.guard (fun s => a = s.fst) a_1 → a_1 = b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>nH : H.Normal<VAR>n : G<VAR>hn : n ∈ H<VAR>g : G<GOAL>g⁻¹ * n * g ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>nH : H.Normal<VAR>n : G<VAR>hn : n ∈ H<VAR>g : G<GOAL>g = g⁻¹⁻¹
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>z < 0 ↔ ∃ x < 0, ↑x = z
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>re z < 0 ∧ im z = 0 ↔ ∃ x < 0, re ↑x = re z ∧ im ↑x = im z
<VAR>step s m n : Nat<VAR>h : range' s m step <+ range' s n step<GOAL>m ≤ n
<VAR>step s m n : Nat<VAR>h : m ≤ n<GOAL>range' s m step <+ range' s n step
<VAR>step s m n : Nat<VAR>h : m ≤ n<GOAL>range' s m step <+ range' s m step ++ range' (s + step * m) (n - m) step
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<GOAL>projRight (prod q₁ q₂) = q₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<VAR>a✝ : Path a₁ a₂<VAR>b✝ : Path b₁ b₂<GOAL>projRight (prod ⟦a✝⟧ ⟦b✝⟧) = ⟦b✝⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a₁ a₂ a₃ : α<VAR>b₁ b₂ b₃ : β<VAR>p₁ p₁' : Path a₁ a₂<VAR>p₂ p₂' : Path b₁ b₂<VAR>q₁ : Homotopic.Quotient a₁ a₂<VAR>q₂ : Homotopic.Quotient b₁ b₂<VAR>r₁ : Homotopic.Quotient a₂ a₃<VAR>r₂ : Homotopic.Quotient b₂ b₃<VAR>c₁ c₂ : α × β<VAR>a✝ : Path a₁ a₂<VAR>b✝ : Path b₁ b₂<GOAL>⟦(a✝.prod b✝).map ⋯⟧ = ⟦b✝⟧
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<GOAL>eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<GOAL>eval (x + y) (3 - ↑1) = 1 + 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<GOAL>eval (x + y) (dickson 1 1 1) = x ^ 1 + y ^ 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<VAR>n : ℕ<GOAL>eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<VAR>n : ℕ<GOAL>(x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a x y : R<VAR>h : x * y = 1<VAR>n : ℕ<GOAL>x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁶ : NormedField 𝕜<VAR>inst✝²⁵ : SeminormedAddCommGroup V<VAR>inst✝²⁴ : NormedSpace 𝕜 V<VAR>inst✝²³ : PseudoMetricSpace P<VAR>inst✝²² : NormedAddTorsor V P<VAR>inst✝²¹ : SeminormedAddCommGroup V₁<VAR>inst✝²⁰ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁹ : PseudoMetricSpace P₁<VAR>inst✝¹⁸ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁷ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁶ : NormedSpace 𝕜 V₁'<VAR>inst✝¹⁵ : MetricSpace P₁'<VAR>inst✝¹⁴ : NormedAddTorsor V₁' P₁'<VAR>inst✝¹³ : SeminormedAddCommGroup V₂<VAR>inst✝¹² : NormedSpace 𝕜 V₂<VAR>inst✝¹¹ : PseudoMetricSpace P₂<VAR>inst✝¹⁰ : NormedAddTorsor V₂ P₂<VAR>inst✝⁹ : SeminormedAddCommGroup V₃<VAR>inst✝⁸ : NormedSpace 𝕜 V₃<VAR>inst✝⁷ : PseudoMetricSpace P₃<VAR>inst✝⁶ : NormedAddTorsor V₃ P₃<VAR>inst✝⁵ : SeminormedAddCommGroup V₄<VAR>inst✝⁴ : NormedSpace 𝕜 V₄<VAR>inst✝³ : PseudoMetricSpace P₄<VAR>inst✝² : NormedAddTorsor V₄ P₄<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : NormedSpace ℝ V<VAR>x y : P<GOAL>dist ((pointReflection ℝ x) y) y = 2 * dist x y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommSemiring R<VAR>f✝ : α → R<VAR>s✝ s : Finset α<VAR>f : α → R<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * ∏ i ∈ s, f i ^ k i
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommSemiring R<VAR>f✝ : α → R<VAR>s✝ s : Finset α<VAR>f : α → R<VAR>n : ℕ<GOAL>(∑ i ∈ s, f i) ^ n = ∑ x ∈ s.piAntidiag n, ↑(multinomial s x) * s.noncommProd (fun i => f i ^ x i) ⋯
<VAR>R : Type u_1<VAR>inst✝¹² : Semiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>N' : Type u_6<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<VAR>v : ι → M<GOAL>(alternatization m) v = ∑ σ : Perm ι, Perm.sign σ • (domDomCongr σ m) v