𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ inner (inner x y • x - inner x x • y) (inner x y • x - inner x x • y) =
    ↑(normSq x * (normSq x * normSq y - ‖inner x y‖ ^ 2))
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ normSq (inner x y • x - inner x x • y) = normSq x * (normSq x * normSq y - ‖inner x y‖ ^ 2)
rw [← @ofReal_inj 𝕜, ofReal_normSq_eq_inner_self]
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ inner x y * (↑(starRingEnd 𝕜) (inner x y) * ↑(normSq x)) - ↑(normSq x) * (↑(starRingEnd 𝕜) (inner x y) * inner x y) -
        inner x y * (↑(normSq x) * inner y x) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖inner x y‖ ^ 2)
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ inner (inner x y • x - inner x x • y) (inner x y • x - inner x x • y) =
    ↑(normSq x * (normSq x * normSq y - ‖inner x y‖ ^ 2))
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]
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑(‖inner x y‖ ^ 2) * ↑(normSq x) - ↑(normSq x) * ↑(‖inner x y‖ ^ 2) - ↑(normSq x) * ↑(‖inner x y‖ ^ 2) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖inner x y‖ ^ 2)
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ inner x y * (↑(starRingEnd 𝕜) (inner x y) * ↑(normSq x)) - ↑(normSq x) * (↑(starRingEnd 𝕜) (inner x y) * inner x y) -
        inner x y * (↑(normSq x) * inner y x) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖inner x y‖ ^ 2)
rw [← mul_assoc, mul_conj, IsROrC.conj_mul, normSq_eq_def', mul_left_comm, ← inner_conj_symm y,
  mul_conj, normSq_eq_def']
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑‖inner x y‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖inner x y‖ ^ 2 - ↑(normSq x) * ↑‖inner x y‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) - ↑(normSq x) * ↑‖inner x y‖ ^ 2
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑(‖inner x y‖ ^ 2) * ↑(normSq x) - ↑(normSq x) * ↑(‖inner x y‖ ^ 2) - ↑(normSq x) * ↑(‖inner x y‖ ^ 2) +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x * (normSq x * normSq y) - normSq x * ‖inner x y‖ ^ 2)
push_cast
no goals
𝕜 : Type u_1
E : Type ?u.645181
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑‖inner x y‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖inner x y‖ ^ 2 - ↑(normSq x) * ↑‖inner x y‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) - ↑(normSq x) * ↑‖inner x y‖ ^ 2
ring