-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem I_prop : innerProp' E (I : 𝕜)

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))

Tactic:
have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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

Tactic:
rw [conj_I, inner_, inner_, mul_left_comm, smul_smul, hI', neg_one_smul]

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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 * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))

Proof state:
case pos
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E 0

Tactic:
simpa using real_prop (𝕜 := 𝕜) 0

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖

Tactic:
rw [← neg_sub, norm_neg, sub_eq_neg_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
⊢ InnerProductSpaceable.innerProp' E I

Tactic:
by_cases hI : (I : 𝕜) = 0

Result:
case pos
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E I

case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
⊢ InnerProductSpaceable.innerProp' E I

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ -
        I * 𝓚 ‖x + y‖ * 𝓚 ‖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‖))

Tactic:
linear_combination (- 𝓚 ‖(I : 𝕜) • x - y‖ ^ 2 + 𝓚 ‖(I : 𝕜) • x + y‖ ^ 2) * hI' / 4

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖

Tactic:
rw [← neg_add', norm_neg]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))

Tactic:
rw [h₁, h₂]

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ -
        I * 𝓚 ‖x + y‖ * 𝓚 ‖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‖))

Proof state:
case pos
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E I

Tactic:
rw [hI]

Result:
case pos
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : I = 0
⊢ InnerProductSpaceable.innerProp' E 0

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
⊢ InnerProductSpaceable.innerProp' E I

Tactic:
intro x y

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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

Tactic:
have hI' := I_mul_I_of_nonzero hI

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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

Proof state:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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 * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))

Tactic:
have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]

Result:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
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‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-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‖))