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>F : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁷ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜₂ G'<VAR>inst✝⁴ : NormedSpace 𝕜' G'<VAR>inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x x' : M<VAR>y : F<GOAL>(f (x + x')) y = (f x) y + (f x') y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, o.rightAngleRotationAux₁ y⟫_ℝ = -(o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotationAux₁ y, x⟫_ℝ = -(o.areaForm x) y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>r : RegularSpace X<VAR>inst✝ : LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<GOAL>_root_.HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>r : RegularSpace X<VAR>inst✝ : LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<VAR>empty_X : IsEmpty X<GOAL>_root_.HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>r : RegularSpace X<VAR>inst✝ : LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<VAR>nonempty_X : Nonempty X<GOAL>_root_.HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>r : RegularSpace X<VAR>inst✝ : LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<VAR>nonempty_X : Nonempty X<VAR>u : X → Set X<VAR>u_open : ∀ (a : X), IsOpen (u a)<VAR>u_dis : ∀ (a : X), Disjoint (closure (u a)) t<VAR>u_nhd : ∀ a ∈ s, a ∈ u a<GOAL>_root_.HasSeparatingCover s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ s t : Set X<VAR>r : RegularSpace X<VAR>inst✝ : LindelofSpace X<VAR>s_cl : IsClosed s<VAR>t_cl : IsClosed t<VAR>st_dis : Disjoint s t<VAR>nonempty_X : Nonempty X<VAR>u : X → Set X<VAR>u_open : ∀ (a : X), IsOpen (u a)<VAR>u_dis : ∀ (a : X), Disjoint (closure (u a)) t<VAR>u_nhd : ∀ a ∈ s, a ∈ u a<VAR>f : ℕ → X<VAR>f_cov : s ⊆ ⋃ n, u (f n)<GOAL>_root_.HasSeparatingCover s t
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<GOAL>p I
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_ind : ∀ J ≤ I, (∀ (s : Set ι), p (J.splitCenterBox s)) → p J<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>H_ind : ∀ J ≤ I, ¬p J → ¬∀ (s : Set ι), p (J.splitCenterBox s)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>H_ind : ∀ J ≤ I, ¬p J → ∃ x, ¬p (J.splitCenterBox x)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>s : Box ι → Set ι<VAR>hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))<VAR>J : ℕ → Box ι := fun m => (fun J => J.splitCenterBox (s J))^[m] I<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>s : Box ι → Set ι<VAR>hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))<VAR>J : ℕ → Box ι := fun m => (fun J => J.splitCenterBox (s J))^[m] I<VAR>J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>s : Box ι → Set ι<VAR>hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))<VAR>J : ℕ → Box ι := fun m => (fun J => J.splitCenterBox (s J))^[m] I<VAR>J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))<VAR>hJmono : Antitone J<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>hpI : ¬p I<VAR>s : Box ι → Set ι<VAR>hs : ∀ J ≤ I, ¬p J → ¬p (J.splitCenterBox (s J))<VAR>J : ℕ → Box ι := fun m => (fun J => J.splitCenterBox (s J))^[m] I<VAR>J_succ : ∀ (m : ℕ), J (m + 1) = (J m).splitCenterBox (s (J m))<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)<VAR>hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)<VAR>hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)<VAR>hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)<VAR>U : Set (ι → ℝ)<VAR>hUz : U ∈ 𝓝[Box.Icc I] z<VAR>hU : ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<GOAL>False
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>p : Box ι → Prop<VAR>I : Box ι<VAR>H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>J : ℕ → Box ι<VAR>hJmono : Antitone J<VAR>hJle : ∀ (m : ℕ), J m ≤ I<VAR>hJp : ∀ (m : ℕ), ¬p (J m)<VAR>hJsub : ∀ (m : ℕ) (i : ι), (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m<VAR>h0 : J 0 = I<VAR>z : ι → ℝ := ⨆ m, (J m).lower<VAR>hzJ : ∀ (m : ℕ), z ∈ Box.Icc (J m)<VAR>hJl_mem : ∀ (m : ℕ), (J m).lower ∈ Box.Icc I<VAR>hJu_mem : ∀ (m : ℕ), (J m).upper ∈ Box.Icc I<VAR>hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)<VAR>hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)<VAR>U : Set (ι → ℝ)<VAR>hUz : U ∈ 𝓝[Box.Icc I] z<VAR>hU : ∀ J ≤ I, ∀ (m : ℕ), z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J<VAR>m : ℕ<VAR>hUm : Set.Icc (J m).lower (J m).upper ∈ 𝒫 U<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<GOAL>(comap f K).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<VAR>J : Ideal R<VAR>hJ : comap f K < J<GOAL>J = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<VAR>J : Ideal R<VAR>hJ : comap f K < J<GOAL>map f J = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<VAR>J : Ideal R<VAR>hJ : comap f K < J<VAR>h : K = map f J<GOAL>comap f (map f J) = J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<VAR>H : K.IsMaximal<VAR>J : Ideal R<VAR>hJ : comap f K < J<VAR>h : K = map f J<GOAL>comap f ⊥ ≤ J
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanHom n B C g<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map (g ∘ f) s).prod = (map (g ∘ f) t).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanHom n B C g<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map g (map f s)).prod = (map g (map f t)).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanHom n B C g<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>∀ ⦃x : β⦄, x ∈ map f s → x ∈ B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hg : IsMulFreimanHom n B C g<VAR>hf : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝¹⁹ : Field F<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : Algebra F K<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>inst✝¹⁶ : Field F<VAR>inst✝¹⁵ : Field K₁<VAR>inst✝¹⁴ : Field K₂<VAR>inst✝¹³ : Field K₃<VAR>inst✝¹² : Algebra F K₁<VAR>inst✝¹¹ : Algebra F K₂<VAR>inst✝¹⁰ : Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E✝ : Type u_6<VAR>inst✝⁹ : Field E✝<VAR>inst✝⁸ : Algebra F E✝<VAR>inst✝⁷ : Algebra E✝ K₁<VAR>inst✝⁶ : Algebra E✝ K₂<VAR>inst✝⁵ : Algebra E✝ K₃<VAR>inst✝⁴ : IsScalarTower F E✝ K₁<VAR>inst✝³ : IsScalarTower F E✝ K₂<VAR>inst✝² : IsScalarTower F E✝ K₃<VAR>inst✝¹ : Algebra F K<VAR>E : IntermediateField F K<VAR>inst✝ : Normal F ↥E<VAR>f : ↥E →ₐ[F] K<VAR>this : Algebra ↥E ↥E := Algebra.id ↥E<VAR>g : ↥E ≃ₐ[F] ↥E := f.restrictNormal' ↥E<GOAL>f.fieldRange = E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → ℝ≥0<VAR>hf : Summable fun i => ↑(f i)<VAR>g : β → ℝ≥0<VAR>hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b<GOAL>Summable fun i => ↑(g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : β → ℝ≥0<VAR>hf : Summable f<VAR>g : β → ℝ≥0<VAR>hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b<GOAL>Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>{x | l.formPerm x ≠ x} = ↑l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>{x | l.formPerm x ≠ x} ≤ ↑l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>h' : ∀ (x : α), l ≠ [x]<GOAL>↑l.toFinset ≤ {x | l.formPerm x ≠ x}
<VAR>α : Type u_1<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : Fintype α<VAR>p : PMF α<VAR>f : α → E<GOAL>∫ (a : α), f a ∂p.toMeasure = ∑ a : α, (p a).toReal • f a
<VAR>α : Type u_1<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : Fintype α<VAR>p : PMF α<VAR>f : α → E<GOAL>∑ x : α, (p.toMeasure {x}).toReal • f x = ∑ a : α, (p a).toReal • f a
<VAR>α : Type u_1<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSingletonClass α<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : Fintype α<VAR>p : PMF α<VAR>f : α → E<VAR>x : α<GOAL>p.toMeasure {x} = p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>mabs a / a = a⁻ᵐ ^ 2
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<GOAL>c * ⨆ i, f i = ⨆ i, c * f i
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>c : Cardinal.{v}<GOAL>⨆ i, f i * c = ⨆ i, c * f i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>f : (i : ι) → β i<VAR>support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<VAR>s : Multiset ι<VAR>hf : ∀ (i : ι), i ∈ s ∨ f i = 0<GOAL>∑ i ∈ (↑⟨s, hf⟩).toFinset, (φ i) ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i) = ∑ i ∈ Finset.filter (fun i => { toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i ≠ 0) (↑⟨s, hf⟩).toFinset, (fun x => ⇑(φ x)) i ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>f : (i : ι) → β i<VAR>support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<VAR>s : Multiset ι<VAR>hf : ∀ (i : ι), i ∈ s ∨ f i = 0<GOAL>∀ x ∈ (↑⟨s, hf⟩).toFinset, (φ x) ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } x) = if { toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } x ≠ 0 then (fun x => ⇑(φ x)) x ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } x) else 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>f : (i : ι) → β i<VAR>support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<VAR>s : Multiset ι<VAR>hf : ∀ (i : ι), i ∈ s ∨ f i = 0<VAR>i : ι<VAR>a✝ : i ∈ (↑⟨s, hf⟩).toFinset<GOAL>(φ i) ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i) = if { toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i ≠ 0 then (fun x => ⇑(φ x)) i ({ toFun := f, support' := Quot.mk Setoid.r ⟨s, hf⟩ } i) else 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>f : (i : ι) → β i<VAR>support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<VAR>s : Multiset ι<VAR>hf : ∀ (i : ι), i ∈ s ∨ f i = 0<VAR>i : ι<VAR>a✝ : i ∈ s.toFinset<GOAL>(φ i) (f i) = if f i ≠ 0 then (φ i) (f i) else 0
<VAR>n k : ℕ<VAR>x✝ : 2 ≤ k + 2<GOAL>(n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)
<VAR>n k : ℕ<VAR>x✝ : 2 ≤ k + 2<GOAL>(n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (ContinuousMap.id X)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>((h₁.invFun.comp h₂.invFun).comp (h₂.toFun.comp h₁.toFun)).Homotopic (h₁.invFun.comp h₁.toFun)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>h₁ : X ≃ₕ Y<VAR>h₂ : Y ≃ₕ Z<GOAL>((h₂.toFun.comp h₁.toFun).comp (h₁.invFun.comp h₂.invFun)).Homotopic (ContinuousMap.id Z)