awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ)) -
      HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) +
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
r : ℝ
simp :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) (HMul.hMul (β := ℝ) r ((re : (a : 𝕜) → ℝ) x : ℝ)) -
      HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-HMul.hMul (β := ℝ) r ((im : (a : 𝕜) → ℝ) x : ℝ)) =
    r *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ))
⊢ (re : (a : 𝕜) → ℝ) (y * star (r • x)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ((re : (a : 𝕜) → ℝ) (y * star x) : ℝ)

Tactic:
simp only [star_def, mul_re, conj_re, conj_im, conj_trivial, smul_re, smul_im]

Premises used: RCLike.conj_re, RCLike.star_def, RCLike.smul_re, conj_trivial, RCLike.smul_im, RCLike.conj_im, RCLike.mul_re
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
r : ℝ
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) (HMul.hMul (β := ℝ) r ((re : (a : 𝕜) → ℝ) x : ℝ)) -
      HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-HMul.hMul (β := ℝ) r ((im : (a : 𝕜) → ℝ) x : ℝ)) =
    r *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) y : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ innerProductSpace = toInnerProductSpaceReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ instInnerProductSpaceRealComplex = toInnerProductSpaceReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
x y : ℝ
rw : inner ℝ x y = y * x
⊢ inner ℝ x y = x * y

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
x y : ℝ
⊢ inner ℝ x y = y * x

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x y : E
⊢ Eq (α := ℝ)
    ((RingHom.id ℝ : (a : ℝ) → ℝ) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ) : ℝ)
    ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)

Tactic:
simp [real_inner_comm]

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ Eq (α := SMul ℝ ℂ) (@SemigroupAction.toSMul _ _ Monoid.toSemigroup _)
    (@Algebra.toSMul _ _ Semifield.toCommSemiring Ring.toSemiring _)

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ Eq (α := SMul ℝ ℂ) (@SemigroupAction.toSMul _ _ Monoid.toSemigroup _)
    (@Algebra.toSMul _ _ Semifield.toCommSemiring Ring.toSemiring _)

Tactic:
with_reducible_and_instances rfl
-- 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
p x : E × E
⊢ (fderivInnerCLM 𝕜 p : (a : E × E) → 𝕜) x = ⟪p.1, x.2⟫ + ⟪x.1, p.2⟫

Tactic:
rfl

Premises used: rfl
-- 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
n : WithTop ℕ∞
⊢ ContDiff.{0, u_2, u_1} ℝ (F := 𝕜) n fun (p : E × E) ↦ ⟪p.1, p.2⟫

Tactic:
isBoundedBilinearMap_inner.contDiff

Premises used: IsBoundedBilinearMap.contDiff
-- 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
p : E × E
n : WithTop ℕ∞
⊢ ContDiffAt.{0, u_2, u_1} ℝ (F := 𝕜) n (fun (p : E × E) ↦ ⟪p.1, p.2⟫) p

Tactic:
ContDiff.contDiffAt contDiff_inner

Premises used: contDiff_inner, 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
⊢ Differentiable.{0, u_2, u_1} ℝ (F := 𝕜) fun (p : E × E) ↦ ⟪p.1, p.2⟫

Tactic:
isBoundedBilinearMap_inner.differentiableAt

Premises used: Differentiable, IsBoundedBilinearMap.differentiableAt
-- 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
⊢ ContDiffWithinAt.{0, u_4, u_1} ℝ (F := 𝕜) n (fun (x : G) ↦ ⟪f x, g x⟫) s x

Tactic:
contDiffAt_inner.comp_contDiffWithinAt x (hf.prodMk hg)

Premises used: ContDiffAt.comp_contDiffWithinAt, contDiffAt_inner, ContDiffWithinAt.prodMk
-- 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
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
⊢ ContDiffAt.{0, u_4, u_1} ℝ (F := 𝕜) n (fun (x : G) ↦ ⟪f x, g x⟫) x

Tactic:
hf.inner 𝕜 hg

Premises used: ContDiffAt, ContDiffWithinAt.inner
-- 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
⊢ ContDiffOn.{0, u_4, u_1} ℝ (F := 𝕜) n (fun (x : G) ↦ ⟪f x, g x⟫) s

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

