case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4

case inr
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
rcases@I_mul_I_ax 𝕜 _ with (h | h)
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(starRingEnd 𝕜) (inner (↑T y) x) =
    (inner x (↑T x) + ↑(starRingEnd 𝕜) (inner (↑T y) x) + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - ↑(starRingEnd 𝕜) (inner (↑T y) x) - (inner (↑T y) x - inner (↑T y) y))) /
      4
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
simp_rw [h, MulZeroClass.zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left,
  inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(starRingEnd 𝕜) (inner (↑T y) x) =
    (inner x (↑T x) + ↑(starRingEnd 𝕜) (inner (↑T y) x) + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - ↑(starRingEnd 𝕜) (inner (↑T y) x) - (inner (↑T y) x - inner (↑T y) y))) /
      4
suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
  rw [conj_eq_iff_re.mpr this]
  ring
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
this : ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
⊢ inner (↑T y) x =
    (inner x (↑T x) + inner (↑T y) x + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - inner (↑T y) x - (inner (↑T y) x - inner (↑T y) y))) /
      4
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
this : ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
⊢ ↑(starRingEnd 𝕜) (inner (↑T y) x) =
    (inner x (↑T x) + ↑(starRingEnd 𝕜) (inner (↑T y) x) + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - ↑(starRingEnd 𝕜) (inner (↑T y) x) - (inner (↑T y) x - inner (↑T y) y))) /
      4
rw [conj_eq_iff_re.mpr this]
no goals
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
this : ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
⊢ inner (↑T y) x =
    (inner x (↑T x) + inner (↑T y) x + (inner (↑T y) x + inner (↑T y) y) -
        (inner x (↑T x) - inner (↑T y) x - (inner (↑T y) x - inner (↑T y) y))) /
      4
ring
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I)) = ↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (inner (↑T y) x)) = inner (↑T y) x
rw [← re_add_im ⟪T y, x⟫]
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re ↑(↑re (inner (↑T y) x))) = ↑(↑re (inner (↑T y) x))
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re (↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I)) = ↑(↑re (inner (↑T y) x)) + ↑(↑im (inner (↑T y) x)) * I
simp_rw [h, MulZeroClass.mul_zero, add_zero]
no goals
case inl
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I = 0
⊢ ↑(↑re ↑(↑re (inner (↑T y) x))) = ↑(↑re (inner (↑T y) x))
norm_cast
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T x) x + inner (↑T x) y + (inner (↑T y) x + inner (↑T y) y) -
          (inner (↑T x) x - (inner (↑T x) y + (inner (↑T y) x - inner (↑T y) y)) +
            (I * inner (↑T x) x + -inner (↑T x) y + (inner (↑T y) x + I * inner (↑T y) y))) +
        (I * inner (↑T x) x - (-inner (↑T x) y + (inner (↑T y) x - I * inner (↑T y) y)))) /
      4
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T (x + y)) (x + y) - inner (↑T (x - y)) (x - y) - I * inner (↑T (x + I • y)) (x + I • y) +
        I * inner (↑T (x - I • y)) (x - I • y)) /
      4
simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right,
  LinearMap.map_smul, inner_smul_left, inner_smul_right, IsROrC.conj_I, mul_add, mul_sub,
  sub_sub, ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]
no goals
case inr
𝕜 : Type u_1
E : Type u_2
E' : Type ?u.137322
F : Type ?u.137325
G : Type ?u.137328
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℝ E'
T : E →ₗ[𝕜] E
hT : IsSymmetric T
x y : E
h : I * I = -1
⊢ inner (↑T x) y =
    (inner (↑T x) x + inner (↑T x) y + (inner (↑T y) x + inner (↑T y) y) -
          (inner (↑T x) x - (inner (↑T x) y + (inner (↑T y) x - inner (↑T y) y)) +
            (I * inner (↑T x) x + -inner (↑T x) y + (inner (↑T y) x + I * inner (↑T y) y))) +
        (I * inner (↑T x) x - (-inner (↑T x) y + (inner (↑T y) x - I * inner (↑T y) y)))) /
      4
ring