ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>w : E<GOAL>stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • (4 • w + (‖w‖ ^ 2 - 4) • v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : w ∈ (Submodule.span ℝ {v})ᗮ<GOAL>stereoInvFunAux v w ∈ Metric.sphere 0 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<GOAL>HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<GOAL>HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (Submodule.span ℝ {v})ᗮ.subtypeL 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<GOAL>ContDiff ℝ ⊤ (stereoInvFunAux v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>↑(stereoInvFun hv w) = (‖w‖ ^ 2 + 4)⁻¹ • (4 • ↑w + (‖w‖ ^ 2 - 4) • v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>stereoInvFun hv w ≠ ⟨v, ⋯⟩
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<GOAL>Continuous (stereoInvFun hv)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(Metric.sphere 0 1)<VAR>hx : ↑x ≠ v<GOAL>stereoInvFun hv (stereoToFun v ↑x) = x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>stereoToFun v ↑(stereoInvFun hv w) = w
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>x : ↑(Metric.sphere 0 1)<GOAL>↑(stereographic hv) x = (2 / (1 - ⟪v, ↑x⟫_ℝ)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<GOAL>(stereographic hv).source = {⟨v, ⋯⟩}ᶜ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<GOAL>(stereographic hv).target = Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : ↑(Metric.sphere 0 1)<GOAL>↑(stereographic ⋯) (-v) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>v : ↑(Metric.sphere 0 1)<GOAL>↑(stereographic ⋯) v = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<GOAL>FiniteDimensional ℝ E
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>v : ↑(Metric.sphere 0 1)<GOAL>(stereographic' n v).source = {v}ᶜ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>v : ↑(Metric.sphere 0 1)<GOAL>(stereographic' n v).target = Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>u v : ↑(Metric.sphere 0 1)<GOAL>u = v ↔ ⟪↑u, ↑v⟫_ℝ = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>v : ↑(Metric.sphere 0 1)<VAR>x : EuclideanSpace ℝ (Fin n)<GOAL>↑(↑(stereographic' n v).symm x) = let U := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr; (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • 4 • ↑(U.symm x) + (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • (‖↑(U.symm x)‖ ^ 2 - 4) • ↑v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<GOAL>ContMDiff 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) ⊤ Subtype.val
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ F H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>m : ℕ∞<VAR>f : M → E<VAR>hf : ContMDiff I 𝓘(ℝ, E) m f<VAR>hf' : ∀ (x : M), f x ∈ Metric.sphere 0 1<GOAL>ContMDiff I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) m (Set.codRestrict f (Metric.sphere 0 1) hf')
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<GOAL>ContMDiff 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) ⊤ fun x => -x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>v : ↑(Metric.sphere 0 1)<GOAL>LinearMap.range (mfderiv 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) Subtype.val v) = (Submodule.span ℝ {↑v})ᗮ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>InnerProductSpace ℝ E<VAR>n : ℕ<VAR>Fact (FiniteDimensional.finrank ℝ E = n + 1)<VAR>v : ↑(Metric.sphere 0 1)<GOAL>Function.Injective ⇑(mfderiv 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) 𝓘(ℝ, E) Subtype.val v)
<GOAL>Fact (FiniteDimensional.finrank ℝ ℂ = 1 + 1)
<GOAL>ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) ⊤ ⇑expMapCircle
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y z : V<VAR>h₁ : ∃ k, k ≠ 1 ∧ x + y = k • (x - y)<VAR>h₂ : ‖z - y‖ = ‖z + y‖<GOAL>‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b p q : P<VAR>hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)<VAR>hq : dist a q = dist b q<GOAL>dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : EuclideanGeometry.Cospherical {a, b, c, d}<VAR>hapb : ∃ k₁, k₁ ≠ 1 ∧ b -ᵥ p = k₁ • (a -ᵥ p)<VAR>hcpd : ∃ k₂, k₂ ≠ 1 ∧ d -ᵥ p = k₂ • (c -ᵥ p)<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : EuclideanGeometry.Cospherical {a, b, c, d}<VAR>hapb : ∠ a p b = π<VAR>hcpd : ∠ c p d = π<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : EuclideanGeometry.Cospherical {a, b, c, d}<VAR>hab : a ≠ b<VAR>hcd : c ≠ d<VAR>hapb : ∠ a p b = 0<VAR>hcpd : ∠ c p d = 0<GOAL>dist a p * dist b p = dist c p * dist d p
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>u v : List (Symbol T N)<GOAL>r.Rewrites u v ↔ ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>w : List (Symbol T g.NT)<GOAL>g.Derives w w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>v w : List (Symbol T g.NT)<VAR>hvw : g.Produces v w<GOAL>g.Derives v w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>u v w : List (Symbol T g.NT)<VAR>huv : g.Derives u v<VAR>hvw : g.Derives v w<GOAL>g.Derives u w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>u v w : List (Symbol T g.NT)<VAR>huv : g.Derives u v<VAR>hvw : g.Produces v w<GOAL>g.Derives u w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>u v w : List (Symbol T g.NT)<VAR>huv : g.Produces u v<VAR>hvw : g.Derives v w<GOAL>g.Derives u w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>u w : List (Symbol T g.NT)<VAR>huw : g.Derives u w<GOAL>u = w ∨ ∃ v, g.Produces u v ∧ g.Derives v w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>u w : List (Symbol T g.NT)<VAR>huw : g.Derives u w<GOAL>u = w ∨ ∃ v, g.Derives u v ∧ g.Produces v w
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>v w : List (Symbol T g.NT)<VAR>hvw : g.Produces v w<VAR>p : List (Symbol T g.NT)<GOAL>g.Produces (p ++ v) (p ++ w)
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>v w : List (Symbol T g.NT)<VAR>hvw : g.Produces v w<VAR>p : List (Symbol T g.NT)<GOAL>g.Produces (v ++ p) (w ++ p)
<VAR>T : Type uT<VAR>N : Type uN<GOAL>Function.Involutive ContextFreeRule.reverse
<VAR>T : Type uT<GOAL>Function.Involutive ContextFreeGrammar.reverse
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>w : List T<GOAL>w ∈ g.reverse.language ↔ w.reverse ∈ g.language
<VAR>T : Type uT<VAR>L : Language T<GOAL>L.IsContextFree → L.reverse.IsContextFree
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>self : LeftInvariantDerivation I G<VAR>g : G<GOAL>(𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑self) = (Derivation.evalAt g) ↑self
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<GOAL>Function.Injective LeftInvariantDerivation.toDerivation
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<GOAL>(↑↑X).toFun = ⇑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<GOAL>Function.Injective DFunLike.coe
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<VAR>h : ∀ (f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯), X f = Y f<GOAL>X = Y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<GOAL>⇑↑X = ⇑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g : G<VAR>X : LeftInvariantDerivation I G<GOAL>(𝒅ₕ ⋯) ((Derivation.evalAt 1) ↑X) = (Derivation.evalAt g) ↑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>X (f + f') = X f + X f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<GOAL>X 0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>X (-f) = -X f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>X (f - f') = X f - X f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>r : 𝕜<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>X (r • f) = r • X f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<VAR>f' : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>X (f * f') = f • X f' + f' • X f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<GOAL>⇑(X + Y) = ⇑X + ⇑Y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<GOAL>⇑0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<GOAL>⇑(-X) = -⇑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<GOAL>⇑(X - Y) = ⇑X - ⇑Y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<GOAL>↑(X + Y) = ↑X + ↑Y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<GOAL>↑0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>r : 𝕜<VAR>X : LeftInvariantDerivation I G<GOAL>⇑(r • X) = r • ⇑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X : LeftInvariantDerivation I G<VAR>k : 𝕜<GOAL>↑(k • X) = k • ↑X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<GOAL>∀ (a : LeftInvariantDerivation I G) (a_1 : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯), (LeftInvariantDerivation.coeFnAddMonoidHom I G) a a_1 = a a_1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g : G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>((LeftInvariantDerivation.evalAt g) X) f = (X f) g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g : G<VAR>X : LeftInvariantDerivation I G<GOAL>(Derivation.evalAt g) ↑X = (LeftInvariantDerivation.evalAt g) X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g : G<VAR>X : LeftInvariantDerivation I G<GOAL>(𝒅ₕ ⋯) ((LeftInvariantDerivation.evalAt 1) X) = (LeftInvariantDerivation.evalAt g) X
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g h : G<VAR>X : LeftInvariantDerivation I G<GOAL>(LeftInvariantDerivation.evalAt (g * h)) X = (𝒅ₕ ⋯) ((LeftInvariantDerivation.evalAt h) X)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>g : G<VAR>X : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>(X f).comp (𝑳 I g) = X (f.comp (𝑳 I g))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<GOAL>⇑⁅X, Y⁆ = ⇑⁅↑X, ↑Y⁆
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>X Y : LeftInvariantDerivation I G<VAR>f : C^⊤⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯<GOAL>⁅X, Y⁆ f = X (Y f) - Y (X f)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x : V<GOAL>(o.rotationAux θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x : V<GOAL>(o.rotation θ) x = θ.cos • x + θ.sin • o.rightAngleRotation x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x : V<GOAL>(o.rotation θ).symm x = θ.cos • x - θ.sin • o.rightAngleRotation x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x : V<VAR>hx : x ≠ 0<GOAL>↑(o.rotation θ).toLinearEquiv = (Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos]
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>LinearEquiv.det (o.rotation θ).toLinearEquiv = 1
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>(o.rotation θ).symm = o.rotation (-θ)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<GOAL>o.rotation 0 = LinearIsometryEquiv.refl ℝ V
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<GOAL>o.rotation ↑π = LinearIsometryEquiv.neg ℝ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>(o.rotation ↑π) x = -x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<GOAL>o.rotation ↑(π / 2) = o.rightAngleRotation
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ₁ θ₂ : Real.Angle<VAR>x : V<GOAL>(o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ₁ θ₂ : Real.Angle<GOAL>(o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.expMapCircle * (o.kahler x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>x : V<GOAL>-(o.rotation θ) x = (o.rotation (↑π + θ)) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>-(o.rotation ↑(-π / 2)) x = (o.rotation ↑(π / 2)) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>-(o.rotation ↑(π / 2)) x = (o.rotation ↑(-π / 2)) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler ((o.rotation θ) x)) y = ↑(-θ).expMapCircle * (o.kahler x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler x) ((o.rotation θ) y) = ↑θ.expMapCircle * (o.kahler x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle ((o.rotation θ) x) y = o.oangle x y - θ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x ((o.rotation θ) y) = o.oangle x y + θ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle ((o.rotation θ) x) x = -θ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x ((o.rotation θ) x) = θ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle ((o.rotation (o.oangle x y)) x) y = 0