𝕜 : Type ?u.2712404
E : Type ?u.2712407
F : Type ?u.2712410
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ inner (↑T y) x =
    (inner (↑T x) x + inner (↑T y) x + (inner (↑T x) y + inner (↑T y) y) -
            (inner (↑T x) x - (inner (↑T y) x + (inner (↑T x) y - inner (↑T y) y))) +
          (Complex.I * inner (↑T x) x + inner (↑T y) x + (-inner (↑T x) y + Complex.I * inner (↑T y) y)) -
        (Complex.I * inner (↑T x) x - (inner (↑T y) x + (-inner (↑T x) y - Complex.I * inner (↑T y) y)))) /
      4
𝕜 : Type ?u.2712404
E : Type ?u.2712407
F : Type ?u.2712410
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ inner (↑T y) x =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) +
          Complex.I * inner (↑T (x + Complex.I • y)) (x + Complex.I • y) -
        Complex.I * inner (↑T (x - Complex.I • y)) (x - Complex.I • y)) /
      4
simp only [map_add, map_sub, inner_add_left, inner_add_right, LinearMap.map_smul, inner_smul_left,
  inner_smul_right, Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right,
  mul_add, ← mul_assoc, mul_neg, neg_neg, sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub]
no goals
𝕜 : Type ?u.2712404
E : Type ?u.2712407
F : Type ?u.2712410
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ inner (↑T y) x =
    (inner (↑T x) x + inner (↑T y) x + (inner (↑T x) y + inner (↑T y) y) -
            (inner (↑T x) x - (inner (↑T y) x + (inner (↑T x) y - inner (↑T y) y))) +
          (Complex.I * inner (↑T x) x + inner (↑T y) x + (-inner (↑T x) y + Complex.I * inner (↑T y) y)) -
        (Complex.I * inner (↑T x) x - (inner (↑T y) x + (-inner (↑T x) y - Complex.I * inner (↑T y) y)))) /
      4
ring