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>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : Finite ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>I : Set ι<VAR>h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)<GOAL>UniqueDiffWithinAt 𝕜 (I.pi s) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>x y : Associates α<VAR>a b : α<VAR>h : ⟦a⟧ * ⟦b⟧ = 1<VAR>this : a * b ~ᵤ 1<GOAL>b * a ~ᵤ 1
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>variance (X + Y) ℙ = (∫ (a : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) a) - (∫ (a : Ω), (X + Y) a) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>(∫ (a : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) a) - (∫ (a : Ω), (X + Y) a) ^ 2 = (((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + 2 * ∫ (a : Ω), (X * Y) a) - ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>(∫ (a : Ω), X a ^ 2 + Y a ^ 2 + 2 * (X a * Y a)) - (∫ (a : Ω), X a + Y a) ^ 2 = (((∫ (a : Ω), X a ^ 2) + ∫ (a : Ω), Y a ^ 2) + 2 * ∫ (a : Ω), X a * Y a) - ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable X ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable Y ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable (fun a => X a ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable (fun a => Y a ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable (fun a => X a ^ 2 + Y a ^ 2) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>Integrable (fun a => 2 * (X a * Y a)) ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>∫ (a : Ω), (X * Y) a = (∫ (a : Ω), X a) * ∫ (a : Ω), Y a
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + 2 * ((∫ (a : Ω), X a) * ∫ (a : Ω), Y a) - ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2 = variance X ℙ + variance Y ℙ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X Y : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>hY : Memℒp Y 2 ℙ<VAR>h : IndepFun X Y ℙ<GOAL>((∫ (a : Ω), X a ^ 2) + ∫ (a : Ω), Y a ^ 2) + 2 * ((∫ (a : Ω), X a) * ∫ (a : Ω), Y a) - ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2 = (∫ (a : Ω), X a ^ 2) - (∫ (a : Ω), X a) ^ 2 + ((∫ (a : Ω), Y a ^ 2) - (∫ (a : Ω), Y a) ^ 2)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t x : ℝ<VAR>n : ℕ<GOAL>HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t x : ℝ<VAR>n : ℕ<GOAL>HasDerivAt (fun y => (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t x : ℝ<VAR>n : ℕ<GOAL>HasDerivAt (fun y => (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t x : ℝ<VAR>n : ℕ<GOAL>↑n + 1 = ↑(n + 1)
<VAR>J : Type u<VAR>inst✝³ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s✝ : Set (F.obj i✝)<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>inst✝¹ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝ : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i : J<VAR>x : F.obj i<VAR>s : Set (F.obj i) := {x}<GOAL>∃ a, (fun s => ↑s i) a = x
<VAR>J : Type u<VAR>inst✝³ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s✝ : Set (F.obj i✝)<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>inst✝¹ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝ : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i : J<VAR>x : F.obj i<VAR>s : Set (F.obj i) := {x}<VAR>this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)<GOAL>∃ a, (fun s => ↑s i) a = x
<VAR>J : Type u<VAR>inst✝³ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s✝ : Set (F.obj i✝)<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>inst✝¹ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝ : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i : J<VAR>x : F.obj i<VAR>s : Set (F.obj i) := {x}<VAR>this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)<VAR>sec : (j : J) → (F.toPreimages s).obj j<VAR>h : sec ∈ (F.toPreimages s).sections<GOAL>∃ a, (fun s => ↑s i) a = x
<VAR>J : Type u<VAR>inst✝³ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j k : J<VAR>s✝ : Set (F.obj i✝)<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>inst✝¹ : ∀ (j : J), Nonempty (F.obj j)<VAR>inst✝ : ∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i : J<VAR>x : F.obj i<VAR>s : Set (F.obj i) := {x}<VAR>this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)<VAR>sec : (j : J) → (F.toPreimages s).obj j<VAR>h : sec ∈ (F.toPreimages s).sections<GOAL>(fun s => ↑s i) ⟨fun j => ↑(sec j), ⋯⟩ = x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>hx : ‖x‖ ≤ r<VAR>hy : ‖y‖ ≤ r<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>‖a • x + b • y‖ < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedLinearOrderedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x y z : E<VAR>a b r : ℝ<VAR>hne : x ≠ y<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hx : x ∈ closedBall 0 r<VAR>hy : y ∈ closedBall 0 r<GOAL>a • x + b • y ∈ ball 0 r
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>C : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)<VAR>mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)<VAR>add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)<VAR>a : CliffordAlgebra Q<VAR>s : Subalgebra R (CliffordAlgebra Q) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>C : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)<VAR>mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)<VAR>add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)<VAR>a : CliffordAlgebra Q<VAR>s : Subalgebra R (CliffordAlgebra Q) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } := ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>C : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)<VAR>mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)<VAR>add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)<VAR>a : CliffordAlgebra Q<VAR>s : Subalgebra R (CliffordAlgebra Q) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } := ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩<VAR>of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp ((lift Q) of)<GOAL>C a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>C : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)<VAR>mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)<VAR>add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)<VAR>a : CliffordAlgebra Q<VAR>s : Subalgebra R (CliffordAlgebra Q) := { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }<VAR>h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))<VAR>of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } := ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩<VAR>of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp ((lift Q) of)<GOAL>C ((s.val.comp ((lift Q) of)) a)
<VAR>X : Compactum<VAR>S : Set X.A<GOAL>IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
<VAR>X : Compactum<VAR>S : Set X.A<GOAL>IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{w', w} D<VAR>K : Type z<VAR>inst✝¹ : Category.{z', z} K<VAR>inst✝ : HasLimitsOfShape K D<VAR>F : K ⥤ Sheaf J D<VAR>E : Cone (F ⋙ sheafToPresheaf J D)<VAR>hE : IsLimit E<GOAL>Presheaf.IsSheaf J E.pt
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{w', w} D<VAR>K : Type z<VAR>inst✝¹ : Category.{z', z} K<VAR>inst✝ : HasLimitsOfShape K D<VAR>F : K ⥤ Sheaf J D<VAR>E : Cone (F ⋙ sheafToPresheaf J D)<VAR>hE : IsLimit E<GOAL>∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s t : Set E<GOAL>(convexHull R) (s + t) = (convexHull R) s + (convexHull R) t
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>p₂ : ι₂ → P<VAR>hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j<VAR>he : p '' ↑s = p₂ '' ↑s₂<GOAL>centroid k s p = centroid k s₂ p₂
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f g : C(X, ℝ)<VAR>x : X<GOAL>↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) x) = ↑(((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) x)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>f g : C(X, ℝ)<VAR>x : X<GOAL>max (f x + g x) 0 + (-f x + max (f x) 0) + (-g x + max (g x) 0) = -(f x + g x) + max (f x + g x) 0 + max (f x) 0 + max (g x) 0
<VAR>α β : Type u<GOAL>1 < ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>h : o.bsup f = o.blsub f<VAR>i : Ordinal.{u}<GOAL>∀ (hi : i < o), f i hi < o.blsub f
<VAR>f✝ g f : CircleDeg1Lift<VAR>h : Bijective ⇑f<VAR>x y : ℝ<VAR>hxy : x ≤ y<GOAL>f ((Equiv.ofBijective (⇑f) h).symm x) ≤ f ((Equiv.ofBijective (⇑f) h).symm y)
<VAR>f✝ g f : CircleDeg1Lift<VAR>h : Bijective ⇑f<VAR>x : ℝ<GOAL>f ({ toFun := ⇑(Equiv.ofBijective (⇑f) h).symm, monotone' := ⋯ }.toFun (x + 1)) = f ({ toFun := ⇑(Equiv.ofBijective (⇑f) h).symm, monotone' := ⋯ }.toFun x + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n a✝ : ℕ<GOAL>a✝ ∈ map valEmbedding univ ↔ a✝ ∈ Iio n
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p q : ℚ≥0<GOAL>↑q ≤ 0 ↔ q ≤ 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Injective ⇑f<GOAL>f (ζ ^ k) = f 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Injective ⇑f<GOAL>∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Injective ⇑f<GOAL>∀ (l : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Injective ⇑f<VAR>l : ℕ<VAR>hl : f (ζ ^ l) = f 1<GOAL>orderOf (f ζ) ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>f : F<VAR>h✝ : IsPrimitiveRoot ζ k<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Injective ⇑f<VAR>l : ℕ<VAR>hl : f ζ ^ l = 1<GOAL>orderOf (f ζ) ∣ l
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v✝ : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>v : ι → M<VAR>v' : ι' → M'<VAR>hv : LinearIndependent R v<VAR>hv' : LinearIndependent R v'<GOAL>Disjoint (span R (Set.range (⇑(inl R M M') ∘ v))) (span R (Set.range (⇑(inr R M M') ∘ v')))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Countable ι<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<GOAL>Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Countable ι<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<VAR>h : IsEmpty ι<GOAL>Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Countable ι<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<VAR>h : Nonempty ι<GOAL>Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝² : MetricSpace β<VAR>μ : Measure α<VAR>n✝ : ℕ<VAR>i j : ι<VAR>s : Set α<VAR>ε : ℝ<VAR>f : ι → α → β<VAR>g : α → β<VAR>inst✝¹ : SemilatticeSup ι<VAR>inst✝ : Countable ι<VAR>hf : ∀ (n : ι), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ ⊤<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>n : ℕ<VAR>h : Nonempty ι<GOAL>Tendsto (fun j => μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 (μ (⋂ i, s ∩ notConvergentSeq f g n i)))
<VAR>G : Type u<VAR>inst✝ : Monoid G<GOAL>exponent G = 1 ↔ Subsingleton G
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>eq_one : exponent G = 1<VAR>a b : G<GOAL>a = b
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>h : Subsingleton G<GOAL>exponent G ≤ 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>h : Subsingleton G<GOAL>1 ≤ exponent G
<VAR>θ : ℂ<VAR>hθ : cos θ ≠ 0<GOAL>tan θ = 0 ↔ ∃ k, ↑k * ↑π = θ
<VAR>θ : ℂ<VAR>hθ : cos θ ≠ 0<GOAL>(∃ k, θ = ↑k * ↑π) ∨ False ↔ ∃ k, ↑k * ↑π = θ
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ : Matrix n n R<VAR>M : Matrix n n R[X]<VAR>r : R<GOAL>eval ((scalar n) r) (matPolyEquiv M) = M.map (eval r)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<GOAL>(⨆ i, μ i).trim = ⨆ i, (μ i).trim
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<GOAL>(⨆ i, μ i.down).trim = ⨆ i, (μ i.down).trim
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<GOAL>(⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s t : Set α<VAR>left✝¹ : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : ∀ (i : Option (PLift ι)), (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i) t = (Option.elim' (⨆ i, μ i.down) (μ ∘ PLift.down) i).trim s<GOAL>(⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s t : Set α<VAR>left✝¹ : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s<GOAL>(⨆ i, μ i.down).trim s = (⨆ i, (μ i.down).trim) s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s t : Set α<VAR>left✝¹ : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (⨆ i, μ i.down) t = (⨆ i, μ i.down).trim s ∧ ∀ (x : PLift ι), ((μ ∘ PLift.down) x) t = ((μ ∘ PLift.down) x).trim s<GOAL>⨆ i, (μ i.down) t = ⨆ i, (μ i.down).trim s
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℤ<VAR>hmn : m.natAbs.Coprime n.natAbs<VAR>h : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n]<GOAL>a ≡ b [ZMOD m * n]
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℤ<VAR>hmn : m.natAbs.Coprime n.natAbs<VAR>h : m ∣ b - a ∧ n ∣ b - a<GOAL>a ≡ b [ZMOD m * n]
<VAR>m✝ n✝ a✝ b✝ c d a b m n : ℤ<VAR>hmn : m.natAbs.Coprime n.natAbs<VAR>h : m ∣ b - a ∧ n ∣ b - a<GOAL>m.natAbs * n.natAbs ∣ (b - a).natAbs
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>add' W (L.map 0) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<GOAL>diam {x, y} = dist x y
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R<VAR>n : ℕ<GOAL>(C a * X ^ n).toFinsupp = Finsupp.single n a
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t K : Set X<VAR>l : Filter Y<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l<GOAL>s ∈ 𝓝ˢ K ×ˢ l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ K : Set X<VAR>l : Filter Y<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l<VAR>t t' : Set X<VAR>ht : t ⊆ t'<VAR>hs : s ∈ 𝓝ˢ t' ×ˢ l<GOAL>s ∈ 𝓝ˢ t ×ˢ l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ K : Set X<VAR>l : Filter Y<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l<VAR>t t' : Set X<VAR>ht : s ∈ 𝓝ˢ t ×ˢ l<VAR>ht' : s ∈ 𝓝ˢ t' ×ˢ l<GOAL>s ∈ 𝓝ˢ (t ∪ t') ×ˢ l