ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>InnerProductGeometry.angle x (x - y) < π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (InnerProductGeometry.angle x (x - y)) = ‖x‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>Real.sin (InnerProductGeometry.angle x (x - y)) = ‖y‖ / ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.tan (InnerProductGeometry.angle x (x - y)) = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (InnerProductGeometry.angle x (x - y)) * ‖x - y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.sin (InnerProductGeometry.angle x (x - y)) * ‖x - y‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>Real.tan (InnerProductGeometry.angle x (x - y)) * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / Real.cos (InnerProductGeometry.angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.sin (InnerProductGeometry.angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.tan (InnerProductGeometry.angle x (x - y)) = ‖x‖
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p1 p2 p3 : P<GOAL>dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ ∠ p1 p2 p3 = π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>0 < ∠ p₂ p₃ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>∠ p₂ p₃ p₁ ≤ π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₃ ≠ p₂<GOAL>∠ p₂ p₃ p₁ < π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂<GOAL>Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<GOAL>Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ = p₂ ∨ p₃ ≠ p₂<GOAL>dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>s : σ<VAR>S : Set σ<VAR>a : α<GOAL>s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>a : α<GOAL>M.stepSet ∅ a = ∅
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>S : Set σ<GOAL>M.evalFrom S [] = S
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>S : Set σ<VAR>a : α<GOAL>M.evalFrom S [a] = M.stepSet S a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>a : α<GOAL>M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<GOAL>M.eval [] = M.start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>a : α<GOAL>M.eval [a] = M.stepSet M.start a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>x : List α<VAR>a : α<GOAL>M.eval (x ++ [a]) = M.stepSet (M.eval x) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>x : List α<GOAL>x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<GOAL>M.toDFA.accepts = M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>Fintype σ<VAR>x : List α<VAR>hx : x ∈ M.accepts<VAR>hlen : Fintype.card (Set σ) ≤ x.length<GOAL>∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ' : Type v<VAR>M : DFA α σ'<VAR>s : σ'<VAR>a : α<GOAL>M.toNFA.step s a = {M.step s a}
<VAR>α : Type u<VAR>σ' : Type v<VAR>M : DFA α σ'<GOAL>M.toNFA.accept = M.accept
<VAR>α : Type u<VAR>σ' : Type v<VAR>M : DFA α σ'<GOAL>M.toNFA.start = {M.start}
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>start : σ<VAR>s : List α<GOAL>M.toNFA.evalFrom {start} s = {M.evalFrom start s}
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<GOAL>M.toNFA.accepts = M.accepts
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : E → E'<VAR>x : E<GOAL>ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<GOAL>ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') n f s ↔ ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : E → E'<GOAL>ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>s : Set M<VAR>t : Set F<VAR>x : M<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x<VAR>h : s ⊆ f ⁻¹' t<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>s : Set M<VAR>x : M<VAR>hg : ContDiffAt 𝕜 n g (f x)<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>x : M<VAR>hg : ContDiffAt 𝕜 n g (f x)<VAR>hf : ContMDiffAt I 𝓘(𝕜, F) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, F') n (g ∘ f) 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>s : Set M<VAR>x : M<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F') n (g ∘ f) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>x : M<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContMDiffAt I 𝓘(𝕜, F) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, F') n (g ∘ f) 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>F' : Type u_11<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>g : F → F'<VAR>f : M → F<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContMDiff I 𝓘(𝕜, F) n f<GOAL>ContMDiff I 𝓘(𝕜, F') n (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] F<GOAL>ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, F) n ⇑L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] F<VAR>x : E<GOAL>ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (⇑L) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] F<VAR>s : Set E<VAR>x : E<GOAL>ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (⇑L) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>L : E →L[𝕜] F<VAR>s : Set E<GOAL>ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, F) n (⇑L) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<GOAL>Smooth 𝓘(𝕜, E) 𝓘(𝕜, F) ⇑L
<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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₁<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₁<VAR>x : M<VAR>hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₁<VAR>s : Set M<VAR>hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f s<GOAL>ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n (fun x => (g x).comp (f x)) s
<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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₁<VAR>hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g<VAR>hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n f<GOAL>ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n fun x => (g x).comp (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F₂) n (fun x => (g x) (f x)) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>x : M<VAR>hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g x<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₁) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, F₂) n (fun x => (g x) (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>s : Set M<VAR>hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₁) n f s<GOAL>ContMDiffOn I 𝓘(𝕜, F₂) n (fun x => (g x) (f x)) s
<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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g<VAR>hf : ContMDiff I 𝓘(𝕜, F₁) n f<GOAL>ContMDiff I 𝓘(𝕜, F₂) n fun x => (g x) (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₁ →L[𝕜] F₂<VAR>s : Set M<VAR>x : M<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.precomp F₃ (f y)) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₁ →L[𝕜] F₂<VAR>x : M<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.precomp F₃ (f y)) 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₁ →L[𝕜] F₂<VAR>s : Set M<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f s<GOAL>ContMDiffOn I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.precomp F₃ (f y)) s
<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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₁ →L[𝕜] F₂<VAR>hf : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₂) n f<GOAL>ContMDiff I 𝓘(𝕜, (F₂ →L[𝕜] F₃) →L[𝕜] F₁ →L[𝕜] F₃) n fun y => ContinuousLinearMap.precomp F₃ (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₂ →L[𝕜] F₃<VAR>s : Set M<VAR>x : M<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.postcomp F₁ (f y)) s 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₂ →L[𝕜] F₃<VAR>x : M<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.postcomp F₁ (f y)) 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₂ →L[𝕜] F₃<VAR>s : Set M<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f s<GOAL>ContMDiffOn I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃) n (fun y => ContinuousLinearMap.postcomp F₁ (f y)) s
<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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>n : ℕ∞<VAR>f : M → F₂ →L[𝕜] F₃<VAR>hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₃) n f<GOAL>ContMDiff I 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃) n fun y => ContinuousLinearMap.postcomp F₁ (f 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>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>f : M → F₁ ≃L[𝕜] F₂<VAR>g : M → F₃ ≃L[𝕜] F₄<VAR>s : Set M<VAR>x : M<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x => ↑(f x).symm) s x<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x => ↑(g x)) s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun y => ↑((f y).arrowCongr (g y))) s x