awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
hbc :
  ‖f x‖ ^ (p - 2 + 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x) =
    ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)
⊢ ‖f x‖ ^ (p - 2) *
      (Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) (f x) : E →L[ℝ] ℝ) *
        Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)) =
    ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)

Tactic:
rw [innerSL_apply_norm, ← mul_assoc, ← Real.rpow_add_one' (by positivity) (by linarith)]

Premises used: mul_assoc, innerSL_apply_norm, Real.rpow_add_one'
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖f x‖ ^ (p - 2 + 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x) =
    ‖f x‖ ^ (p - 1) * Norm.norm (E := F →L[ℝ] E) (fderiv ℝ f x)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
rw :
  ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) =
    p * ‖x‖ ^ (p - 1)
⊢ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x) = p * ‖x‖ ^ (p - 1)

Tactic:
rw [fderiv_norm_rpow x hp, norm_smul, norm_mul]

Premises used: norm_smul, norm_mul, fderiv_norm_rpow
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
simp_rw : p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)
⊢ ‖p‖ * ‖‖x‖ ^ (p - 2)‖ * Norm.norm (E := E →L[ℝ] ℝ) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ) =
    p * ‖x‖ ^ (p - 1)

Tactic:
simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc, innerSL_apply_norm]

Premises used: Iff.mpr, mul_assoc, LT.lt.le, norm_norm, zero_le_one, innerSL_apply_norm, LE.le.trans, Real.norm_rpow_of_nonneg, abs_eq_self, norm_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
linarith : p - 2 + 1 = 0 → 1 - p + (p - 2 + 1 - 0) = 0
⊢ p - 2 + 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
rw : p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)
⊢ p * (‖x‖ ^ (p - 2) * ‖x‖) = p * ‖x‖ ^ (p - 1)

Tactic:
rw [← Real.rpow_add_one' (by positivity) (by linarith)]

Premises used: Real.rpow_add_one'
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2 + 1) = p * ‖x‖ ^ (p - 1)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ≥0
hp : 1 < p
⊢ nnnorm (E := F →L[ℝ] ℝ) (fderiv ℝ (fun (x : F) ↦ ‖f x‖ ^ (↑p : ℝ)) x) ≤
    p * ‖f x‖₊ ^ ((↑p : ℝ) - 1) * nnnorm (E := F →L[ℝ] E) (fderiv ℝ f x)

Tactic:
norm_fderiv_norm_rpow_le hf hp

Premises used: norm_fderiv_norm_rpow_le, NNReal.toReal
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ≥0
hp : 1 < p
⊢ enorm (E := F →L[ℝ] ℝ) (fderiv ℝ (fun (x : F) ↦ ‖f x‖ ^ (↑p : ℝ)) x) ≤
    (↑p : ENNReal) * ‖f x‖ₑ ^ ((↑p : ℝ) - 1) * enorm (E := F →L[ℝ] E) (fderiv ℝ f x)

Tactic:
simpa [enorm, ← ENNReal.coe_rpow_of_nonneg _ (sub_nonneg.2 <| NNReal.one_le_coe.2 hp.le),
    ← ENNReal.coe_mul] using nnnorm_fderiv_norm_rpow_le hf hp

Premises used: Iff.mpr, ENNReal.coe_rpow_of_nonneg, NNReal.one_le_coe, LT.lt.le, ENNReal.coe_mul, ENorm.enorm, nnnorm_fderiv_norm_rpow_le, sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
rw :
  (Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
⊢ ContDiff ℝ (F := ℝ) 1 fun (x : E) ↦ ‖x‖ ^ p

Tactic:
rw [contDiff_one_iff_fderiv]

Premises used: contDiff_one_iff_fderiv
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
⊢ (Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)

Tactic:
⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩

Premises used: hasFDerivAt_norm_rpow, HasFDerivAt.differentiableAt, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
refine : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)
⊢ (Differentiable ℝ (F := ℝ) fun (x : E) ↦ ‖x‖ ^ p) ∧
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)

