ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<VAR>y : E<VAR>hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)<VAR>z : E<VAR>zs : z ∈ s<VAR>hz : r • z = -x + y<VAR>I : ‖r • z‖ ≤ ε<GOAL>y ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this✝ : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<VAR>y : E<VAR>hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)<VAR>z : E<VAR>zs : z ∈ s<VAR>hz : r • z = -x + y<VAR>I : ‖r • z‖ ≤ ε<VAR>this : y = x + r • z<GOAL>y ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>hs : Bornology.IsBounded s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 x<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>hε : closedBall x ε ⊆ u<VAR>R : ℝ<VAR>Rpos : 0 < R<VAR>hR : s ⊆ closedBall 0 R<VAR>this✝ : closedBall 0 (ε / R) ∈ 𝓝 0<VAR>r : 𝕜<VAR>hr : r ∈ closedBall 0 (ε / R)<VAR>y : E<VAR>hy : y ∈ (fun x_1 => -x + x_1) ⁻¹' (r • s)<VAR>z : E<VAR>zs : z ∈ s<VAR>hz : r • z = -x + y<VAR>I : ‖r • z‖ ≤ ε<VAR>this : y = x + r • z<GOAL>y ∈ closedBall x ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>hb : 1 ≤ b<GOAL>b * a ≤ b → a∗ ≤ b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ W X X' Y Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<VAR>h : Y ≅ Z<GOAL>f ≫ g ≫ h.hom = f' ≫ g' ≫ h.hom ↔ f ≫ g = f' ≫ g'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : StrictMonoOn f s<VAR>h₂ : StrictMonoOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x < y<GOAL>f x < f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : StrictMonoOn f s<VAR>h₂ : StrictMonoOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x < y<VAR>hxc : x < c<GOAL>f x < f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : StrictMonoOn f s<VAR>h₂ : StrictMonoOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x < y<VAR>hcx : c ≤ x<GOAL>f x < f y
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>b : ℝ<VAR>a : ℝ≥0<GOAL>↑a < ENNReal.ofReal b ↔ (↑a).toReal < b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a x : G<GOAL>x ∈ ⋃ h, (↑h * a) • ↑K ↔ x ∈ doset a ↑H ↑K
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a x : G<GOAL>(∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>f : V₁ →ₗ[K] V₂<GOAL>Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f
<VAR>x✝ y✝ z x y : ℝ<VAR>hx_nonneg : 0 ≤ x<GOAL>‖x ^ y‖ = ‖x‖ ^ y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : FirstCountableTopology α<VAR>f : Filter β<VAR>inst✝ : CountableInterFilter f<VAR>u : β → α<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<GOAL>∀ᶠ (b : β) in f, u b ≤ limsup u f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : FirstCountableTopology α<VAR>f : Filter β<VAR>inst✝ : CountableInterFilter f<VAR>u : β → α<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>ha : IsTop (limsup u f)<GOAL>∀ᶠ (b : β) in f, u b ≤ limsup u f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : FirstCountableTopology α<VAR>f : Filter β<VAR>inst✝ : CountableInterFilter f<VAR>u : β → α<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>ha : ∃ b, limsup u f < b<GOAL>∀ᶠ (b : β) in f, u b ≤ limsup u f
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>Q : Type v<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>M : Type v<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>inj : Injective R (ULift.{v', v} M)<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>f : X →ₗ[R] Y<VAR>hf : Function.Injective ⇑f<VAR>g : X →ₗ[R] M<VAR>eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv<GOAL>Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX)
<VAR>a✝ x✝ y✝ a x y : ℂ<GOAL>angle (x / a) y = angle x (y * a)
<VAR>a x✝ y✝ x y : ℂ<GOAL>angle (x / 0) y = angle x (y * 0)
<VAR>a✝ x✝ y✝ a x y : ℂ<VAR>ha : a ≠ 0<GOAL>angle (x / a) y = angle x (y * a)
<VAR>k : ℕ<VAR>x : ℝ<GOAL>HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x
<VAR>k : ℕ<VAR>x : ℝ<GOAL>↑k * bernoulliFun (k - 1) x = Polynomial.eval x (Polynomial.derivative (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫_𝕜<GOAL>0 ≤ μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<GOAL>0 ≤ μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<VAR>hpos : 0 < ‖v‖ ^ 2<GOAL>0 ≤ μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>μ : ℝ<VAR>T : E →ₗ[𝕜] E<VAR>hμ : HasEigenvalue T ↑μ<VAR>hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫_𝕜<VAR>v : E<VAR>hv : HasEigenvector T (↑μ) v<VAR>hpos : 0 < ‖v‖ ^ 2<VAR>this : RCLike.re ⟪v, T v⟫_𝕜 = μ * ‖v‖ ^ 2<GOAL>0 ≤ μ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix l m R<VAR>N : Matrix m n R<VAR>x : n → R<GOAL>(toLin' (M * N)) x = (toLin' M) ((toLin' N) x)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>m : M<VAR>hB : ∀ (y : M), (B m) y = 0<GOAL>m = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0<GOAL>v.repr.symm vi = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0<GOAL>vi = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0<VAR>i : n<GOAL>vi i = 0 i
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (y : M), (B (v.repr.symm vi)) y = 0<VAR>i : n<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : (B (v.repr.symm vi)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : (RingHom.id R) (vi i) • (B (v i)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0<GOAL>∀ b ∈ vi.support, b ≠ i → (RingHom.id R) (vi b) • (B (v b)) (v i) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0<GOAL>i ∉ vi.support → (RingHom.id R) (vi i) • (B (v i)) (v i) = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>p : 𝕜[X]<VAR>a : A<GOAL>p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set (Set α)<VAR>hs : s.Finite<VAR>H : ∀ t ∈ s, t.Finite<GOAL>(⋃₀ s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₃<VAR>h₂ : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₃<VAR>h₂ : coinduced f t₁ ≤ t₂<GOAL>coinduced f t₁ ≤ t₃
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : ℝ<VAR>h : y ∈ uIcc x z<GOAL>dist x y ≤ dist x z
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : UniformSpace E<VAR>inst✝¹ : UniformAddGroup E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : TotallyBounded s<GOAL>Bornology.IsVonNBounded 𝕜 s
<VAR>n✝ p i n : ℕ<VAR>h : 2 ≤ p<GOAL>n / p ^ i = ofDigits p (List.drop i (p.digits n))
<VAR>n✝ p i n : ℕ<VAR>h : 2 ≤ p<GOAL>n = ofDigits p (p.digits n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>hb : 1 ≤ b<GOAL>a * b ≤ b → a∗ ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x✝ : α × β<GOAL>x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : μ.IsAddLeftInvariant<VAR>inst✝² : μ.IsNegInvariant<VAR>inst✝¹ : MeasurableNeg G<VAR>inst✝ : MeasurableAdd G<VAR>x : G<GOAL>(g ⋆[L.flip, μ] f) x = (f ⋆[L, μ] g) x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : μ.IsAddLeftInvariant<VAR>inst✝² : μ.IsNegInvariant<VAR>inst✝¹ : MeasurableNeg G<VAR>inst✝ : MeasurableAdd G<VAR>x : G<GOAL>∫ (t : G), (L.flip (g t)) (f (x - t)) ∂μ = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : μ.IsAddLeftInvariant<VAR>inst✝² : μ.IsNegInvariant<VAR>inst✝¹ : MeasurableNeg G<VAR>inst✝ : MeasurableAdd G<VAR>x : G<GOAL>∫ (x_1 : G), (L.flip (g (x - x_1))) (f (x - (x - x_1))) ∂μ = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : SheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑X.toPresheafedSpace<GOAL>op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>l : Filter α<VAR>p : ι → α → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp<VAR>g : GenContFract K := of v<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<GOAL>let g := of v; let B := (g.contsAux (n + 1)).b; let pB := (g.contsAux n).b; v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp<VAR>g : GenContFract K := of v<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr<GOAL>let g := of v; let B := (g.contsAux (n + 1)).b; let pB := (g.contsAux n).b; v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp<VAR>g : GenContFract K := of v<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr<VAR>ifp_fr_eq_zero : ifp.fr = 0<GOAL>let g := of v; let B := (g.contsAux (n + 1)).b; let pB := (g.contsAux n).b; v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>ifp : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp<VAR>g : GenContFract K := of v<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr<VAR>ifp_fr_ne_zero : ifp.fr ≠ 0<GOAL>let g := of v; let B := (g.contsAux (n + 1)).b; let pB := (g.contsAux n).b; v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime x (y + x * z)<GOAL>IsRelPrime x y
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsRelPrime (y + x * z) x<GOAL>IsRelPrime y x
<VAR>z w : ℂ<GOAL>(z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h1 : Antiperiodic f c₁<VAR>h2 : Antiperiodic f c₂<GOAL>Periodic f (c₁ + c₂)
<VAR>a b x y u v : ℕ<VAR>ha : ↑a = ↑x ^ 2 + ↑y ^ 2<VAR>hb : ↑b = ↑u ^ 2 + ↑v ^ 2<GOAL>∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
<VAR>a b x y u v : ℕ<VAR>ha : ↑a = ↑x ^ 2 + ↑y ^ 2<VAR>hb : ↑b = ↑u ^ 2 + ↑v ^ 2<VAR>r s : ℤ<VAR>h : ↑a * ↑b = r ^ 2 + s ^ 2<GOAL>∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
<VAR>a b x y u v : ℕ<VAR>ha : ↑a = ↑x ^ 2 + ↑y ^ 2<VAR>hb : ↑b = ↑u ^ 2 + ↑v ^ 2<VAR>r s : ℤ<VAR>h : ↑a * ↑b = r ^ 2 + s ^ 2<GOAL>↑a * ↑b = ↑r.natAbs ^ 2 + ↑s.natAbs ^ 2
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>iInf f * a = ⨅ i, f i * a
<VAR>ι : Sort u_1<VAR>f✝ f : ι → ℝ≥0<VAR>a : ℝ≥0<GOAL>(⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>v : m → α<GOAL>‖row ι v‖ = ‖(WithLp.equiv 2 (m → α)).symm v‖
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>v : m → α<GOAL>(∑ j : m, ‖row ι v default j‖ ^ 2) ^ (1 / 2) = (∑ i : m, ‖(WithLp.equiv 2 (m → α)).symm v i‖ ^ 2) ^ (1 / 2)