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 y : F
t : ℝ
this :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t)
          ((re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
this₁ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
this₂ this₃ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ)
          ((re : (a : 𝕜) → ℝ)
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ :
            ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) (⟪x, y⟫ * (↑t : 𝕜)) : ℝ))
        ((re : (a : 𝕜) → ℝ) (⟪y, x⟫ * (↑t : 𝕜)) : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
rw
    [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]

Premises used: InnerProductSpace.Core.inner_smul_ofReal_right, InnerProductSpace.Core.inner_smul_ofReal_left, InnerProductSpace.Core.re_inner_smul_ofReal_smul_self
-- 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
t : ℝ
rw rw₁ :
  normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ HAdd.hAdd (β := ℝ)
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t)
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
rw [← normSq]

Premises used: InnerProductSpace.Core.normSq
-- 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
t : ℝ
rw rw₁ :
  normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
rw [inner_re_symm]

Premises used: InnerProductSpace.Core.inner_re_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
t : ℝ
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
        HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) * t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
ring
-- 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 :
  ⟪⟪x, y⟫ • x - ⟪x, x⟫ • y, ⟪x, y⟫ • x - ⟪x, x⟫ • y⟫ =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x *
          (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2)) :
      𝕜)
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x - ⟪x, x⟫ • y) =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x *
      (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2)

Tactic:
rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]

Premises used: RCLike.ofReal_inj, InnerProductSpace.Core.ofReal_normSq_eq_inner_self
-- 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, y⟫ *
            HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜)
              ((↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ⟪x, y⟫ -
        ⟪x, y⟫ * ((↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * ⟪y, x⟫) +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x * (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y) -
          normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) :
      𝕜)
⊢ ⟪⟪x, y⟫ • x - ⟪x, x⟫ • y, ⟪x, y⟫ • x - ⟪x, x⟫ • y⟫ =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x *
          (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2)) :
      𝕜)

Tactic:
simp only [inner_sub_sub_self, inner_smul_left, inner_smul_right, conj_ofReal, mul_sub, ←
    ofReal_normSq_eq_inner_self x, ← ofReal_normSq_eq_inner_self y]

Premises used: InnerProductSpace.Core.inner_smul_right, InnerProductSpace.Core.inner_smul_left, mul_sub, RCLike.conj_ofReal, InnerProductSpace.Core.inner_sub_sub_self, InnerProductSpace.Core.ofReal_normSq_eq_inner_self
-- 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 :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 -
        (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x * (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y) -
          normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) :
      𝕜)
⊢ ⟪x, y⟫ *
            HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜)
              ((↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) ⟪x, y⟫ -
        ⟪x, y⟫ * ((↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * ⟪y, x⟫) +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x * (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y) -
          normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) :
      𝕜)

Tactic:
rw [← mul_assoc, mul_conj, RCLike.conj_mul, mul_left_comm, ← inner_conj_symm y, mul_conj]

Premises used: RCLike.mul_conj, mul_assoc, RCLike.conj_mul, mul_left_comm, InnerProductSpace.Core.inner_conj_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
push_cast :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 -
        (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) -
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 -
        (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x * (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y) -
          normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) :
      𝕜)

