-- 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 : ℝ
calc :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y⟫ :
      ℝ)
    ((re : (a : 𝕜) → ℝ)
        (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
            ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
          ⟪y, y⟫) :
      ℝ)
calc₁ :
  (re : (a : 𝕜) → ℝ)
      (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
            ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
          ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
        ⟪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⟫ : ℝ)
calc₂ :
  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⟫ : ℝ)
calc₃ :
  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 (β := ℝ)
      (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⟫ : ℝ)
calc₄ :
  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
calc₅ :
  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
calc₆ :
  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
⊢ 0 ≤
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) * t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y

Tactic:
calc 0 ≤ re ⟪(ofReal t : 𝕜) • x + y, (ofReal t : 𝕜) • x + y⟫ := inner_self_nonneg
  _ = re (⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫ + ⟪(ofReal t : 𝕜) • x, y⟫
      + ⟪y, (ofReal t : 𝕜) • x⟫ + ⟪y, y⟫) := by rw [inner_add_add_self ((ofReal t : 𝕜) • x) y]
  _ = re ⟪(ofReal t : 𝕜) • x, (ofReal t : 𝕜) • x⟫
      + re ⟪(ofReal t : 𝕜) • x, y⟫ + re ⟪y, (ofReal t : 𝕜) • x⟫ + re ⟪y, y⟫ := by
      simp only [map_add]
  _ = normSq x * t * t + re (⟪x, y⟫ * t) + re (⟪y, x⟫ * t) + re ⟪y, y⟫ := by rw
    [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
  _ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + re ⟪y, y⟫ := by rw [mul_comm ⟪x, y⟫ _,
    RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]
  _ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + normSq y := by rw [← normSq]
  _ = normSq x * t * t + re ⟪x, y⟫ * t + re ⟪x, y⟫ * t + normSq y := by rw [inner_re_symm]
  _ = normSq x * t * t + 2 * re ⟪x, y⟫ * t + normSq y := by ring

Premises used: InnerProductSpace.Core.inner_self_nonneg, InnerProductSpace.Core.normSq