case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₁ : ∃ k, k ≠ 1 ∧ x + y = k • (x - y)
h₂ : ‖z - y‖ = ‖z + y‖
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
obtain ⟨k, hk_ne_one, hk⟩ := h₁
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
let r := (k - 1)⁻¹ * (k + 1)
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
have hxy : x = r • y := by
  rw [← smul_smul, eq_inv_smul_iff₀ (sub_ne_zero.mpr hk_ne_one), ← sub_eq_zero]
  calc
    (k - 1) • x - (k + 1) • y = k • x - x - (k • y + y) := by
      simp_rw [sub_smul, add_smul, one_smul]
    _ = k • x - k • y - (x + y) := by simp_rw [← sub_sub, sub_right_comm]
    _ = k • (x - y) - (x + y) := by rw [← smul_sub k x y]
    _ = 0 := sub_eq_zero.mpr hk.symm
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
have hzy : ⟪z, y⟫ = 0 := by
  rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
    eq_comm]
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
have hzx : ⟪z, x⟫ = 0 := by rw [hxy, inner_smul_right, hzy, MulZeroClass.mul_zero]
no goals
case intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖x - y‖ * ‖x + y‖ = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
calc
  ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hxy]
  _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
  _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
  _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
  _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
  _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hxy, norm_smul, mul_pow, sq_abs]
  _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
    simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ (k - 1) • x - (k + 1) • y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ x = r • y
rw [← smul_smul, eq_inv_smul_iff₀ (sub_ne_zero.mpr hk_ne_one), ← sub_eq_zero]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ (k - 1) • x - (k + 1) • y = 0
calc
  (k - 1) • x - (k + 1) • y = k • x - x - (k • y + y) := by
    simp_rw [sub_smul, add_smul, one_smul]
  _ = k • x - k • y - (x + y) := by simp_rw [← sub_sub, sub_right_comm]
  _ = k • (x - y) - (x + y) := by rw [← smul_sub k x y]
  _ = 0 := sub_eq_zero.mpr hk.symm
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ (k - 1) • x - (k + 1) • y = k • x - x - (k • y + y)
simp_rw [sub_smul, add_smul, one_smul]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ k • x - x - (k • y + y) = k • x - k • y - (x + y)
simp_rw [← sub_sub, sub_right_comm]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
⊢ k • x - k • y - (x + y) = k • (x - y) - (x + y)
rw [← smul_sub k x y]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
⊢ inner z y = 0
rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
  eq_comm]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
⊢ inner z x = 0
rw [hxy, inner_smul_right, hzy, MulZeroClass.mul_zero]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖
simp [sub_smul, add_smul, hxy]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖(r - 1) • y‖ * ‖(r + 1) • y‖ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖)
simp_rw [norm_smul]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2
ring
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 = abs ((r - 1) * (r + 1) * ‖y‖ ^ 2)
simp [abs_mul]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ abs ((r - 1) * (r + 1) * ‖y‖ ^ 2) = abs (r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2)
ring_nf
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ abs (r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2) = abs (‖x‖ ^ 2 - ‖y‖ ^ 2)
simp [hxy, norm_smul, mul_pow, sq_abs]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₂ : ‖z - y‖ = ‖z + y‖
k : ℝ
hk_ne_one : k ≠ 1
hk : x + y = k • (x - y)
r : ℝ := (k - 1)⁻¹ * (k + 1)
hxy : x = r • y
hzy : inner z y = 0
hzx : inner z x = 0
⊢ abs (‖x‖ ^ 2 - ‖y‖ ^ 2) = abs (‖z + y‖ ^ 2 - ‖z - x‖ ^ 2)
simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]