awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t) ((re : (a : 𝕜) → ℝ) ((↑t : 𝕜) * ⟪x, y⟫) : ℝ))
        ((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⟫ : ℝ)
rw₁ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ))
        ((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⟫ : ℝ)
rw₂ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((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⟫ : ℝ)
rw₃ :
  HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ) (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t)
        ((re : (a : 𝕜) → ℝ) ((↑t : 𝕜) * ⟪y, x⟫) : ℝ))
      ((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⟫ : ℝ)
⊢ 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⟫ : ℝ)
have rw₄ : HAdd.hAdd (β := ℝ)
    (normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) t +
      HMul.hMul (β := ℝ) t ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ))
    ((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⟫ : ℝ)
Tactic: rw [mul_comm ⟪x, y⟫ _,
    RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 : ℝ
⊢ 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
have 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
Tactic: rw [← normSq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 : 𝕜) → ℝ) ⟪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
have 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
Tactic: rw [inner_re_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 : ℝ
⊢ 0 ≤
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) * t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y
have 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⟫) :
    ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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⟫) :
      ℝ)
⊢ 0 ≤
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) * t +
      normSq.{u_1, u_3} (𝕜 := 𝕜) y
have 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⟫ : ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ 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)
have 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)) :
    𝕜)
Tactic: rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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, 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)) :
      𝕜)
have 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) :
    𝕜)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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, 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) :
      𝕜)
have 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) :
    𝕜)
Tactic: rw [← mul_assoc, mul_conj, RCLike.conj_mul, mul_left_comm, ← inner_conj_symm y, mul_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 * (normSq.{u_1, u_3} (𝕜 := 𝕜) x * normSq.{u_1, u_3} (𝕜 := 𝕜) y) -
          normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) :
      𝕜)
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have rw : ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: rw [norm_inner_symm y x]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
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
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have linarith₁ : HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) < ‖⟪x, y⟫‖ * ‖⟪x, y⟫‖ →
  GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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, y⟫‖ * ‖⟪y, x⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have suffices : discrim (normSq.{u_1, u_3} (𝕜 := 𝕜) x) (2 * ‖⟪x, y⟫‖) (normSq.{u_1, u_3} (𝕜 := 𝕜) y) ≤ 0
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
have refine : ∀ (t : ℝ), 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
Tactic: refine discrim_le_zero fun t ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 : ℝ
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have pos : ∀ (hzero : ⟪x, y⟫ = 0), 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have neg : ∀ (hzero : ¬⟪x, y⟫ = 0), 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have pos : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 + normSq.{u_1, u_3} (𝕜 := 𝕜) y
Tactic: simp only [← sq, hzero, norm_zero, mul_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
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 * HPow.hPow (β := ℕ) t 2 + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have hx : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x
Tactic: obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, inner_self_nonneg⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
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} (𝕜 := 𝕜) x * HPow.hPow (β := ℕ) t 2 + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have hy : 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) y
Tactic: obtain ⟨hx, hy⟩ : (0 ≤ normSqF x ∧ 0 ≤ normSqF y) := ⟨inner_self_nonneg, inner_self_nonneg⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
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 * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have hzero' : ‖⟪x, y⟫‖ ≠ 0
Tactic: have hzero' : ‖⟪x, y⟫‖ ≠ 0 := norm_ne_zero_iff.2 hzero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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 * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have h : normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) = normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖)
Tactic: convert! cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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⟫‖)
⊢ 0 ≤ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq.{u_1, u_3} (𝕜 := 𝕜) y
have h₁ : 2 * ‖⟪x, y⟫‖ * t = HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪⟪x, y⟫ • x, y⟫ : ℝ) * (t / ‖⟪x, y⟫‖)
Tactic: convert! cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
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
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) x * (t * t) = normSq.{u_1, u_3} (𝕜 := 𝕜) (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖)
have 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)
Tactic: field_simp