ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<VAR>this : (f u - f x) / (u - x) < (f y - f x) / (y - x)<GOAL>f' < slope f x y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<VAR>u : ℝ<VAR>hxu : x < u<VAR>huy : u < y<VAR>hu : u ∈ S<VAR>this : slope f x u < slope f x y<GOAL>f' < slope f x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>Memℒp.toLp ((s.indicator fun x => c) + s.indicator fun x => c') ⋯ = Memℒp.toLp (fun a => s.indicator (fun x => c) a + s.indicator (fun x => c') a) ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>∫ (x : X) in s, ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X) in s, t.indicator (fun x => e) x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>e : E<GOAL>∫ (x : X) in s, t.indicator (fun x => e) x ∂μ = (μ (t ∩ s)).toReal • e
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s t : ↥S<GOAL>Localization.mk r s • mk m t = mk (r • m) (s * t)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>m : M<VAR>s t : ↥S<GOAL>IsLocalization.mk' (Localization S) r s • mk m t = mk (r • m) (s * t)
<VAR>S✝ : Set Ordinal.{u}<VAR>S T : Set Ordinal.{u_1}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>hST : S ⊆ T<VAR>a : Ordinal.{u_1}<GOAL>enumOrd T a ≤ enumOrd S a
<VAR>S✝ : Set Ordinal.{u}<VAR>S T : Set Ordinal.{u_1}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>hST : S ⊆ T<VAR>a : Ordinal.{u_1}<GOAL>∀ (j : Ordinal.{u_1}), (∀ k < j, enumOrd T k ≤ enumOrd S k) → enumOrd T j ≤ enumOrd S j
<VAR>S✝ : Set Ordinal.{u}<VAR>S T : Set Ordinal.{u_1}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>hST : S ⊆ T<VAR>a b : Ordinal.{u_1}<VAR>H : ∀ k < b, enumOrd T k ≤ enumOrd S k<GOAL>enumOrd T b ≤ enumOrd S b
<VAR>S✝ : Set Ordinal.{u}<VAR>S T : Set Ordinal.{u_1}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>hST : S ⊆ T<VAR>a b : Ordinal.{u_1}<VAR>H : ∀ k < b, enumOrd T k ≤ enumOrd S k<GOAL>sInf (T ∩ {b_1 | ∀ c < b, enumOrd T c < b_1}) ≤ enumOrd S b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => x + c) (Ico a b) = Ico (a + c) (b + c)
<VAR>x : ℝ≥0∞<VAR>n : ℕ<GOAL>(x ^ n).log = ↑n * x.log
<VAR>x : ℝ≥0∞<VAR>n : ℕ<VAR>n_zero : n = 0<GOAL>(x ^ n).log = ↑n * x.log
<VAR>x : ℝ≥0∞<VAR>n : ℕ<VAR>n_pos : n > 0<GOAL>(x ^ n).log = ↑n * x.log
<VAR>n : ℕ<VAR>n_pos : n > 0<GOAL>(0 ^ n).log = ↑n * log 0
<VAR>n : ℕ<VAR>n_pos : n > 0<GOAL>(⊤ ^ n).log = ↑n * ⊤.log
<VAR>x : ℝ≥0∞<VAR>n : ℕ<VAR>n_pos : n > 0<VAR>x_real : 0 < x.toReal<GOAL>(x ^ n).log = ↑n * x.log
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).b₂ = φ W.b₂
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>φ W.a₁ ^ 2 + 4 * φ W.a₂ = φ (W.a₁ ^ 2 + 4 * W.a₂)
<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<VAR>s : ℝ≥0∞<GOAL>(r • s).toReal = r • s.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r✝ p q r : ℝ≥0<VAR>s : ℝ≥0∞<GOAL>↑r * s.toReal = r • s.toReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<VAR>h₁ : a = x ⊔ a<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<VAR>h₂ : a < x ⊔ a<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<VAR>h₂ : a < x ⊔ a<VAR>y : γ<VAR>lty : a < y<VAR>ylt : y < x ⊔ a<GOAL>x ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<VAR>h₂ : a < x ⊔ a<VAR>y : γ<VAR>lty : a < y<VAR>ylt : y < x ⊔ a<GOAL>x ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>s t : Set α<VAR>a✝ b✝ : α<VAR>inst✝¹ : SemilatticeSup γ<VAR>inst✝ : DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<VAR>x : γ<VAR>hx : x ∈ lowerBounds (Ioo a b)<VAR>h₂ : a < x ⊔ a<VAR>y : γ<VAR>lty : a < y<VAR>ylt : y < x ⊔ a<VAR>u : γ<VAR>au : a < u<VAR>ub : u < b<GOAL>x ≤ b
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Finite m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>x : R<GOAL>(toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (scalar n) x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c✝ : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →ₛₗ[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖<VAR>x : E<VAR>hx : ¬x = 0<GOAL>‖f x‖ ≤ C * ‖x‖
<VAR>a b c d c' : List Γ'<GOAL>update (elim a b c d) aux c' = elim a b c' d
<VAR>a b c d c' : List Γ'<VAR>x : K'<GOAL>update (elim a b c d) aux c' x = elim a b c' d x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>(a ⊔ b) \ (a ⊓ b) = a ∆ b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : PolishSpace X<VAR>inst✝ : T2Space Y<VAR>s : Set Y<VAR>hs : AnalyticSet s<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>AnalyticSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : PolishSpace X<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>Z : Type<VAR>w✝¹ : TopologicalSpace Z<VAR>w✝ : PolishSpace Z<VAR>g : Z → Y<VAR>hg : Continuous g<VAR>hs : AnalyticSet (range g)<GOAL>AnalyticSet (f ⁻¹' range g)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : PolishSpace X<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>Z : Type<VAR>w✝¹ : TopologicalSpace Z<VAR>w✝ : PolishSpace Z<VAR>g : Z → Y<VAR>hg : Continuous g<VAR>hs : AnalyticSet (range g)<VAR>this : IsClosed {x | f x.1 = g x.2}<GOAL>AnalyticSet (f ⁻¹' range g)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : PolishSpace X<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>Z : Type<VAR>w✝¹ : TopologicalSpace Z<VAR>w✝ : PolishSpace Z<VAR>g : Z → Y<VAR>hg : Continuous g<VAR>hs : AnalyticSet (range g)<VAR>this : IsClosed {x | f x.1 = g x.2}<GOAL>f ⁻¹' range g = Prod.fst '' {x | f x.1 = g x.2}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : PolishSpace X<VAR>inst✝ : T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>Z : Type<VAR>w✝¹ : TopologicalSpace Z<VAR>w✝ : PolishSpace Z<VAR>g : Z → Y<VAR>hg : Continuous g<VAR>hs : AnalyticSet (range g)<VAR>this : IsClosed {x | f x.1 = g x.2}<VAR>x : X<GOAL>x ∈ f ⁻¹' range g ↔ x ∈ Prod.fst '' {x | f x.1 = g x.2}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<GOAL>⁅e, f⁆ = ((killingForm K L) e) f • ↑α'
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<GOAL>⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ LinearMap.ker (killingForm K L)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<GOAL>⁅e, f⁆ - ((killingForm K L) e) f • ↑α' ∈ rootSpace H 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>aux : ∀ (h : ↥H), ⁅h, e⁆ = α h • e<VAR>α' : ↥H := (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)<GOAL>∀ y ∈ rootSpace H (-0), ((killingForm K L) (⁅e, f⁆ - ((killingForm K L) e) f • ↑α')) y = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ : 1 ≠ 0<GOAL>StrictMono fun x => x ^ 1
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<VAR>x✝ : n + 2 ≠ 0<VAR>x y : ℝ≥0∞<VAR>h : x < y<GOAL>(fun x => x ^ (n + 2)) x < (fun x => x ^ (n + 2)) y
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<VAR>x✝ : n + 2 ≠ 0<VAR>x y : ℝ≥0∞<VAR>h : x < y<GOAL>x ^ (n + 1) * x < y ^ (n + 1) * y
<VAR>x y : ℝ<GOAL>cosh (x - y) = cosh x * cosh y - sinh x * sinh 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>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<GOAL>LinearMap.range f = ⊤
<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>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<VAR>v : V₁<VAR>hv : f v ≠ 0<GOAL>LinearMap.range f = ⊤
<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>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<VAR>v : V₁<VAR>hv : f v ≠ 0<GOAL>⊤ ≤ LinearMap.range f
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<GOAL>∀ (a b : α), Setoid.r a b = (a⁻¹ * b ∈ s)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<GOAL>∀ (a b : α), Setoid.r a b ↔ a⁻¹ * b ∈ s
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>y : E i<VAR>l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))<VAR>update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i<GOAL>HasFDerivAt ((fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i) l y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type u_3<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>y : E i<VAR>l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))<VAR>update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i<GOAL>l = 0 + l.comp (ContinuousLinearMap.id 𝕜 (E i))
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>x✝ : x ∈ univ<VAR>this : 0 < 1 + ‖x‖ ^ 2<GOAL>(fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x) x ∈ ball 0 1
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>x✝ : x ∈ univ<VAR>this : 0 < 1 + ‖x‖ ^ 2<GOAL>‖x‖ ^ 2 < 1 + ‖x‖ ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>x✝ : x ∈ univ<GOAL>(fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y) ((fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x) x) = x
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<GOAL>(fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>y : E<VAR>hy : y ∈ ball 0 1<VAR>this : 0 < 1 - ‖y‖ ^ 2<GOAL>(fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x) ((fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y) y) = y
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>ContinuousOn ↑{ toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ } { toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.source
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous fun x => (√(1 + ‖x‖ ^ 2))⁻¹
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>Continuous fun x => √(1 + ‖x‖ ^ 2)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>ContinuousOn { toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.invFun { toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.target
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>this : ∀ y ∈ ball 0 1, √(1 - ‖y‖ ^ 2) ≠ 0<GOAL>ContinuousOn { toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.invFun { toFun := fun x => (√(1 + ‖x‖ ^ 2))⁻¹ • x, invFun := fun y => (√(1 - ‖y‖ ^ 2))⁻¹ • y, source := univ, target := ball 0 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.target
<VAR>x y : ℝ<GOAL>Real.one.cauchy = 1
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ✝<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f'✝ : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → γ → δ'<VAR>g' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b<GOAL>image2 f (image2 g ↑s ↑t) ↑u = image2 g' (image2 f' ↑s ↑u) ↑t
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ : ?m.346325<VAR>F₂ : BilinForm R M<VAR>f : Module.End R₁ M₁<GOAL>f ∈ B₁.skewAdjointSubmodule ↔ B₁.IsSkewAdjoint f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ : ?m.346325<VAR>F₂ : BilinForm R M<VAR>f : Module.End R₁ M₁<GOAL>f ∈ B₁.skewAdjointSubmodule ↔ (-B₁).IsAdjointPair B₁ f f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((Scheme.ΓSpecIso Γ(X, U)).inv f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>(Spec Γ(X, U)).basicOpen (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) f) = (Spec Γ(X, U)).basicOpen ((Scheme.ΓSpecIso Γ(X, U)).inv f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>s' : Set α<VAR>hf : UniformCauchySeqOn F p s<VAR>hss' : s' ⊆ s<GOAL>UniformCauchySeqOn F p s'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>s' : Set α<VAR>hf : UniformCauchySeqOnFilter F p (𝓟 s)<VAR>hss' : s' ⊆ s<GOAL>UniformCauchySeqOnFilter F p (𝓟 s')
<VAR>n : ℤ<GOAL>(-1) ^ (-n) = (-1) ^ n
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<GOAL>∃ n ω, ω.length = n ∧ cs.wordProd ω = w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>∃ n ω_1, ω_1.length = n ∧ cs.wordProd ω_1 = cs.wordProd ω
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hβ : β.IsNonZero<VAR>k : K<VAR>h : ⇑β = k • ⇑α<VAR>hα : ¬α.IsZero<GOAL>β = -α ∨ β = α