awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
hne : f x ≠ g x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y - g y‖) s x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: ContDiffWithinAt.sub, Iff.mpr, sub_ne_zero, ContDiffWithinAt.norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
⊢ ContDiffOn ℝ (F := ℝ) n (fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2) s

Tactic:
fun x hx => (hf x hx).norm_sq 𝕜

Premises used: ContDiffOn, ContDiffWithinAt.norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
h0 : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y‖) s

Tactic:
fun x hx => (hf x hx).norm 𝕜 (h0 x hx)

Premises used: ContDiffOn, ContDiffWithinAt.norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hg : ContDiffOn ℝ n g s
hne : ∀ x ∈ s, f x ≠ g x
⊢ ContDiffOn ℝ (F := ℝ) n (fun (y : G) ↦ Dist.dist (f y) (g y)) s

Tactic:
fun x hx =>
  (hf x hx).dist 𝕜 (hg x hx) (hne x hx)

Premises used: ContDiffOn, ContDiffWithinAt.dist
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
n : ℕ∞ω
hf : ContDiff ℝ n f
h0 : ∀ (x : G), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) n fun (y : G) ↦ ‖f y‖

Tactic:
contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.norm 𝕜 (h0 x)

Premises used: Iff.mpr, ContDiffAt.norm, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
n : ℕ∞ω
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
hne : ∀ (x : G), f x ≠ g x
⊢ ContDiff ℝ (F := ℝ) n fun (y : G) ↦ Dist.dist (f y) (g y)

Tactic:
contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.dist 𝕜 hg.contDiffAt (hne x)

Premises used: Iff.mpr, ContDiffAt.dist, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
simp :
  HasStrictFDerivAt (fun (x : F) ↦ (re : (a : ℝ) → ℝ) ⟪x, x⟫)
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x
⊢ HasStrictFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2)
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x

Tactic:
simp only [sq, ← @inner_self_eq_norm_mul_norm ℝ]

Premises used: sq, inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun (t : F) ↦ ⟪id t, id t⟫)
    (fderivInnerCLM ℝ (id x, id x) ∘SL
      ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F))
    x

Tactic:
(hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)

Premises used: Real, HasStrictFDerivAt.inner, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
h :
  instAddCommGroup = Ring.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) =
        fderivInnerCLM ℝ (id x, id x) ∘SL
          ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)
⊢ HasStrictFDerivAt (fun (x : F) ↦ (re : (a : ℝ) → ℝ) ⟪x, x⟫)
    (HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)) x

Tactic:
convert! (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)

Premises used: Real, HasStrictFDerivAt.inner, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : F),
    Eq (α := ℝ)
      ((HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ)
      ((fderivInnerCLM ℝ (id x, id x) ∘SL
              ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F) :
            (a : F) → ℝ)
          y :
        ℝ)
⊢ HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) =
    fderivInnerCLM ℝ (id x, id x) ∘SL ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F)

Tactic:
ext y
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : F
⊢ Eq (α := ℝ)
    ((HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ) : (a : F) → ℝ) y : ℝ)
    ((fderivInnerCLM ℝ (id x, id x) ∘SL
            ContinuousLinearMap.prod (ContinuousLinearMap.id ℝ F) (ContinuousLinearMap.id ℝ F) :
          (a : F) → ℝ)
        y :
      ℝ)

Tactic:
simp [two_smul, real_inner_comm]

Premises used: two_smul, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ fderiv ℝ (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) x =
    HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2 ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) x : F →L[ℝ] ℝ)

Tactic:
(hasStrictFDerivAt_norm_sq x).hasFDerivAt.fderiv

Premises used: hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
h :
  ∀ (x : F),
    fderiv ℝ (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) x =
      HSMul.hSMul (α := ℕ) (β := (a : F) → F →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : F) → F →L[ℝ] ℝ) x
⊢ (fderiv ℝ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) =
    HSMul.hSMul (α := ℕ) (β := (a : F) → F →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : F) → F →L[ℝ] ℝ)

