ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>I J J₁ : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>Hle : π₁ ≤ π₂<GOAL>π₁.restrict J ≤ π₂.restrict J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<GOAL>Monotone fun π => π.restrict J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : I ≤ J<GOAL>(π.restrict J).boxes = π.boxes
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.restrict I = π
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>(π.restrict J).iUnion = ↑J ∩ π.iUnion
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hJ : J ∈ π<GOAL>(π.biUnion πi).restrict J = πi J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>π' : BoxIntegral.Prepartition I<GOAL>π.biUnion πi ≤ π' ↔ ∀ J ∈ π, πi J ≤ π'.restrict J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>π' : BoxIntegral.Prepartition I<GOAL>π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<GOAL>π₁ ⊓ π₂ = π₁.biUnion fun J => π₂.restrict J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<GOAL>J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, ↑J = ↑J₁ ⊓ ↑J₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<GOAL>(π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter p).boxes = Finset.filter p π.boxes
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>J ∈ π.filter p ↔ J ∈ π ∧ p J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>π.filter p ≤ π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>p : BoxIntegral.Box ι → Prop<VAR>hp : ∀ J ∈ π, p J<GOAL>π.filter p = π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>(π.filter fun x => True) = π
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>α : Type u_2<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>π : BoxIntegral.Prepartition I<VAR>f : BoxIntegral.Box ι → α<VAR>g : BoxIntegral.Box ι → M<GOAL>∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J = ∑ J ∈ π.boxes, g J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>H : Disjoint π₁.iUnion π₂.iUnion<GOAL>J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>f : BoxIntegral.Box ι → M<GOAL>∑ J ∈ π₁.boxes ∪ π₂.boxes, f J = ∑ J ∈ π₁.boxes, f J + ∑ J ∈ π₂.boxes, f J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>Fintype ι<VAR>h : J ∈ π<GOAL>J.distortion ≤ π.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>Fintype ι<VAR>c : ℝ≥0<GOAL>π.distortion ≤ c ↔ ∀ J ∈ π, J.distortion ≤ c
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnion πi).distortion = π.boxes.sup fun J => (πi J).distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>Fintype ι<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>Fintype ι<VAR>c : ℝ≥0<VAR>h₁ : π.boxes.Nonempty<VAR>h₂ : ∀ J ∈ π, J.distortion = c<GOAL>π.distortion = c
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<GOAL>⊤.distortion = I.distortion
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<GOAL>⊥.distortion = 0
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<GOAL>π.IsPartition ↔ π.iUnion = ↑I
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>h : J ≤ I<GOAL>(BoxIntegral.Prepartition.single I J h).IsPartition ↔ J = I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<GOAL>⊤.IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<GOAL>π.iUnion = ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<VAR>π₁ : BoxIntegral.Prepartition I<GOAL>π₁.iUnion ⊆ π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>x : ι → ℝ<VAR>h : π.IsPartition<VAR>hx : x ∈ I<GOAL>∃! J, J ∈ π ∧ x ∈ J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<GOAL>π.boxes.Nonempty
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₁.boxes ⊆ π₂.boxes<GOAL>π₁ = π₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₂.IsPartition<GOAL>π₁ ≤ π₂ ↔ ∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J'
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>h : π.IsPartition<VAR>hi : ∀ J ∈ π, (πi J).IsPartition<GOAL>(π.biUnion πi).IsPartition
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>h : π.IsPartition<VAR>hJ : J ≤ I<GOAL>(π.restrict J).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₂.IsPartition<GOAL>(π₁ ⊓ π₂).IsPartition
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>h : ∀ J ∈ π, (πi J).IsPartition<GOAL>(π.biUnion πi).iUnion = π.iUnion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.Prepartition I<VAR>h : π₂.iUnion = ↑I \ π₁.iUnion<GOAL>(π₁.disjUnion π₂ ⋯).IsPartition
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>p x : E × E<GOAL>(fderivInnerCLM 𝕜 p) x = ⟪p.1, x.2⟫_𝕜 + ⟪x.1, p.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>n : ℕ∞<GOAL>ContDiff ℝ n fun p => ⟪p.1, p.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>p : E × E<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n (fun p => ⟪p.1, p.2⟫_𝕜) p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<GOAL>Differentiable ℝ fun p => ⟪p.1, p.2⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hg : ContDiffWithinAt ℝ n g s x<GOAL>ContDiffWithinAt ℝ n (fun x => ⟪f x, g x⟫_𝕜) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>hg : ContDiffAt ℝ n g x<GOAL>ContDiffAt ℝ n (fun x => ⟪f x, g x⟫_𝕜) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>hg : ContDiffOn ℝ n g s<GOAL>ContDiffOn ℝ n (fun x => ⟪f x, g x⟫_𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<GOAL>ContDiff ℝ n fun x => ⟪f x, g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>s : Set G<VAR>x : G<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<GOAL>HasFDerivWithinAt (fun t => ⟪f t, g t⟫_𝕜) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>x : G<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<GOAL>HasStrictFDerivAt (fun t => ⟪f t, g t⟫_𝕜) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>f' g' : G →L[ℝ] E<VAR>x : G<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<GOAL>HasFDerivAt (fun t => ⟪f t, g t⟫_𝕜) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>f' g' : E<VAR>s : Set ℝ<VAR>x : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<GOAL>HasDerivWithinAt (fun t => ⟪f t, g t⟫_𝕜) (⟪f x, g'⟫_𝕜 + ⟪f', g x⟫_𝕜) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>f' g' : E<VAR>x : ℝ<GOAL>HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun t => ⟪f t, g t⟫_𝕜) (⟪f x, g'⟫_𝕜 + ⟪f', g x⟫_𝕜) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>x : G<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hg : DifferentiableWithinAt ℝ g s x<GOAL>DifferentiableWithinAt ℝ (fun x => ⟪f x, g x⟫_𝕜) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>x : G<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<GOAL>DifferentiableAt ℝ (fun x => ⟪f x, g x⟫_𝕜) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>hf : DifferentiableOn ℝ f s<VAR>hg : DifferentiableOn ℝ g s<GOAL>DifferentiableOn ℝ (fun x => ⟪f x, g x⟫_𝕜) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<GOAL>Differentiable ℝ fun x => ⟪f x, g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>x : G<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>y : G<GOAL>(fderiv ℝ (fun t => ⟪f t, g t⟫_𝕜) x) y = ⟪f x, (fderiv ℝ g x) y⟫_𝕜 + ⟪(fderiv ℝ f x) y, g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>x : ℝ<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<GOAL>deriv (fun t => ⟪f t, g t⟫_𝕜) x = ⟪f x, deriv g x⟫_𝕜 + ⟪deriv f x, g x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>n : ℕ∞<GOAL>ContDiff ℝ n fun x => ‖x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => ‖f x‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun y => ‖f y‖ ^ 2) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => ‖f x‖ ^ 2) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>n : ℕ∞<VAR>x : E<VAR>hx : x ≠ 0<GOAL>ContDiffAt ℝ n norm x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>h0 : f x ≠ 0<GOAL>ContDiffAt ℝ n (fun y => ‖f y‖) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>hg : ContDiffAt ℝ n g x<VAR>hne : f x ≠ g x<GOAL>ContDiffAt ℝ n (fun y => dist (f y) (g y)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>h0 : f x ≠ 0<GOAL>ContDiffWithinAt ℝ n (fun y => ‖f y‖) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>x : G<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hg : ContDiffWithinAt ℝ n g s x<VAR>hne : f x ≠ g x<GOAL>ContDiffWithinAt ℝ n (fun y => dist (f y) (g y)) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun y => ‖f y‖ ^ 2) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>h0 : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn ℝ n (fun y => ‖f y‖) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>hg : ContDiffOn ℝ n g s<VAR>hne : ∀ x ∈ s, f x ≠ g x<GOAL>ContDiffOn ℝ n (fun y => dist (f y) (g y)) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>h0 : ∀ (x : G), f x ≠ 0<GOAL>ContDiff ℝ n fun y => ‖f y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>hne : ∀ (x : G), f x ≠ g x<GOAL>ContDiff ℝ n fun y => dist (f y) (g y)
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>x : F<GOAL>HasStrictFDerivAt (fun x => ‖x‖ ^ 2) (2 • (innerSL ℝ) x) x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>x : G<VAR>f : G → F<VAR>f' : G →L[ℝ] F<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => ‖f x‖ ^ 2) (2 • ((innerSL ℝ) (f x)).comp f') x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : ℝ → F<VAR>f' : F<VAR>x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => ‖f x‖ ^ 2) (2 * ⟪f x, f'⟫_ℝ) x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>s : Set G<VAR>x : G<VAR>f : G → F<VAR>f' : G →L[ℝ] F<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 • ((innerSL ℝ) (f x)).comp f') s x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>f : ℝ → F<VAR>f' : F<VAR>s : Set ℝ<VAR>x : ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 * ⟪f x, f'⟫_ℝ) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>x : G<VAR>hf : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun y => ‖f y‖ ^ 2) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>x : G<VAR>hf : DifferentiableAt ℝ f x<VAR>h0 : f x ≠ 0<GOAL>DifferentiableAt ℝ (fun y => ‖f y‖) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>x : G<VAR>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>hne : f x ≠ g x<GOAL>DifferentiableAt ℝ (fun y => dist (f y) (g y)) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>hf : Differentiable ℝ f<GOAL>Differentiable ℝ fun y => ‖f y‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>hf : Differentiable ℝ f<VAR>h0 : ∀ (x : G), f x ≠ 0<GOAL>Differentiable ℝ fun y => ‖f y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<VAR>hne : ∀ (x : G), f x ≠ g x<GOAL>Differentiable ℝ fun y => dist (f y) (g y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun y => ‖f y‖ ^ 2) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>x : G<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>h0 : f x ≠ 0<GOAL>DifferentiableWithinAt ℝ (fun y => ‖f y‖) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>x : G<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hg : DifferentiableWithinAt ℝ g s x<VAR>hne : f x ≠ g x<GOAL>DifferentiableWithinAt ℝ (fun y => dist (f y) (g y)) s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>hf : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun y => ‖f y‖ ^ 2) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f : G → E<VAR>s : Set G<VAR>hf : DifferentiableOn ℝ f s<VAR>h0 : ∀ x ∈ s, f x ≠ 0<GOAL>DifferentiableOn ℝ (fun y => ‖f y‖) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>NormedSpace ℝ E<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f g : G → E<VAR>s : Set G<VAR>hf : DifferentiableOn ℝ f s<VAR>hg : DifferentiableOn ℝ g s<VAR>hne : ∀ x ∈ s, f x ≠ g x<GOAL>DifferentiableOn ℝ (fun y => dist (f y) (g y)) s
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>y : H<GOAL>DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => f x i) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>t : Set H<GOAL>DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<GOAL>Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>y : H<GOAL>HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>HasFDerivWithinAt f f' t y ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => f x i) ((EuclideanSpace.proj i).comp f') t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => f x i) t y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => f x i) y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>RCLike 𝕜<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => f x i