Premises used: ContDiffOn, ContDiffWithinAt.inner
-- 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
⊢ ContDiff.{0, u_4, u_1} ℝ (F := 𝕜) n fun (x : G) ↦ ⟪f x, g x⟫

Tactic:
contDiff_inner.comp (hf.prodMk hg)

Premises used: ContDiff.prodMk, ContDiff.comp, contDiff_inner
-- 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
f' g' : G →L[ℝ] E
s : Set G
x : G
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun (t : G) ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') s x

Tactic:
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: setOf, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, fderivInnerCLM
-- 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
f' g' : G →L[ℝ] E
s : Set G
x : G
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun (t : G) ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') s x

Tactic:
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasFDerivAt (f x, g x) |>.comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- 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
f' g' : G →L[ℝ] E
x : G
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (fun (t : G) ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

Tactic:
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasStrictFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)

Premises used: setOf, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp, fderivInnerCLM
-- 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
f' g' : G →L[ℝ] E
x : G
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun (t : G) ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

Tactic:
isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)

Premises used: setOf, HasFDerivAt.prodMk, fderivInnerCLM, HasFDerivAt.comp
-- 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
f' g' : G →L[ℝ] E
x : G
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun (t : G) ↦ ⟪f t, g t⟫) (fderivInnerCLM 𝕜 (f x, g x) ∘SL f'.prod g') x

Tactic:
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
    |>.hasFDerivAt (f x, g x) |>.comp x (hf.prodMk hg)

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- 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
f g : ℝ → E
f' g' : E
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) s x

Tactic:
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.inner, 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
f g : ℝ → E
f' g' : E
x : ℝ
⊢ HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun (t : ℝ) ↦ ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) x

Tactic:
simpa only [← hasDerivWithinAt_univ] using HasDerivWithinAt.inner 𝕜

Premises used: HasDerivWithinAt.inner, hasDerivWithinAt_univ
-- 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
⊢ DifferentiableWithinAt.{0, u_4, u_1} ℝ (F := 𝕜) (fun (x : G) ↦ ⟪f x, g x⟫) s x

Tactic:
(hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.inner, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- 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
⊢ DifferentiableAt.{0, u_4, u_1} ℝ (F := 𝕜) (fun (x : G) ↦ ⟪f x, g x⟫) x

Tactic:
(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).differentiableAt

Premises used: HasFDerivAt.inner, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- 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
⊢ DifferentiableOn.{0, u_4, u_1} ℝ (F := 𝕜) (fun (x : G) ↦ ⟪f x, g x⟫) s

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

Premises used: DifferentiableOn, DifferentiableWithinAt.inner
-- 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
⊢ Differentiable.{0, u_4, u_1} ℝ (F := 𝕜) fun (x : G) ↦ ⟪f x, g x⟫

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

Premises used: Differentiable, DifferentiableAt.inner
-- 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
y : G
rw :
  (fderivInnerCLM 𝕜 (f x, g x) ∘SL ContinuousLinearMap.prod (fderiv ℝ f x) (fderiv ℝ g x) : (a : G) → 𝕜) y =
    ⟪f x, (fderiv ℝ g x : (a : G) → E) y⟫ + ⟪(fderiv ℝ f x : (a : G) → E) y, g x⟫
⊢ (fderiv ℝ (fun (t : G) ↦ ⟪f t, g t⟫) x : (a : G) → 𝕜) y =
    ⟪f x, (fderiv ℝ g x : (a : G) → E) y⟫ + ⟪(fderiv ℝ f x : (a : G) → E) y, g x⟫

Tactic:
rw [(hf.hasFDerivAt.inner 𝕜 hg.hasFDerivAt).fderiv]

Premises used: HasFDerivAt.inner, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- 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
y : G
⊢ (fderivInnerCLM 𝕜 (f x, g x) ∘SL ContinuousLinearMap.prod (fderiv ℝ f x) (fderiv ℝ g x) : (a : G) → 𝕜) y =
    ⟪f x, (fderiv ℝ g x : (a : G) → E) y⟫ + ⟪(fderiv ℝ f x : (a : G) → E) y, g x⟫

Tactic:
rfl
-- 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
f g : ℝ → E
x : ℝ
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
⊢ deriv (fun (t : ℝ) ↦ ⟪f t, g t⟫) x = ⟪f x, deriv g x⟫ + ⟪deriv f x, g x⟫

Tactic:
(hf.hasDerivAt.inner 𝕜 hg.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.inner
-- 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
n : WithTop ℕ∞
⊢ ContDiff.{0, u_2, 0} ℝ (E := E) (F := ℝ) n
    (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑reCLM : (a : 𝕜) → ℝ) fun (x : E) ↦ ⟪id x, id x⟫)

Tactic:
(reCLM : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))