Tactic:
refine ⟨fun x ↦ hasFDerivAt_norm_rpow x hp |>.differentiableAt, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
simp_rw : ∀ (x : E), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p)

Tactic:
simp_rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
pos : ∀ (hx : x = 0), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
neg : ∀ (hx : ¬x = 0), ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
pos : Filter.Tendsto.{u_1, u_1} (α := E) (β := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x

Tactic:
simp_rw [hx, ContinuousAt, fderiv_norm_rpow (0 : E) hp, norm_zero, map_zero, smul_zero]

Premises used: ContinuousAt, norm_zero, smul_zero, map_zero, fderiv_norm_rpow, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
pos :
  Filter.Tendsto (β := ℝ) (fun (x : E) ↦ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x)) (𝓝 0) (𝓝 0)
⊢ Filter.Tendsto.{u_1, u_1} (α := E) (β := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x)) (𝓝 0) (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_
      (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)

Premises used: Norm.norm, tendsto_of_tendsto_of_tendsto_of_le_of_le, Real, tendsto_const_nhds, Eq.le, fderiv, HPow.hPow, norm_fderiv_norm_id_rpow, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
pos : Filter.Tendsto (β := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ Norm.norm (E := E →L[ℝ] ℝ) (fderiv ℝ (fun (x : E) ↦ ‖x‖ ^ p) x)) (𝓝 0) (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (tendsto_const_nhds) ?_
      (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_fderiv_norm_id_rpow _ hp |>.le)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, Eq.le, norm_fderiv_norm_id_rpow, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
this : ContinuousAt (Y := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this

Premises used: ContinuousAt, LT.lt.ne', sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
pos : ContinuousAt (Y := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) 0
⊢ Filter.Tendsto (β := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
suffices ContinuousAt (fun x : E ↦ p * ‖x‖ ^ (p - 1)) 0 by
      simpa [ContinuousAt, sub_ne_zero_of_ne hp.ne'] using this
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Norm.norm.{u_1} (E := E) 0 ≠ 0 ∨ 0 ≤ p - 1

Tactic:
simp [hp.le]

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
funProp : Norm.norm.{u_1} (E := E) 0 ≠ 0 ∨ 0 ≤ p - 1
⊢ ContinuousAt (Y := ℝ) (fun (x : E) ↦ p * ‖x‖ ^ (p - 1)) 0

Tactic:
fun_prop (discharger := simp [hp.le])

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
neg :
  ContinuousAt (Y := E →L[ℝ] ℝ)
    (fun (x : E) ↦ HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
⊢ ContinuousAt (Y := E →L[ℝ] ℝ) (fderiv ℝ fun (x : E) ↦ ‖x‖ ^ p) x

Tactic:
simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]

Premises used: funext, fderiv_norm_rpow
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ‖x‖ ≠ 0 ∨ 0 ≤ p - 2

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
funProp : ‖x‖ ≠ 0 ∨ 0 ≤ p - 2
⊢ ContinuousAt (Y := E →L[ℝ] ℝ)
    (fun (x : E) ↦ HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x

Tactic:
fun_prop (discharger := simp [hx])
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : ContDiff ℝ 1 f
p : ℝ
hp : 1 < p
⊢ ContDiff ℝ (F := ℝ) 1 fun (x : F) ↦ ‖f x‖ ^ p

Tactic:
contDiff_norm_rpow hp |>.comp hf

Premises used: ContDiff.comp, contDiff_norm_rpow
-- Module: Mathlib.Analysis.InnerProductSpace.NormPow
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
p : ℝ
hp : 1 < p
⊢ Differentiable ℝ (F := ℝ) fun (x : F) ↦ ‖f x‖ ^ p

Tactic:
contDiff_norm_rpow hp |>.differentiable one_ne_zero |>.comp hf

Premises used: ContDiff.differentiable, contDiff_norm_rpow, one_ne_zero, Differentiable.comp
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ InnerProductSpaceable E

Tactic:
⟨parallelogram_law_with_norm_mul 𝕜⟩

Premises used: parallelogram_law_with_norm_mul, InnerProductSpaceable.mk
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
⊢ InnerProductSpaceable E

Tactic:
⟨parallelogram_law_with_norm_mul ℝ⟩

Premises used: parallelogram_law_with_norm_mul, Real, InnerProductSpaceable.mk
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
unfold :
  Continuous.{0, u_1} (Y := 𝕜) fun (x : ℝ) ↦
    4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) +
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜) -
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (x : ℝ) ↦ _root_.inner_ 𝕜 (f x) (g x)

Tactic:
unfold _root_.inner_

Premises used: _private.0.inner_
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (x : ℝ) ↦
    4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x + g x‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖f x - g x‖ : 𝕜) +
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) + g x‖ : 𝕜) -
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (f x) - g x‖ : 𝕜))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
simp :
  HPow.hPow (β := ℕ) ‖x‖ 2 =
    4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * ‖x + x‖ - HMul.hMul (α := ℝ) 0 0 - (‖x - x‖ * ‖x - x‖ - HMul.hMul (α := ℝ) 0 0) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                0) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              0)) -
      -0 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                0 +
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              0 +
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖))
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (inner_ 𝕜 x x)

