[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ InnerProductSpaceable.innerProp' E ↑(-1)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ inner_ 𝕜 (↑(-1) • x) y = ↑(starRingEnd 𝕜) ↑(-1) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [inner_, neg_mul_eq_neg_mul, one_mul, Int.cast_one, one_smul, RingHom.map_one, map_neg, Int.cast_neg,
  neg_smul, neg_one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ 4⁻¹ *
      (↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
        I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖) =
    -4⁻¹ *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
rw [neg_mul_comm]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ 4⁻¹ *
      (↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
        I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖) =
    4⁻¹ *
      -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
          I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
      I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ‖-x - y‖ = ‖x + y‖
[PROOFSTEP]
rw [← neg_add', norm_neg]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
      I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ‖-x + y‖ = ‖x - y‖
[PROOFSTEP]
rw [← neg_sub, norm_neg, sub_eq_neg_add]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
      I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
have h₃ : ‖(I : 𝕜) • -x + y‖ = ‖(I : 𝕜) • x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add, ← smul_neg]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ‖I • -x + y‖ = ‖I • x - y‖
[PROOFSTEP]
rw [← neg_sub, norm_neg, sub_eq_neg_add, ← smul_neg]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
h₃ : ‖I • -x + y‖ = ‖I • x - y‖
⊢ ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
      I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
have h₄ : ‖(I : 𝕜) • -x - y‖ = ‖(I : 𝕜) • x + y‖ := by rw [smul_neg, ← neg_add', norm_neg]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
h₃ : ‖I • -x + y‖ = ‖I • x - y‖
⊢ ‖I • -x - y‖ = ‖I • x + y‖
[PROOFSTEP]
rw [smul_neg, ← neg_add', norm_neg]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
h₃ : ‖I • -x + y‖ = ‖I • x - y‖
h₄ : ‖I • -x - y‖ = ‖I • x + y‖
⊢ ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ - ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ + I * ↑𝓚 ‖I • -x + y‖ * ↑𝓚 ‖I • -x + y‖ -
      I * ↑𝓚 ‖I • -x - y‖ * ↑𝓚 ‖I • -x - y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
rw [h₁, h₂, h₃, h₄]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
h₃ : ‖I • -x + y‖ = ‖I • x - y‖
h₄ : ‖I • -x - y‖ = ‖I • x + y‖
⊢ ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ - ↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ + I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ -
      I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ =
    -(↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous fun x => _root_.inner_ 𝕜 (f x) (g x)
[PROOFSTEP]
unfold inner_
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
⊢ Continuous fun x =>
    4⁻¹ *
      (↑𝓚 ‖f x + g x‖ * ↑𝓚 ‖f x + g x‖ - ↑𝓚 ‖f x - g x‖ * ↑𝓚 ‖f x - g x‖ + I * ↑𝓚 ‖I • f x + g x‖ * ↑𝓚 ‖I • f x + g x‖ -
        I * ↑𝓚 ‖I • f x - g x‖ * ↑𝓚 ‖I • f x - g x‖)
[PROOFSTEP]
have := Continuous.const_smul (M := 𝕜) hf I
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : ℝ → E
hf : Continuous f
hg : Continuous g
this : Continuous fun x => I • f x
⊢ Continuous fun x =>
    4⁻¹ *
      (↑𝓚 ‖f x + g x‖ * ↑𝓚 ‖f x + g x‖ - ↑𝓚 ‖f x - g x‖ * ↑𝓚 ‖f x - g x‖ + I * ↑𝓚 ‖I • f x + g x‖ * ↑𝓚 ‖I • f x + g x‖ -
        I * ↑𝓚 ‖I • f x - g x‖ * ↑𝓚 ‖I • f x - g x‖)
[PROOFSTEP]
continuity
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ ^ 2 = ↑re (inner_ 𝕜 x x)
[PROOFSTEP]
simp only [inner_]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ ^ 2 =
    ↑re
      (4⁻¹ *
        (↑𝓚 ‖x + x‖ * ↑𝓚 ‖x + x‖ - ↑𝓚 ‖x - x‖ * ↑𝓚 ‖x - x‖ + I * ↑𝓚 ‖I • x + x‖ * ↑𝓚 ‖I • x + x‖ -
          I * ↑𝓚 ‖I • x - x‖ * ↑𝓚 ‖I • x - x‖))
[PROOFSTEP]
have h₁ : IsROrC.normSq (4 : 𝕜) = 16 :=
  by
  have : ((4 : ℝ) : 𝕜) = (4 : 𝕜) := by norm_cast
  rw [← this, normSq_eq_def', IsROrC.norm_of_nonneg (by norm_num : (0 : ℝ) ≤ 4)]
  norm_num
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ↑normSq 4 = 16
[PROOFSTEP]
have : ((4 : ℝ) : 𝕜) = (4 : 𝕜) := by norm_cast
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ↑4 = 4
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
this : ↑4 = 4
⊢ ↑normSq 4 = 16
[PROOFSTEP]
rw [← this, normSq_eq_def', IsROrC.norm_of_nonneg (by norm_num : (0 : ℝ) ≤ 4)]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
this : ↑4 = 4
⊢ 0 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
this : ↑4 = 4
⊢ 4 ^ 2 = 16
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ↑normSq 4 = 16
⊢ ‖x‖ ^ 2 =
    ↑re
      (4⁻¹ *
        (↑𝓚 ‖x + x‖ * ↑𝓚 ‖x + x‖ - ↑𝓚 ‖x - x‖ * ↑𝓚 ‖x - x‖ + I * ↑𝓚 ‖I • x + x‖ * ↑𝓚 ‖I • x + x‖ -
          I * ↑𝓚 ‖I • x - x‖ * ↑𝓚 ‖I • x - x‖))
[PROOFSTEP]
have h₂ : ‖x + x‖ = 2 * ‖x‖ := by rw [← two_smul 𝕜, norm_smul, IsROrC.norm_two]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ↑normSq 4 = 16
⊢ ‖x + x‖ = 2 * ‖x‖
[PROOFSTEP]
rw [← two_smul 𝕜, norm_smul, IsROrC.norm_two]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ↑normSq 4 = 16
h₂ : ‖x + x‖ = 2 * ‖x‖
⊢ ‖x‖ ^ 2 =
    ↑re
      (4⁻¹ *
        (↑𝓚 ‖x + x‖ * ↑𝓚 ‖x + x‖ - ↑𝓚 ‖x - x‖ * ↑𝓚 ‖x - x‖ + I * ↑𝓚 ‖I • x + x‖ * ↑𝓚 ‖I • x + x‖ -
          I * ↑𝓚 ‖I • x - x‖ * ↑𝓚 ‖I • x - x‖))
[PROOFSTEP]
simp only [h₁, h₂, algebraMap_eq_ofReal, sub_self, norm_zero, mul_re, inv_re, ofNat_re, map_sub, map_add, ofReal_re,
  ofNat_im, ofReal_im, mul_im, I_re, inv_im]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ↑normSq 4 = 16
h₂ : ‖x + x‖ = 2 * ‖x‖
⊢ ‖x‖ ^ 2 =
    4 / 16 *
        (2 * ‖x‖ * (2 * ‖x‖) - 0 * 0 - 0 +
            ((0 * ‖I • x + x‖ - ↑im I * 0) * ‖I • x + x‖ - (0 * 0 + ↑im I * ‖I • x + x‖) * 0) -
          ((0 * ‖I • x - x‖ - ↑im I * 0) * ‖I • x - x‖ - (0 * 0 + ↑im I * ‖I • x - x‖) * 0)) -
      -0 / 16 *
        (2 * ‖x‖ * 0 + 0 * (2 * ‖x‖) - (0 * 0 + 0 * 0) +
            ((0 * ‖I • x + x‖ - ↑im I * 0) * 0 + (0 * 0 + ↑im I * ‖I • x + x‖) * ‖I • x + x‖) -
          ((0 * ‖I • x - x‖ - ↑im I * 0) * 0 + (0 * 0 + ↑im I * ‖I • x - x‖) * ‖I • x - x‖))
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑(starRingEnd 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y
[PROOFSTEP]
simp only [inner_]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑(starRingEnd 𝕜)
      (4⁻¹ *
        (↑𝓚 ‖y + x‖ * ↑𝓚 ‖y + x‖ - ↑𝓚 ‖y - x‖ * ↑𝓚 ‖y - x‖ + I * ↑𝓚 ‖I • y + x‖ * ↑𝓚 ‖I • y + x‖ -
          I * ↑𝓚 ‖I • y - x‖ * ↑𝓚 ‖I • y - x‖)) =
    4⁻¹ *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
have h4 : conj (4⁻¹ : 𝕜) = 4⁻¹ := by norm_num
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
⊢ ↑(starRingEnd 𝕜)
      (4⁻¹ *
        (↑𝓚 ‖y + x‖ * ↑𝓚 ‖y + x‖ - ↑𝓚 ‖y - x‖ * ↑𝓚 ‖y - x‖ + I * ↑𝓚 ‖I • y + x‖ * ↑𝓚 ‖I • y + x‖ -
          I * ↑𝓚 ‖I • y - x‖ * ↑𝓚 ‖I • y - x‖)) =
    4⁻¹ *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
rw [map_mul, h4]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
⊢ 4⁻¹ *
      ↑(starRingEnd 𝕜)
        (↑𝓚 ‖y + x‖ * ↑𝓚 ‖y + x‖ - ↑𝓚 ‖y - x‖ * ↑𝓚 ‖y - x‖ + I * ↑𝓚 ‖I • y + x‖ * ↑𝓚 ‖I • y + x‖ -
          I * ↑𝓚 ‖I • y - x‖ * ↑𝓚 ‖I • y - x‖) =
    4⁻¹ *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
⊢ ↑(starRingEnd 𝕜)
      (↑𝓚 ‖y + x‖ * ↑𝓚 ‖y + x‖ - ↑𝓚 ‖y - x‖ * ↑𝓚 ‖y - x‖ + I * ↑𝓚 ‖I • y + x‖ * ↑𝓚 ‖I • y + x‖ -
        I * ↑𝓚 ‖I • y - x‖ * ↑𝓚 ‖I • y - x‖) =
    ↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
      I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖
[PROOFSTEP]
simp only [map_sub, map_add, algebraMap_eq_ofReal, ← ofReal_mul, conj_ofReal, map_mul, conj_I]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
⊢ ↑(‖y + x‖ * ‖y + x‖) - ↑(‖y - x‖ * ‖y - x‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
rw [add_comm y x, norm_sub_rev]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
by_cases hI : (I : 𝕜) = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : I = 0
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
simp only [hI, neg_zero, zero_mul]
  -- Porting note: this replaces `norm_I_of_ne_zero` which does not exist in Lean 4
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
have : ‖(I : 𝕜)‖ = 1 := by
  rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul, I_mul_I_of_nonzero hI, norm_neg,
    norm_one]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
⊢ ‖I‖ = 1
[PROOFSTEP]
rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul, I_mul_I_of_nonzero hI, norm_neg,
  norm_one]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ :=
  by
  trans ‖(I : 𝕜) • ((I : 𝕜) • y - x)‖
  · rw [norm_smul, this, one_mul]
  · rw [smul_sub, smul_smul, I_mul_I_of_nonzero hI, neg_one_smul, ← neg_add', add_comm, norm_neg]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
⊢ ‖I • y - x‖ = ‖I • x + y‖
[PROOFSTEP]
trans ‖(I : 𝕜) • ((I : 𝕜) • y - x)‖
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
⊢ ‖I • y - x‖ = ‖I • (I • y - x)‖
[PROOFSTEP]
rw [norm_smul, this, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
⊢ ‖I • (I • y - x)‖ = ‖I • x + y‖
[PROOFSTEP]
rw [smul_sub, smul_smul, I_mul_I_of_nonzero hI, neg_one_smul, ← neg_add', add_comm, norm_neg]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
have h₂ : ‖(I : 𝕜) • y + x‖ = ‖(I : 𝕜) • x - y‖ :=
  by
  trans ‖(I : 𝕜) • ((I : 𝕜) • y + x)‖
  · rw [norm_smul, this, one_mul]
  · rw [smul_add, smul_smul, I_mul_I_of_nonzero hI, neg_one_smul, ← neg_add_eq_sub]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ ‖I • y + x‖ = ‖I • x - y‖
[PROOFSTEP]
trans ‖(I : 𝕜) • ((I : 𝕜) • y + x)‖
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ ‖I • y + x‖ = ‖I • (I • y + x)‖
[PROOFSTEP]
rw [norm_smul, this, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
⊢ ‖I • (I • y + x)‖ = ‖I • x - y‖
[PROOFSTEP]
rw [smul_add, smul_smul, I_mul_I_of_nonzero hI, neg_one_smul, ← neg_add_eq_sub]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
h₂ : ‖I • y + x‖ = ‖I • x - y‖
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ - -I * ↑‖I • y - x‖ * ↑‖I • y - x‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
rw [h₁, h₂, ← sub_add_eq_add_sub]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
h4 : ↑(starRingEnd 𝕜) 4⁻¹ = 4⁻¹
hI : ¬I = 0
this : ‖I‖ = 1
h₁ : ‖I • y - x‖ = ‖I • x + y‖
h₂ : ‖I • y + x‖ = ‖I • x - y‖
⊢ ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) - -I * ↑‖I • x + y‖ * ↑‖I • x + y‖ + -I * ↑‖I • x - y‖ * ↑‖I • x - y‖ =
    ↑(‖x + y‖ * ‖x + y‖) - ↑(‖x - y‖ * ‖x - y‖) + I * ↑‖I • x + y‖ * ↑‖I • x + y‖ - I * ↑‖I • x - y‖ * ↑‖I • x - y‖
[PROOFSTEP]
simp only [neg_mul, sub_eq_add_neg, neg_neg]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖x + y + z‖ * ‖x + y + z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) / 2 - ‖x - z‖ * ‖x - z‖
[PROOFSTEP]
rw [eq_sub_iff_add_eq, eq_div_iff (two_ne_zero' ℝ), mul_comm _ (2 : ℝ), eq_comm]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
[PROOFSTEP]
convert parallelogram_identity (x + y + z) (x - z) using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ 2 • x + y = x + y + z + (x - z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ x + x + y = x + y + z + (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ x + x + y = x + y + z + (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ 2 • x + y = x + y + z + (x - z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ x + x + y = x + y + z + (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ x + x + y = x + y + z + (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ 2 • z + y = x + y + z - (x - z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ z + z + y = x + y + z - (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ z + z + y = x + y + z - (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ 2 • z + y = x + y + z - (x - z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ z + z + y = x + y + z - (x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ z + z + y = x + y + z - (x - z)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖x + y - z‖ * ‖x + y - z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 - ‖x + z‖ * ‖x + z‖
[PROOFSTEP]
rw [eq_sub_iff_add_eq, eq_div_iff (two_ne_zero' ℝ), mul_comm _ (2 : ℝ), eq_comm]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity (x + y - z) (x + z)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ ‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ 2 • x + y = x + y - z + (x + z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ x + x + y = x + y - z + (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ x + x + y = x + y - z + (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ 2 • x + y = x + y - z + (x + z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ x + x + y = x + y - z + (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ x + x + y = x + y - z + (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - 2 • z = x + y - z - (x + z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - (z + z) = x + y - z - (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - (z + z) = x + y - z - (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - 2 • z = x + y - z - (x + z)
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - (z + z) = x + y - z - (x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
⊢ y - (z + z) = x + y - z - (x + z)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖x + y + z‖ * ‖x + y + z‖ - ‖x + y - z‖ * ‖x + y - z‖ =
    ‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2
[PROOFSTEP]
rw [add_left_aux1, add_left_aux2]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ (‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) / 2 - ‖x - z‖ * ‖x - z‖ -
      ((‖2 • x + y‖ * ‖2 • x + y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 - ‖x + z‖ * ‖x + z‖) =
    ‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
[PROOFSTEP]
apply eq_sub_of_add_eq
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖2 • z + y‖ * ‖2 • z + y‖ + ‖y‖ * ‖y‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
convert parallelogram_identity (y + z) z using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ 2 • z + y = y + z + z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ 2 • z + y = y + z + z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ 2 • z + y = y + z + z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ 2 • z + y = y + z + z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ z + z + y = y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ z + z + y = y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ z + z + y = y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ z + z + y = y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ y = y + z - z
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖
[PROOFSTEP]
apply eq_sub_of_add_eq'
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity (y - z) z
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ ‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - 2 • z = y - z - z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - 2 • z = y - z - z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - 2 • z = y - z - z
[PROOFSTEP]
try rw [two_smul]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - 2 • z = y - z - z
[PROOFSTEP]
rw [two_smul]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y = y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - (z + z) = y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - (z + z) = y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - (z + z) = y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
⊢ y - (z + z) = y - z - z
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ (‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 = ‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖
[PROOFSTEP]
rw [add_left_aux3, add_left_aux4]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ (2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖ - (2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖)) / 2 =
    ‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ =
    (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖) / 2 - ‖I • x - z‖ * ‖I • x - z‖
[PROOFSTEP]
rw [eq_sub_iff_add_eq, eq_div_iff (two_ne_zero' ℝ), mul_comm _ (2 : ℝ), eq_comm]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity ((I : 𝕜) • (x + y) + z) ((I : 𝕜) • x - z)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • (2 • x + y) = I • (x + y) + z + (I • x - z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • (2 • x + y) = I • (x + y) + z + (I • x - z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • x + I • x + I • y = I • x + I • y + z + (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • x + I • x + I • y = I • x + I • y + z + (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • (2 • x + y) = I • (x + y) + z + (I • x - z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • (2 • x + y) = I • (x + y) + z + (I • x - z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • x + I • x + I • y = I • x + I • y + z + (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • x + I • x + I • y = I • x + I • y + z + (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + 2 • z = I • (x + y) + z - (I • x - z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + 2 • z = I • (x + y) + z - (I • x - z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + (z + z) = I • x + I • y + z - (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + (z + z) = I • x + I • y + z - (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + 2 • z = I • (x + y) + z - (I • x - z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + 2 • z = I • (x + y) + z - (I • x - z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + (z + z) = I • x + I • y + z - (I • x - z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) + z + (I • x - z)‖ * ‖I • (x + y) + z + (I • x - z)‖ +
      ‖I • (x + y) + z - (I • x - z)‖ * ‖I • (x + y) + z - (I • x - z)‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)
⊢ I • y + (z + z) = I • x + I • y + z - (I • x - z)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ =
    (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖) / 2 - ‖I • x + z‖ * ‖I • x + z‖
[PROOFSTEP]
rw [eq_sub_iff_add_eq, eq_div_iff (two_ne_zero' ℝ), mul_comm _ (2 : ℝ), eq_comm]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity ((I : 𝕜) • (x + y) - z) ((I : 𝕜) • x + z)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • (2 • x + y) = I • (x + y) - z + (I • x + z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • (2 • x + y) = I • (x + y) - z + (I • x + z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • x + I • x + I • y = I • x + I • y - z + (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • x + I • x + I • y = I • x + I • y - z + (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • (2 • x + y) = I • (x + y) - z + (I • x + z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • (2 • x + y) = I • (x + y) - z + (I • x + z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • x + I • x + I • y = I • x + I • y - z + (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • x + I • x + I • y = I • x + I • y - z + (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - 2 • z = I • (x + y) - z - (I • x + z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - 2 • z = I • (x + y) - z - (I • x + z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - (z + z) = I • x + I • y - z - (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - (z + z) = I • x + I • y - z - (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - 2 • z = I • (x + y) - z - (I • x + z)
[PROOFSTEP]
try simp only [two_smul, smul_add]; abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - 2 • z = I • (x + y) - z - (I • x + z)
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - (z + z) = I • x + I • y - z - (I • x + z)
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
h₀ :
  ‖I • (x + y) - z + (I • x + z)‖ * ‖I • (x + y) - z + (I • x + z)‖ +
      ‖I • (x + y) - z - (I • x + z)‖ * ‖I • (x + y) - z - (I • x + z)‖ =
    2 * (‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ + ‖I • x + z‖ * ‖I • x + z‖)
⊢ I • y - (z + z) = I • x + I • y - z - (I • x + z)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖
[PROOFSTEP]
apply eq_sub_of_add_eq
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity ((I : 𝕜) • y + z) z
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ + ‖I • y‖ * ‖I • y‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + 2 • z = I • y + z + z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + 2 • z = I • y + z + z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + (z + z) = I • y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + (z + z) = I • y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + 2 • z = I • y + z + z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + 2 • z = I • y + z + z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + (z + z) = I • y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y + (z + z) = I • y + z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y + z + z‖ * ‖I • y + z + z‖ + ‖I • y + z - z‖ * ‖I • y + z - z‖ = 2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y + z - z
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖
[PROOFSTEP]
apply eq_sub_of_add_eq'
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
have h₀ := parallelogram_identity ((I : 𝕜) • y - z) z
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ ‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
[PROOFSTEP]
convert h₀ using 4
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_5.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y = I • y - z + z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - 2 • z = I • y - z - z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - 2 • z = I • y - z - z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - (z + z) = I • y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_5.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - (z + z) = I • y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - 2 • z = I • y - z - z
[PROOFSTEP]
try simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - 2 • z = I • y - z - z
[PROOFSTEP]
simp only [two_smul, smul_add]
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - (z + z) = I • y - z - z
[PROOFSTEP]
abel
[GOAL]
case h.e'_2.h.e'_6.h.e'_6.h.e'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
h₀ : ‖I • y - z + z‖ * ‖I • y - z + z‖ + ‖I • y - z - z‖ * ‖I • y - z - z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)
⊢ I • y - (z + z) = I • y - z - z
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z
[PROOFSTEP]
simp only [inner_, ← mul_add]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ 4⁻¹ *
      (↑𝓚 ‖x + y + z‖ * ↑𝓚 ‖x + y + z‖ - ↑𝓚 ‖x + y - z‖ * ↑𝓚 ‖x + y - z‖ +
          I * ↑𝓚 ‖I • (x + y) + z‖ * ↑𝓚 ‖I • (x + y) + z‖ -
        I * ↑𝓚 ‖I • (x + y) - z‖ * ↑𝓚 ‖I • (x + y) - z‖) =
    4⁻¹ *
      (↑𝓚 ‖x + z‖ * ↑𝓚 ‖x + z‖ - ↑𝓚 ‖x - z‖ * ↑𝓚 ‖x - z‖ + I * ↑𝓚 ‖I • x + z‖ * ↑𝓚 ‖I • x + z‖ -
          I * ↑𝓚 ‖I • x - z‖ * ↑𝓚 ‖I • x - z‖ +
        (↑𝓚 ‖y + z‖ * ↑𝓚 ‖y + z‖ - ↑𝓚 ‖y - z‖ * ↑𝓚 ‖y - z‖ + I * ↑𝓚 ‖I • y + z‖ * ↑𝓚 ‖I • y + z‖ -
          I * ↑𝓚 ‖I • y - z‖ * ↑𝓚 ‖I • y - z‖))
[PROOFSTEP]
congr
[GOAL]
case e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ↑𝓚 ‖x + y + z‖ * ↑𝓚 ‖x + y + z‖ - ↑𝓚 ‖x + y - z‖ * ↑𝓚 ‖x + y - z‖ + I * ↑𝓚 ‖I • (x + y) + z‖ * ↑𝓚 ‖I • (x + y) + z‖ -
      I * ↑𝓚 ‖I • (x + y) - z‖ * ↑𝓚 ‖I • (x + y) - z‖ =
    ↑𝓚 ‖x + z‖ * ↑𝓚 ‖x + z‖ - ↑𝓚 ‖x - z‖ * ↑𝓚 ‖x - z‖ + I * ↑𝓚 ‖I • x + z‖ * ↑𝓚 ‖I • x + z‖ -
        I * ↑𝓚 ‖I • x - z‖ * ↑𝓚 ‖I • x - z‖ +
      (↑𝓚 ‖y + z‖ * ↑𝓚 ‖y + z‖ - ↑𝓚 ‖y - z‖ * ↑𝓚 ‖y - z‖ + I * ↑𝓚 ‖I • y + z‖ * ↑𝓚 ‖I • y + z‖ -
        I * ↑𝓚 ‖I • y - z‖ * ↑𝓚 ‖I • y - z‖)
[PROOFSTEP]
simp only [mul_assoc, ← map_mul, add_sub_assoc, ← mul_sub, ← map_sub]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ↑𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) +
      I * ↑𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) =
    ↑𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖) + I * ↑𝓚 (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖) +
      (↑𝓚 (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖) + I * ↑𝓚 (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
[PROOFSTEP]
rw [add_add_add_comm]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ↑𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) +
      I * ↑𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) =
    ↑𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖) + ↑𝓚 (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖) +
      (I * ↑𝓚 (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖) +
        I * ↑𝓚 (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
[PROOFSTEP]
simp only [← map_add, ← mul_add]
[GOAL]
case e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ↑𝓚 (‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖) +
      I * ↑𝓚 (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖) =
    ↑𝓚 (‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖)) +
      I *
        ↑𝓚
          (‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖ +
            (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.h.e_6.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖x + y + z‖ * ‖x + y + z‖ - ‖x + (y - z)‖ * ‖x + (y - z)‖ =
    ‖x + z‖ * ‖x + z‖ - ‖x - z‖ * ‖x - z‖ + (‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖)
[PROOFSTEP]
rw [← add_sub_assoc, add_left_aux2', add_left_aux4']
[GOAL]
case e_a.e_a.e_a.h.e_6.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ - ‖I • (x + y) - z‖ * ‖I • (x + y) - z‖ =
    ‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖ + (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖)
[PROOFSTEP]
rw [add_left_aux5, add_left_aux6, add_left_aux7, add_left_aux8]
[GOAL]
case e_a.e_a.e_a.h.e_6.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + (2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖)) / 2 -
        ‖I • x - z‖ * ‖I • x - z‖ -
      ((‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + (2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖)) / 2 -
        ‖I • x + z‖ * ‖I • x + z‖) =
    ‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖ + (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖)
[PROOFSTEP]
simp only [map_sub, map_mul, map_add, div_eq_mul_inv]
[GOAL]
case e_a.e_a.e_a.h.e_6.h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ (‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + (2 * (‖I • y + z‖ * ‖I • y + z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖)) * 2⁻¹ -
        ‖I • x - z‖ * ‖I • x - z‖ -
      ((‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + (2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖) - ‖I • y‖ * ‖I • y‖)) *
          2⁻¹ -
        ‖I • x + z‖ * ‖I • x + z‖) =
    ‖I • x + z‖ * ‖I • x + z‖ - ‖I • x - z‖ * ‖I • x - z‖ + (‖I • y + z‖ * ‖I • y + z‖ - ‖I • y - z‖ * ‖I • y - z‖)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℕ
x y : E
⊢ inner_ 𝕜 (↑n • x) y = ↑n * inner_ 𝕜 x y
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ inner_ 𝕜 (↑Nat.zero • x) y = ↑Nat.zero * inner_ 𝕜 x y
[PROOFSTEP]
simp only [inner_, Nat.zero_eq, zero_sub, Nat.cast_zero, zero_mul, eq_self_iff_true, zero_smul, zero_add, mul_zero,
  sub_self, norm_neg, smul_zero]
[GOAL]
case succ
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
n : ℕ
ih : inner_ 𝕜 (↑n • x) y = ↑n * inner_ 𝕜 x y
⊢ inner_ 𝕜 (↑(Nat.succ n) • x) y = ↑(Nat.succ n) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [Nat.cast_succ, add_smul, one_smul]
[GOAL]
case succ
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
n : ℕ
ih : inner_ 𝕜 (↑n • x) y = ↑n * inner_ 𝕜 x y
⊢ inner_ 𝕜 (↑n • x + x) y = (↑n + 1) * inner_ 𝕜 x y
[PROOFSTEP]
rw [add_left, ih, add_mul, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℕ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
simp only [map_natCast]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℕ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = ↑r * inner_ 𝕜 x y
[PROOFSTEP]
exact nat r x y
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
⊢ InnerProductSpaceable.innerProp' E ↑n
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
⊢ inner_ 𝕜 (↑n • x) y = ↑(starRingEnd 𝕜) ↑n * inner_ 𝕜 x y
[PROOFSTEP]
rw [← n.sign_mul_natAbs]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
⊢ inner_ 𝕜 (↑(Int.sign n * ↑(Int.natAbs n)) • x) y = ↑(starRingEnd 𝕜) ↑(Int.sign n * ↑(Int.natAbs n)) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [Int.cast_ofNat, map_natCast, map_intCast, Int.cast_mul, map_mul, mul_smul]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
⊢ inner_ 𝕜 (↑(Int.sign n) • ↑(Int.natAbs n) • x) y = ↑(Int.sign n) * ↑(Int.natAbs n) * inner_ 𝕜 x y
[PROOFSTEP]
obtain hn | rfl | hn := lt_trichotomy n 0
[GOAL]
case inl
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
hn : n < 0
⊢ inner_ 𝕜 (↑(Int.sign n) • ↑(Int.natAbs n) • x) y = ↑(Int.sign n) * ↑(Int.natAbs n) * inner_ 𝕜 x y
[PROOFSTEP]
rw [Int.sign_eq_neg_one_of_neg hn, innerProp_neg_one ((n.natAbs : 𝕜) • x), nat]
[GOAL]
case inl
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
hn : n < 0
⊢ ↑(starRingEnd 𝕜) ↑(-1) * (↑(Int.natAbs n) * inner_ 𝕜 x y) = ↑(-1) * ↑(Int.natAbs n) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [map_neg, neg_mul, one_mul, mul_eq_mul_left_iff, true_or_iff, Int.natAbs_eq_zero, eq_self_iff_true,
  Int.cast_one, map_one, neg_inj, Nat.cast_eq_zero, Int.cast_neg]
[GOAL]
case inr.inl
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ inner_ 𝕜 (↑(Int.sign 0) • ↑(Int.natAbs 0) • x) y = ↑(Int.sign 0) * ↑(Int.natAbs 0) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [inner_, Int.cast_zero, zero_sub, Nat.cast_zero, zero_mul, eq_self_iff_true, Int.sign_zero, zero_smul,
  zero_add, mul_zero, smul_zero, sub_self, norm_neg, Int.natAbs_zero]
[GOAL]
case inr.inr
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
hn : 0 < n
⊢ inner_ 𝕜 (↑(Int.sign n) • ↑(Int.natAbs n) • x) y = ↑(Int.sign n) * ↑(Int.natAbs n) * inner_ 𝕜 x y
[PROOFSTEP]
rw [Int.sign_eq_one_of_pos hn]
[GOAL]
case inr.inr
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
n : ℤ
x y : E
hn : 0 < n
⊢ inner_ 𝕜 (↑1 • ↑(Int.natAbs n) • x) y = ↑1 * ↑(Int.natAbs n) * inner_ 𝕜 x y
[PROOFSTEP]
simp only [one_mul, mul_eq_mul_left_iff, true_or_iff, Int.natAbs_eq_zero, eq_self_iff_true, Int.cast_one, one_smul,
  Nat.cast_eq_zero, nat]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
⊢ InnerProductSpaceable.innerProp' E ↑r
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
have : (r.den : 𝕜) ≠ 0 := by
  haveI : CharZero 𝕜 := IsROrC.charZero_isROrC
  exact_mod_cast r.pos.ne'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
⊢ ↑r.den ≠ 0
[PROOFSTEP]
haveI : CharZero 𝕜 := IsROrC.charZero_isROrC
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
this : CharZero 𝕜
⊢ ↑r.den ≠ 0
[PROOFSTEP]
exact_mod_cast r.pos.ne'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
this : ↑r.den ≠ 0
⊢ inner_ 𝕜 (↑r • x) y = ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
rw [← r.num_div_den, ← mul_right_inj' this, ← nat r.den _ y, smul_smul, Rat.cast_div]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
this : ↑r.den ≠ 0
⊢ inner_ 𝕜 ((↑r.den * (↑↑r.num / ↑↑r.den)) • x) y = ↑r.den * (↑(starRingEnd 𝕜) (↑↑r.num / ↑↑r.den) * inner_ 𝕜 x y)
[PROOFSTEP]
simp only [map_natCast, Rat.cast_coe_nat, map_intCast, Rat.cast_coe_int, map_div₀]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
this : ↑r.den ≠ 0
⊢ inner_ 𝕜 ((↑r.den * (↑r.num / ↑r.den)) • x) y = ↑r.den * (↑r.num / ↑r.den * inner_ 𝕜 x y)
[PROOFSTEP]
rw [← mul_assoc, mul_div_cancel' _ this, int_prop _ x, map_intCast]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℝ
⊢ InnerProductSpaceable.innerProp' E ↑r
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℝ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
revert r
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ ∀ (r : ℝ), inner_ 𝕜 (↑r • x) y = ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
rw [← Function.funext_iff]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ (fun r => inner_ 𝕜 (↑r • x) y) = fun r => ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
refine' Rat.denseEmbedding_coe_real.dense.equalizer _ _ (funext fun X => _)
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ Continuous fun r => inner_ 𝕜 (↑r • x) y
[PROOFSTEP]
exact (continuous_ofReal.smul continuous_const).inner_ continuous_const
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ Continuous fun r => ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
[PROOFSTEP]
exact (continuous_conj.comp continuous_ofReal).mul continuous_const
[GOAL]
case refine'_3
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
X : ℚ
⊢ ((fun r => inner_ 𝕜 (↑r • x) y) ∘ Rat.cast) X = ((fun r => ↑(starRingEnd 𝕜) ↑r * inner_ 𝕜 x y) ∘ Rat.cast) X
[PROOFSTEP]
simp only [Function.comp_apply, IsROrC.ofReal_ratCast, rat_prop _ _]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
⊢ InnerProductSpaceable.innerProp' E I
[PROOFSTEP]
by_cases hI : (I : 𝕜) = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E I
[PROOFSTEP]
rw [hI, ← Nat.cast_zero]
[GOAL]
case pos
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E ↑0
[PROOFSTEP]
exact nat_prop _
[GOAL]
case neg
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
⊢ InnerProductSpaceable.innerProp' E I
[PROOFSTEP]
intro x y
[GOAL]
case neg
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
⊢ inner_ 𝕜 (I • x) y = ↑(starRingEnd 𝕜) I * inner_ 𝕜 x y
[PROOFSTEP]
have hI' : (-I : 𝕜) * I = 1 := by rw [← inv_I, inv_mul_cancel hI]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
⊢ -I * I = 1
[PROOFSTEP]
rw [← inv_I, inv_mul_cancel hI]
[GOAL]
case neg
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ inner_ 𝕜 (I • x) y = ↑(starRingEnd 𝕜) I * inner_ 𝕜 x y
[PROOFSTEP]
rw [conj_I, inner_, inner_, mul_left_comm]
[GOAL]
case neg
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ 4⁻¹ *
      (↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖I • I • x + y‖ * ↑𝓚 ‖I • I • x + y‖ -
        I * ↑𝓚 ‖I • I • x - y‖ * ↑𝓚 ‖I • I • x - y‖) =
    4⁻¹ *
      (-I *
        (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
          I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖))
[PROOFSTEP]
congr 1
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖I • I • x + y‖ * ↑𝓚 ‖I • I • x + y‖ -
      I * ↑𝓚 ‖I • I • x - y‖ * ↑𝓚 ‖I • I • x - y‖ =
    -I *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
rw [smul_smul, I_mul_I_of_nonzero hI, neg_one_smul]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ -
      I * ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ =
    -I *
      (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ - ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ + I * ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
        I * ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖)
[PROOFSTEP]
rw [mul_sub, mul_add, mul_sub, mul_assoc I (𝓚 ‖I • x - y‖), ← mul_assoc (-I) I, hI', one_mul,
  mul_assoc I (𝓚 ‖I • x + y‖), ← mul_assoc (-I) I, hI', one_mul]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ -
      I * ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ =
    -I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖) - -I * (↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
      ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖
[PROOFSTEP]
have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
⊢ ‖-x - y‖ = ‖x + y‖
[PROOFSTEP]
rw [← neg_add', norm_neg]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ -
      I * ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ =
    -I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖) - -I * (↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
      ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖
[PROOFSTEP]
have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ‖-x + y‖ = ‖x - y‖
[PROOFSTEP]
rw [← neg_sub, norm_neg, sub_eq_neg_add]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖-x + y‖ * ↑𝓚 ‖-x + y‖ -
      I * ↑𝓚 ‖-x - y‖ * ↑𝓚 ‖-x - y‖ =
    -I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖) - -I * (↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
      ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ - ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖ + I * ↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖ -
      I * ↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖ =
    -I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖) - -I * (↑𝓚 ‖x - y‖ * ↑𝓚 ‖x - y‖) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ -
      ↑𝓚 ‖I • x - y‖ * ↑𝓚 ‖I • x - y‖
[PROOFSTEP]
simp only [sub_eq_add_neg, mul_assoc]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ + -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖) + I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖) +
      -(I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖)) =
    -I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖) + -(-I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖)) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ +
      -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖)
[PROOFSTEP]
rw [← neg_mul_eq_neg_mul, ← neg_mul_eq_neg_mul]
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ + -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖) + I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖) +
      -(I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖)) =
    -(I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖)) + - -(I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖)) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ +
      -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖)
[PROOFSTEP]
abel
[GOAL]
case neg.e_a
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : -I * I = 1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ + -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖) + I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖) +
      -(I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖)) =
    -(I * (↑𝓚 ‖x + y‖ * ↑𝓚 ‖x + y‖)) + - -(I * (↑𝓚 ‖x + -y‖ * ↑𝓚 ‖x + -y‖)) + ↑𝓚 ‖I • x + y‖ * ↑𝓚 ‖I • x + y‖ +
      -(↑𝓚 ‖I • x + -y‖ * ↑𝓚 ‖I • x + -y‖)
[PROOFSTEP]
abel
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
⊢ InnerProductSpaceable.innerProp' E r
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ inner_ 𝕜 (r • x) y = ↑(starRingEnd 𝕜) r * inner_ 𝕜 x y
[PROOFSTEP]
rw [← re_add_im r, add_smul, add_left, real_prop _ x, ← smul_smul, real_prop _ _ y, I_prop, map_add, map_mul,
  conj_ofReal, conj_ofReal, conj_I]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ ↑(↑re r) * inner_ 𝕜 x y + ↑(↑im r) * (-I * inner_ 𝕜 x y) = (↑(↑re r) + ↑(↑im r) * -I) * inner_ 𝕜 x y
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : InnerProductSpaceable E
inst✝ : NormedSpace ℝ E
⊢ UniformConvexSpace E
[PROOFSTEP]
cases nonempty_innerProductSpace ℝ E
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : IsROrC 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : InnerProductSpaceable E
inst✝ : NormedSpace ℝ E
val✝ : InnerProductSpace ℝ E
⊢ UniformConvexSpace E
[PROOFSTEP]
infer_instance