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
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
rw₁ :
  (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
    √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
rw₂ rw₃ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖

Tactic:
rw [norm_eq_sqrt_re_inner, ← sqrt_mul inner_self_nonneg, sqrt_mul_self inner_self_nonneg]

Premises used: InnerProductSpace.Core.norm_eq_sqrt_re_inner, Real.sqrt_mul_self, Real.sqrt_mul, 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
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) = ‖x‖

Tactic:
rfl

Premises used: InnerProductSpace.Core.normSq, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
rw rw₁ : ‖⟪y, x⟫‖ * ‖⟪y, x⟫‖ = ‖⟪y, x⟫‖ * ‖⟪y, x⟫‖
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ = ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖

Tactic:
rw [norm_inner_symm]

Premises used: InnerProductSpace.Core.norm_inner_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
simp : ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
simp only [inner_self_eq_norm_mul_norm]

Premises used: InnerProductSpace.Core.inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
ring
-- 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
c : PreInnerProductSpace.Core 𝕜 F
⊢ √((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) = 0

Tactic:
simp only [sqrt_zero, inner_zero_right, map_zero]

Premises used: map_zero, InnerProductSpace.Core.inner_zero_right, Real.sqrt_zero
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖

Tactic:
have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖

Tactic:
have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ≤ ‖x‖ * ‖y‖
rwa₁ rwa₂ rwa₃ rwa₄ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖

Tactic:
rwa [← inner_conj_symm, conj_re]

Premises used: RCLike.conj_re, InnerProductSpace.Core.inner_conj_symm
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖

Tactic:
have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
simp :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)

Tactic:
simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]

Premises used: InnerProductSpace.Core.inner_self_eq_norm_mul_norm, map_add, mul_comm, mul_add, InnerProductSpace.Core.inner_add_add_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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
linarith :
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
        HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) <
      HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
          ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) →
    ‖⟪x, y⟫‖ - ‖x‖ * ‖y‖ + HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ‖⟪x, y⟫‖ +
          HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (‖x‖ * ‖y‖) +
        (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
            HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
          HAdd.hAdd (β := ℝ)
            (HAdd.hAdd (β := ℝ)
              (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
              ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
            ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)) =
      0
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
linarith
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)

Tactic:
have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) := by
          simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
          linarith
-- 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this

Premises used: nonneg_le_nonneg_of_sq_le_sq, add_nonneg, Real.sqrt_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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this

Premises used: nonneg_le_nonneg_of_sq_le_sq, add_nonneg, Real.sqrt_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
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪-x, -x⟫) = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)

Tactic:
simp only [inner_neg_left, neg_neg, inner_neg_right]

Premises used: InnerProductSpace.Core.inner_neg_left, InnerProductSpace.Core.inner_neg_right, neg_neg
-- 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
c : PreInnerProductSpace.Core 𝕜 F
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
c : PreInnerProductSpace.Core 𝕜 F
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
c : PreInnerProductSpace.Core 𝕜 F
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
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖r‖ 2

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
c_1 : PreInnerProductSpace.Core 𝕜 F
c : 𝕜
x : F
this : NormedSpace 𝕜 F := toNormedSpace
⊢ ‖c • x‖ = ‖c‖ * ‖x‖

Tactic:
_root_.norm_smul c x

Premises used: norm_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c_1 : PreInnerProductSpace.Core 𝕜 F
c : 𝕜
x : F
this : NormedSpace 𝕜 F := toNormedSpace
⊢ ‖c • x‖ = ‖c‖ * ‖x‖

Tactic:
exact _root_.norm_smul c x

Premises used: norm_smul
-- 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
x : F
⊢ ⟪x, x⟫ = 0 ↔ x = 0

Tactic:
⟨cd.definite _, inner_self_of_eq_zero⟩

Premises used: Iff.intro, InnerProductSpace.Core.inner_self_of_eq_zero, InnerProductSpace.Core.definite
-- 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
x : F
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x = 0 ↔ ⟪x, x⟫ = 0

Tactic:
simp only [normSq, ext_iff, map_zero, inner_self_im, and_true]

Premises used: and_true, map_zero, InnerProductSpace.Core.normSq, InnerProductSpace.Core.inner_self_im
-- 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
x : F
⊢ ⟪x, x⟫ ≠ 0 ↔ x ≠ 0

Tactic:
inner_self_eq_zero.not