Tactic:
push_cast
-- 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
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) -
          (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 -
        (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 +
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) =
    (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) *
        HMul.hMul (α := 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) y) : 𝕜) -
      (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2

Tactic:
ring
-- 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
this : discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0
rw : ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
rw [norm_inner_symm y x]

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
this : discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0
⊢ 2 * ‖⟪x, y⟫‖ * (2 * ‖⟪x, y⟫‖) -
      HMul.hMul (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) (4 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    0

Tactic:
rw [discrim, normSq, normSq, sq] at this

Premises used: discrim, sq, InnerProductSpace.Core.normSq
-- 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
this :
  2 * ‖⟪x, y⟫‖ * (2 * ‖⟪x, y⟫‖) -
      HMul.hMul (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) (4 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) ≤
    0
linarith :
  HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) < ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ →
    2 * ‖⟪x, y⟫‖ * (2 * ‖⟪x, y⟫‖) -
            HMul.hMul (β := ℝ) (HMul.hMul (α := ℝ) (β := ℝ) (4 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
              ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
          0 +
        4 *
          (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
            ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖) =
      0
linarith₁ :
  HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) < ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ →
    GT.gt (α := ℝ) 4 0
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
linarith
-- 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
suffices : discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0
⊢ ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
suffices discrim (normSqF x) (2 * ‖⟪x, y⟫_𝕜‖) (normSqF y) ≤ 0 by
    rw [norm_inner_symm y x]
    rw [discrim, normSq, normSq, sq] at this
    linarith
-- 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
⊢ discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0

Tactic:
discrim_le_zero fun t ↦ ?_

Premises used: discrim_le_zero
-- 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
refine : ∀ (t : ℝ), 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0

Tactic:
refine discrim_le_zero fun t ↦ ?_

Premises used: discrim_le_zero
-- 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
t : ℝ
pos :
  ∀ (hzero : ⟪x, y⟫ = 0), 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
neg :
  ∀ (hzero : ¬⟪x, y⟫ = 0), 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
by_cases hzero : ⟪x, y⟫ = 0
-- 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
t : ℝ
hzero : ⟪x, y⟫ = 0
pos : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 + normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
simp only [← sq, hzero, norm_zero, mul_zero, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, norm_zero, sq, MulZeroClass.mul_zero, add_zero
-- 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
t : ℝ
hzero : ⟪x, y⟫ = 0
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x ∧ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
⟨inner_self_nonneg, inner_self_nonneg⟩

Premises used: InnerProductSpace.Core.inner_self_nonneg, 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
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ⟪x, y⟫ = 0
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x

Tactic:
obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, 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 y : F
t : ℝ
hzero : ⟪x, y⟫ = 0
hx : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, 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 y : F
t : ℝ
hzero : ⟪x, y⟫ = 0
hx : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x
hy : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) y
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 + normSq.{u_1, u_3} (𝕜 := 𝕜) y

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 : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
⊢ ‖⟪x, y⟫‖ ≠ 0

Tactic:
have hzero' : ‖⟪x, y⟫‖ ≠ 0 := norm_ne_zero_iff.2 hzero
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ 0 ≤
    normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖) +
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ) * (t / ‖⟪x, y⟫‖) +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖)

Premises used: Norm.norm, Inner.inner, HDiv.hDiv, InnerProductSpace.Core.cauchy_schwarz_aux', HSMul.hSMul
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h : normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) = normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖)
h₁ : 2 * ‖⟪x, y⟫‖ * t = HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ) * (t / ‖⟪x, y⟫‖)
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
convert! cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h :
  normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HPow.hPow (β := ℕ) t 2 * normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x)
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) = normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖)

Tactic:
field_simp
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) t 2)
      ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * ⟪x, x⟫) : ℝ)
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HPow.hPow (β := ℕ) t 2 * normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x)

Tactic:
rw [normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫,
        mul_conj]

Premises used: InnerProductSpace.Core.inner_smul_right, InnerProductSpace.Core.inner_smul_left, RCLike.mul_conj, InnerProductSpace.Core.normSq
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HPow.hPow (β := ℕ) t 2 * HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) t 2)
      ((re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖⟪x, y⟫‖ : 𝕜) 2 * ⟪x, x⟫) : ℝ)

Tactic:
rw [← ofReal_pow, re_ofReal_mul]

Premises used: RCLike.ofReal_pow, RCLike.re_ofReal_mul
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (HPow.hPow (β := ℕ) t 2) * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 =
    HPow.hPow (β := ℕ) t 2 * HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
ring
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h : HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ)
⊢ 2 * ‖⟪x, y⟫‖ * t = HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ) * (t / ‖⟪x, y⟫‖)

Tactic:
field_simp
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
h : HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = t * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ)

Tactic:
rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]

Premises used: InnerProductSpace.Core.inner_smul_left, RCLike.ofReal_re, RCLike.mul_conj, Inner.inner, RCLike.ofReal_pow, mul_comm
-- 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
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2 * t = t * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2

Tactic:
ring
-- 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
⊢ ‖x‖ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)

Tactic:
rfl

Premises used: rfl