Tactic:
ext1
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ fderiv ℝ (fun (x : F) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) x =
    HSMul.hSMul (α := ℕ) (β := (a : F) → F →L[ℝ] ℝ) 2 (⇑(innerSL ℝ) : (a : F) → F →L[ℝ] ℝ) x

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
G : Type u_4
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
x : G
f : G → F
f' : G →L[ℝ] F
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : G) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2)
    (HSMul.hSMul (α := ℕ) (β := G →L[ℝ] ℝ) 2
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (f x)) f'))
    x

Tactic:
(hasStrictFDerivAt_norm_sq _).hasFDerivAt.comp x hf

Premises used: ContinuousLinearMap.comp, hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
f : ℝ → F
f' : F
x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) (2 * ⟪f x, f'⟫) x

Tactic:
simpa using hf.hasFDerivAt.norm_sq.hasDerivAt

Premises used: HasFDerivAt.norm_sq, HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
G : Type u_4
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
s : Set G
x : G
f : G → F
f' : G →L[ℝ] F
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : G) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2)
    (HSMul.hSMul (α := ℕ) (β := G →L[ℝ] ℝ) 2
      (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (f x)) f'))
    s x

Tactic:
(hasStrictFDerivAt_norm_sq _).hasFDerivAt.comp_hasFDerivWithinAt x hf

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, hasStrictFDerivAt_norm_sq, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
f : ℝ → F
f' : F
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) (2 * ⟪f x, f'⟫) s x

Tactic:
simpa using hf.hasFDerivWithinAt.norm_sq.hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.norm_sq, HasFDerivWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
x : G
hf : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2) x

Tactic:
((contDiffAt_id.norm_sq 𝕜).differentiableAt one_ne_zero).comp x hf

Premises used: ContDiffAt.differentiableAt, ContDiffAt.norm_sq, contDiffAt_id, DifferentiableAt.comp, one_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
x : G
hf : DifferentiableAt ℝ f x
h0 : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y‖) x

Tactic:
((contDiffAt_norm 𝕜 h0).differentiableAt one_ne_zero).comp x hf

Premises used: ContDiffAt.differentiableAt, contDiffAt_norm, DifferentiableAt.comp, one_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
simp : DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ Dist.dist (f y) (g y)) x

Tactic:
simp only [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) x

Tactic:
(hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: Iff.mpr, sub_ne_zero, DifferentiableAt.sub, DifferentiableAt.norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: Iff.mpr, sub_ne_zero, DifferentiableAt.sub, DifferentiableAt.norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
hf : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2

Tactic:
fun x => (hf x).norm_sq 𝕜

Premises used: Differentiable, DifferentiableAt.norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
hf : Differentiable ℝ f
h0 : ∀ (x : G), f x ≠ 0
⊢ Differentiable ℝ (F := ℝ) fun (y : G) ↦ ‖f y‖

Tactic:
fun x => (hf x).norm 𝕜 (h0 x)

Premises used: Differentiable, DifferentiableAt.norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
hf : Differentiable ℝ f
hg : Differentiable ℝ g
hne : ∀ (x : G), f x ≠ g x
⊢ Differentiable ℝ (F := ℝ) fun (y : G) ↦ Dist.dist (f y) (g y)

Tactic:
fun x =>
  (hf x).dist 𝕜 (hg x) (hne x)

Premises used: Differentiable, DifferentiableAt.dist
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2) s x

Tactic:
((contDiffAt_id.norm_sq 𝕜).differentiableAt one_ne_zero).comp_differentiableWithinAt x hf

Premises used: ContDiffAt.differentiableAt, ContDiffAt.norm_sq, contDiffAt_id, DifferentiableAt.comp_differentiableWithinAt, one_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
h0 : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y‖) s x

Tactic:
((contDiffAt_id.norm 𝕜 h0).differentiableAt one_ne_zero).comp_differentiableWithinAt x hf

Premises used: ContDiffAt.differentiableAt, ContDiffAt.norm, contDiffAt_id, DifferentiableAt.comp_differentiableWithinAt, one_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
simp : DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) s x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ Dist.dist (f y) (g y)) s x

Tactic:
simp only [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) s x

Tactic:
(hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: Iff.mpr, DifferentiableWithinAt.norm, sub_ne_zero, DifferentiableWithinAt.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
x : G
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
hne : f x ≠ g x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : G) ↦ ‖f y - g y‖) s x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: Iff.mpr, DifferentiableWithinAt.norm, sub_ne_zero, DifferentiableWithinAt.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
hf : DifferentiableOn ℝ f s
⊢ DifferentiableOn ℝ (F := ℝ) (fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2) s

