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
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_re]
-- 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
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_re]
-- 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
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_im]
-- 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
rw : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
have rw₁ : Eq (α := ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_im]
-- 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
r : 𝕜
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪y, x⟫) = r * ⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_smul_left]
-- 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 : F
⊢ ⟪0, x⟫ = 0
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0
Tactic: rw [← zero_smul 𝕜 (0 : F), inner_smul_left]
-- 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 : F
⊢ ⟪x, 0⟫ = 0
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)
Tactic: rw [← inner_conj_symm, inner_zero_left]
-- 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⟫‖
have rw : Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = ‖⟪y, x⟫‖
Tactic: rw [← inner_conj_symm, norm_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
rw : Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = ‖⟪y, x⟫‖
⊢ ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖
have rw₁ : ‖⟪y, x⟫‖ = ‖⟪y, x⟫‖
Tactic: rw [← inner_conj_symm, norm_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
⊢ ⟪-x, y⟫ = -⟪x, y⟫
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-1) : 𝕜) ⟪x, y⟫ = -⟪x, y⟫
Tactic: rw [← neg_one_smul 𝕜 x, inner_smul_left]
-- 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, y⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_neg_left]
-- 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
⊢ (re : (a : 𝕜) → ℝ) (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖
have rw : (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)) =
  ‖HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)‖
Tactic: rw [← inner_conj_symm, mul_comm]
-- 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 + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫
have simp : ⟪x, x⟫ + ⟪y, x⟫ + (⟪x, y⟫ + ⟪y, y⟫) = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫
Tactic: simp only [inner_add_left, inner_add_right]
-- 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 - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫
have simp : ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫
Tactic: simp only [inner_sub_left, inner_sub_right]
-- 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 : ℝ
⊢ ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑t : 𝕜) : 𝕜) ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
Tactic: rw [inner_smul_left, conj_ofReal, mul_comm]
-- 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 : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑t : 𝕜) : 𝕜) ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
⊢ ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
have rw₁ : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
Tactic: rw [inner_smul_left, conj_ofReal, mul_comm]
-- 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 : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑t : 𝕜) : 𝕜) ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
rw₁ : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
⊢ ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
have rw₂ : ⟪x, y⟫ * (↑t : 𝕜) = ⟪x, y⟫ * (↑t : 𝕜)
Tactic: rw [inner_smul_left, conj_ofReal, mul_comm]
-- 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 : ℝ
⊢ ⟪x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
have rw : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
Tactic: rw [inner_smul_right, mul_comm]
-- 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 : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
⊢ ⟪x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
have rw₁ : ⟪x, y⟫ * (↑t : 𝕜) = ⟪x, y⟫ * (↑t : 𝕜)
Tactic: rw [inner_smul_right, mul_comm]
-- 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 : ℝ
⊢ 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⟫) :
      ℝ)
have rw : Eq (α := ℝ)
  ((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⟫) :
    ℝ)
  ((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: rw [inner_add_add_self ((ofReal t : 𝕜) • x) 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
t : ℝ
⊢ 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⟫ : ℝ)
have 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⟫ : ℝ)
Tactic: rw
    [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
-- 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 : ℝ
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⟫ : ℝ)
⊢ 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⟫ : ℝ)
have 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⟫ : ℝ)
Tactic: rw
    [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
-- 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 : ℝ
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⟫ : ℝ)
⊢ 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⟫ : ℝ)
have 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⟫ : ℝ)
Tactic: rw
    [re_inner_smul_ofReal_smul_self, inner_smul_ofReal_left, inner_smul_ofReal_right]
-- 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 (β := ℝ)
      (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 (β := ℝ)
    (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⟫ : ℝ)
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 : ℝ
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⟫ : ℝ)
⊢ 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 (β := ℝ)
    (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⟫ : ℝ)
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 : ℝ
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⟫ : ℝ)
⊢ 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 (β := ℝ)
    (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⟫ : ℝ)
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 : ℝ
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⟫ : ℝ)
⊢ 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 (β := ℝ)
    (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⟫ : ℝ)
Tactic: rw [mul_comm ⟪x, y⟫ _,
    RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]