awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
h₁ : ‖v‖ < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
⊢ v ∈ p.ball 0 1 ↔ Membership.mem (γ := Set F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} v

Tactic:
simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_setOf_eq, p]

Premises used: dist_eq_norm, sub_zero, ball_normSeminorm, Set.mem_setOf_eq, Metric.mem_ball
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
h₁ : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
⊢ ‖v‖ < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)

Tactic:
change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1

Premises used: Inner.inner, RCLike.re, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ 1 = √1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
rw : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1
| √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1

Tactic:
rw [show (1 : ℝ) = √1 by simp]
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
h₁ : √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)
⊢ √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < 1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)

Tactic:
conv_lhs => rw [show (1 : ℝ) = √1 by simp]
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
h₁ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ)
⊢ √((re : (a : 𝕜) → ℝ) ⟪v, v⟫) < √1 ↔ LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)

Tactic:
rw [sqrt_lt_sqrt_iff]

Premises used: Real.sqrt_lt_sqrt_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ)

Tactic:
InnerProductSpace.Core.inner_self_nonneg

Premises used: InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
v : F
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ)

Tactic:
exact InnerProductSpace.Core.inner_self_nonneg

Premises used: InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
have : p.ball 0 1 = {v | re (cd.inner v v) < 1} := by
    ext v
    simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_setOf_eq, p]
    change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1
    conv_lhs => rw [show (1 : ℝ) = √1 by simp]
    rw [sqrt_lt_sqrt_iff]
    exact InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
rw :
  Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} ∧
    IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p

Tactic:
rw [withSeminorms_iff_mem_nhds_isVonNBounded, this]

Premises used: withSeminorms_iff_mem_nhds_isVonNBounded
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} ∧
    IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
⟨?_, h'⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
refine : Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} ∧
    IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
refine ⟨?_, h'⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0

Tactic:
have A : ContinuousAt (fun (v : F) ↦ re (cd.inner v v)) 0 := by fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
simp : Membership.mem (γ := Filter ℝ) (𝓝 0) (Set.Iio 1)
⊢ Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)

Tactic:
simp only [InnerProductSpace.Core.inner_zero_left, map_zero]

Premises used: map_zero, InnerProductSpace.Core.inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
⊢ LT.lt (α := ℝ) 0 1

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0) (Set.Iio 1)

Tactic:
exact Iio_mem_nhds (by positivity)

Premises used: Iio_mem_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
⊢ Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)

Tactic:
have B : Set.Iio 1 ∈ 𝓝 (re (cd.inner 0 0)) := by
    simp only [InnerProductSpace.Core.inner_zero_left, map_zero]
    exact Iio_mem_nhds (by positivity)
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
B : Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
A B

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
B : Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
exact A B
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
rw : √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [norm_eq_sqrt_re_inner, inner_smul_left, inner_smul_right, ← mul_assoc]

Premises used: InnerProductSpace.Core.inner_smul_right, InnerProductSpace.Core.inner_smul_left, InnerProductSpace.Core.norm_eq_sqrt_re_inner, mul_assoc
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
rw : √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖
hx : 0 ≤ HPow.hPow (β := ℕ) ‖r‖ 2
⊢ √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖

Tactic:
rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self,
        ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.conj_mul, Real.sqrt_mul, RCLike.ofReal_pow, RCLike.re_ofReal_mul, InnerProductSpace.Core.ofReal_normSq_eq_inner_self
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖

Tactic:
simp [sqrt_normSq_eq_norm]

Premises used: InnerProductSpace.Core.sqrt_normSq_eq_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖r‖ 2

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2

Tactic:
have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)

Tactic:
have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
h₂ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜

Tactic:
simp [h₁, sq_sqrt, h₂]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
hF : Module 𝕜 F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫_𝕜 : ℝ) (1 : ℝ)}
this_1 : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2

Tactic:
have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
hF : Module 𝕜 F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫_𝕜 : ℝ) (1 : ℝ)}
this_1 : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)

Tactic:
have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
hF : Module 𝕜 F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫_𝕜 : ℝ) (1 : ℝ)}
this_1 : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
h₂ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜

Tactic:
simp [h₁, sq_sqrt, h₂]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ ∀ (x : PUnit.{u_4 + 1}), HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ ∀ (x y : PUnit.{u_4 + 1}), Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ ∀ (x y z : PUnit.{u_4 + 1}), 0 = HAdd.hAdd (α := 𝕜) 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
⊢ ∀ (x y : PUnit.{u_4 + 1}) (r : 𝕜), 0 = HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (0 : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x y : PUnit.{u_4 + 1}
⊢ inner 𝕜 x y = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq (α := E →L⋆[𝕜] StrongDual 𝕜 E) (LinearIsometry.toContinuousLinearMap (E₂ := StrongDual 𝕜 E) (toDualMap 𝕜 E))
    (innerSL 𝕜)

Tactic:
rfl

Premises used: innerSL, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, LinearMap.mkContinuousOfExistsBound₂, rfl, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E) : (a : E) → 𝕜) y = ⟪x, y⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ Eq (α := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
      ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) y : E →L[𝕜] 𝕜) ↔
    x = y

Tactic:
(toDualMap 𝕜 E).injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearIsometry.injective, InnerProductSpace.toDualMap