Tactic:
fun x hx => (hf x hx).norm_sq 𝕜

Premises used: DifferentiableOn, DifferentiableWithinAt.norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : G → E
s : Set G
hf : DifferentiableOn ℝ f s
h0 : ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (y : G) ↦ ‖f y‖) s

Tactic:
fun x hx => (hf x hx).norm 𝕜 (h0 x hx)

Premises used: DifferentiableWithinAt.norm, DifferentiableOn
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : G → E
s : Set G
hf : DifferentiableOn ℝ f s
hg : DifferentiableOn ℝ g s
hne : ∀ x ∈ s, f x ≠ g x
⊢ DifferentiableOn ℝ (F := ℝ) (fun (y : G) ↦ Dist.dist (f y) (g y)) s

Tactic:
fun x hx =>
  (hf x hx).dist 𝕜 (hg x hx) (hne x hx)

Premises used: DifferentiableWithinAt.dist, DifferentiableOn
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
t : Set H
y : H
inst_3 : Finite ι
⊢ DifferentiableWithinAt 𝕜 f t y ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
differentiableWithinAt_piLp _

Premises used: differentiableWithinAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
y : H
inst_3 : Finite ι
⊢ DifferentiableAt 𝕜 f y ↔ ∀ (i : ι), DifferentiableAt 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
differentiableAt_piLp _

Premises used: differentiableAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
t : Set H
inst_3 : Finite ι
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
differentiableOn_piLp _

Premises used: differentiableOn_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
inst_3 : Finite ι
⊢ Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) fun (x : H) ↦ (f x).ofLp i

Tactic:
differentiable_piLp _

Premises used: differentiable_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
y : H
inst_3 : Finite ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
hasStrictFDerivAt_piLp _

Premises used: hasStrictFDerivAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
f' : H →L[𝕜] EuclideanSpace 𝕜 ι
t : Set H
y : H
inst_3 : Finite ι
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
hasFDerivWithinAt_piLp _

Premises used: hasFDerivWithinAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
t : Set H
y : H
inst_3 : Fintype ι
n : WithTop ℕ∞
⊢ ContDiffWithinAt 𝕜 n f t y ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) n (fun (x : H) ↦ (f x).ofLp i) t y

Tactic:
contDiffWithinAt_piLp _

Premises used: contDiffWithinAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
y : H
inst_3 : Fintype ι
n : WithTop ℕ∞
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) n (fun (x : H) ↦ (f x).ofLp i) y

Tactic:
contDiffAt_piLp _

Premises used: contDiffAt_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
t : Set H
inst_3 : Fintype ι
n : WithTop ℕ∞
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) n (fun (x : H) ↦ (f x).ofLp i) t

Tactic:
contDiffOn_piLp _

Premises used: contDiffOn_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
𝕜 : Type u_1
ι : Type u_2
H : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup H
inst_2 : NormedSpace 𝕜 H
f : H → EuclideanSpace 𝕜 ι
inst_3 : Fintype ι
n : WithTop ℕ∞
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 (F := (fun (x : ι) ↦ 𝕜) i) n fun (x : H) ↦ (f x).ofLp i

Tactic:
contDiff_piLp _

Premises used: contDiff_piLp
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
suffices : ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹
⊢ ContDiff.{0, u_1, u_1} ℝ (E := E) (↑n : WithTop ℕ∞) (↑univUnitBall : E → E)

Tactic:
suffices ContDiff ℝ n fun x : E => (√(1 + ‖x‖ ^ 2 : ℝ))⁻¹ from this.smul contDiff_id
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
⊢ 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ ∀ (x : E), 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Calculus
Goal:
n : ℕ∞
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : E) ↦ (√(1 + HPow.hPow (β := ℕ) ‖x‖ 2))⁻¹

Tactic:
ContDiff.inv ?_ fun x => Real.sqrt_ne_zero'.mpr (h x)

Premises used: Iff.mpr, ContDiff.inv, Real.sqrt_ne_zero'