𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ h₀' : x ≠ 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
have h₀' := h₀
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ h₀' : x ≠ 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
rw [← norm_ne_zero_iff, Ne.def, ← @ofReal_eq_zero 𝕜] at h₀'
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
⊢ (↑‖y‖ / ↑‖x‖) • x = y

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ inner x y = ↑‖x‖ * ↑‖y‖
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y
constructor <;> intro h
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (inner x y / inner x x) • x
⊢ (↑‖y‖ / ↑‖x‖) • x = y
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
⊢ (↑‖y‖ / ↑‖x‖) • x = y
have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
  ((@norm_inner_eq_norm_tfae 𝕜 _ _ _ _ x y).out 0 1).1 (by simp [h])
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (inner x y / inner x x) • x
⊢ (↑‖(↑‖x‖ * ↑‖y‖ / inner x x) • x‖ / ↑‖x‖) • x = (↑‖x‖ * ↑‖y‖ / inner x x) • x
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (inner x y / inner x x) • x
⊢ (↑‖y‖ / ↑‖x‖) • x = y
rw [this.resolve_left h₀, h]
no goals
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (inner x y / inner x x) • x
⊢ (↑‖(↑‖x‖ * ↑‖y‖ / inner x x) • x‖ / ↑‖x‖) • x = (↑‖x‖ * ↑‖y‖ / inner x x) • x
simp [norm_smul, inner_self_ofReal_norm, mul_div_cancel _ h₀']
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : inner x y = ↑‖x‖ * ↑‖y‖
⊢ ‖inner x y‖ = ‖x‖ * ‖y‖
simp [h]
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ↑‖y‖ / ↑‖x‖ * ↑‖x‖ ^ 2 = ↑‖x‖ * ↑‖y‖
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ inner x y = ↑‖x‖ * ↑‖y‖
conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]
no goals
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.3199819
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ↑‖y‖ / ↑‖x‖ * ↑‖x‖ ^ 2 = ↑‖x‖ * ↑‖y‖
field_simp [sq, mul_left_comm]