Premises used: contDiff_id, RCLike.reCLM, ContDiff.inner, ContDiff.comp, ContinuousLinearMap.contDiff
-- 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
n : WithTop ℕ∞
h :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 2 =
      Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑reCLM : (a : 𝕜) → ℝ) (fun (x : E) ↦ ⟪id x, id x⟫) x
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
convert! (reCLM : 𝕜 →L[ℝ] ℝ).contDiff.comp ((contDiff_id (E := E)).inner 𝕜 (contDiff_id (E := E)))

Premises used: contDiff_id, RCLike.reCLM, ContDiff.inner, ContDiff.comp, ContinuousLinearMap.contDiff
-- 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
n : WithTop ℕ∞
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑reCLM : (a : 𝕜) → ℝ) (fun (x : E) ↦ ⟪id x, id x⟫) x

Tactic:
(inner_self_eq_norm_sq _).symm

Premises used: inner_self_eq_norm_sq, Eq.symm
-- 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
n : WithTop ℕ∞
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑reCLM : (a : 𝕜) → ℝ) (fun (x : E) ↦ ⟪id x, id x⟫) x

Tactic:
exact (inner_self_eq_norm_sq _).symm

Premises used: inner_self_eq_norm_sq, Eq.symm
-- 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
⊢ ContDiff ℝ (F := ℝ) n fun (x : G) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2

Tactic:
(contDiff_norm_sq 𝕜).comp hf

Premises used: contDiff_norm_sq, ContDiff.comp
-- 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
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ HPow.hPow (β := ℕ) ‖f y‖ 2) s x

Tactic:
(contDiff_norm_sq 𝕜).contDiffAt.comp_contDiffWithinAt x hf

Premises used: contDiff_norm_sq, ContDiffAt.comp_contDiffWithinAt, 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 → E
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : G) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) x

Tactic:
hf.norm_sq 𝕜

Premises used: ContDiffAt, 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
n : WithTop ℕ∞
x : E
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) ‖id x‖ 2 ≠ 0

Tactic:
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
-- 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
n : WithTop ℕ∞
x : E
hx : x ≠ 0
this : HPow.hPow (β := ℕ) ‖id x‖ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this

Premises used: id, ContDiffAt.norm_sq, contDiffAt_id, Real.sqrt_sq, norm_nonneg, ContDiffAt.sqrt
-- 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
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
h0 : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y‖) x

Tactic:
(contDiffAt_norm 𝕜 h0).comp x hf

Premises used: contDiffAt_norm, ContDiffAt.comp
-- 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
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
simp : ContDiffAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y - g y‖) x
⊢ ContDiffAt ℝ (F := ℝ) n (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
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ (F := ℝ) n (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, ContDiffAt.norm, ContDiffAt.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
x : G
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
hne : f x ≠ g x
⊢ ContDiffAt ℝ (F := ℝ) n (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, ContDiffAt.norm, ContDiffAt.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
x : G
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
h0 : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y‖) s x

Tactic:
(contDiffAt_norm 𝕜 h0).comp_contDiffWithinAt x hf

Premises used: contDiffAt_norm, ContDiffAt.comp_contDiffWithinAt
-- 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
simp : ContDiffWithinAt ℝ (F := ℝ) n (fun (y : G) ↦ ‖f y - g y‖) s x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (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
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:
(hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Premises used: ContDiffWithinAt.sub, Iff.mpr, sub_ne_zero, ContDiffWithinAt.norm