Tactic:
simp only [inner_, normSq_apply, ofNat_re, ofNat_im, map_sub, map_add,
    ofReal_re, ofReal_im, mul_re, inv_re, mul_im, I_re, inv_im]

Premises used: RCLike.ofReal_re, map_sub, RCLike.ofNat_re, _private.0.inner_, map_add, RCLike.inv_im, RCLike.ofReal_im, RCLike.ofNat_im, RCLike.mul_im, RCLike.mul_re, RCLike.I_re, RCLike.normSq_apply, RCLike.inv_re
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ ‖x - x‖ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ ‖x - x‖ = 0

Tactic:
have h₁ : ‖x - x‖ = 0 := by simp
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ ‖HSMul.hSMul (α := ℕ) 2 x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖

Tactic:
norm_nsmul 𝕜 2 x

Premises used: RCLike.norm_nsmul, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
h : x + x = HSMul.hSMul (α := ℕ) 2 x
⊢ ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖

Tactic:
convert! norm_nsmul 𝕜 2 x using 2

Premises used: RCLike.norm_nsmul, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ x + x = HSMul.hSMul (α := ℕ) 2 x

Tactic:
module
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖

Tactic:
have h₂ : ‖x + x‖ = 2 • ‖x‖ := by convert! norm_nsmul 𝕜 2 x using 2; module
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
h₂ : ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (HSMul.hSMul (α := ℕ) 2 ‖x‖ * HSMul.hSMul (α := ℕ) 2 ‖x‖ - HMul.hMul (α := ℝ) 0 0 -
              (HMul.hMul (α := ℝ) 0 0 - HMul.hMul (α := ℝ) 0 0) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                0) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              0)) -
      -0 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (HSMul.hSMul (α := ℕ) 2 ‖x‖ * 0 + 0 * HSMul.hSMul (α := ℕ) 2 ‖x‖ -
              (HMul.hMul (α := ℝ) 0 0 + HMul.hMul (α := ℝ) 0 0) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                0 +
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              0 +
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖))

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
simp :
  4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖y + x‖ : 𝕜) (↑‖y + x‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖y - x‖ : 𝕜) (↑‖y - x‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y

Tactic:
simp only [inner_, map_sub, map_add, map_mul, map_inv₀, map_ofNat, conj_ofReal, conj_I]

Premises used: map_sub, _private.0.inner_, RCLike.conj_ofReal, map_ofNat, map_inv₀, map_add, map_mul, RCLike.conj_I