Premises used: InnerProductSpace.Core.inner_self_eq_zero, Iff.not
-- 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
⊢ √((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) = 0

Tactic:
simp only [sqrt_zero, inner_zero_right, map_zero]

Premises used: map_zero, InnerProductSpace.Core.inner_zero_right, Real.sqrt_zero
-- 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
x y : F
⊢ ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
have h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖ := norm_inner_le_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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖

Tactic:
have h₂ : re ⟪x, y⟫ ≤ ‖⟪x, y⟫‖ := re_le_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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖

Tactic:
have h₃ : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ := h₂.trans h₁
-- 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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ≤ ‖x‖ * ‖y‖
rwa₁ rwa₂ rwa₃ rwa₄ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖

Tactic:
rwa [← inner_conj_symm, conj_re]

Premises used: RCLike.conj_re, InnerProductSpace.Core.inner_conj_symm
-- 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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖

Tactic:
have h₄ : re ⟪y, x⟫ ≤ ‖x‖ * ‖y‖ := by rwa [← inner_conj_symm, conj_re]
-- 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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
simp :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)

Tactic:
simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]

Premises used: InnerProductSpace.Core.inner_self_eq_norm_mul_norm, map_add, mul_comm, mul_add, InnerProductSpace.Core.inner_add_add_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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
linarith :
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
        HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) <
      HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
          ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) →
    ‖⟪x, y⟫‖ - ‖x‖ * ‖y‖ + HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ‖⟪x, y⟫‖ +
          HSub.hSub (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (‖x‖ * ‖y‖) +
        (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
            HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
          HAdd.hAdd (β := ℝ)
            (HAdd.hAdd (β := ℝ)
              (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
              ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
            ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)) =
      0
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (‖x‖ * ‖y‖) +
      HAdd.hAdd (β := ℝ) (‖x‖ * ‖y‖) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
linarith
-- 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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)

Tactic:
have : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖) := by
          simp only [← inner_self_eq_norm_mul_norm, inner_add_add_self, mul_add, mul_comm, map_add]
          linarith
-- 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
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this

Premises used: nonneg_le_nonneg_of_sq_le_sq, add_nonneg, Real.sqrt_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 : Core 𝕜 F
x y : F
h₁ : ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖
h₂ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖⟪x, y⟫‖
h₃ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖
h₄ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ ≤ ‖x‖ * ‖y‖
this : ‖x + y‖ * ‖x + y‖ ≤ (‖x‖ + ‖y‖) * (‖x‖ + ‖y‖)
⊢ √((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫) ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) + √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
exact nonneg_le_nonneg_of_sq_le_sq (add_nonneg (sqrt_nonneg _) (sqrt_nonneg _)) this

Premises used: nonneg_le_nonneg_of_sq_le_sq, add_nonneg, Real.sqrt_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 : Core 𝕜 F
x : F
⊢ √((re : (a : 𝕜) → ℝ) ⟪-x, -x⟫) = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)

Tactic:
simp only [inner_neg_left, neg_neg, inner_neg_right]

Premises used: InnerProductSpace.Core.inner_neg_left, InnerProductSpace.Core.inner_neg_right, neg_neg
-- 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
c : 𝕜
x : F
this : NormedSpace 𝕜 F := toNormedSpace
⊢ ‖c • x‖ = ‖c‖ * ‖x‖

Tactic:
_root_.norm_smul c x

Premises used: norm_smul
-- 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
c : 𝕜
x : F
this : NormedSpace 𝕜 F := toNormedSpace
⊢ ‖c • x‖ = ‖c‖ * ‖x‖

Tactic:
exact _root_.norm_smul c x

Premises used: norm_smul
-- 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 : WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
rw :
  Eq.{u_3 + 1} (α := TopologicalSpace F) (⨅ (i : Fin 1), UniformSpace.toTopologicalSpace)
    UniformSpace.toTopologicalSpace
⊢ tF = UniformSpace.toTopologicalSpace

Tactic:
rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]

Premises used: SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, Iff.mp
-- 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 : WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
⊢ Eq.{u_3 + 1} (α := TopologicalSpace F) (⨅ (i : Fin 1), UniformSpace.toTopologicalSpace)
    UniformSpace.toTopologicalSpace

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
suffices : WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
⊢ tF = UniformSpace.toTopologicalSpace

Tactic:
suffices WithSeminorms (fun (i : Fin 1) ↦ p) by
    rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 this]
    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
h₁ :
  ∀ (v : F),
    v ∈ p.ball 0 1 ↔ Membership.mem (γ := Set F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} v
⊢ p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}

Tactic:
ext v