-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_eq_norm_mul_iff_div {x y : E} (h₀ : x ≠ 0) :
    ⟪x, y⟫ = (‖x‖ : 𝕜) * ‖y‖ ↔ (‖y‖ / ‖x‖ : 𝕜) • x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
have h₀' := h₀

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ h₀' : x ≠ 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
⊢ ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖

Tactic:
simp [h]

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ (↑‖(↑‖x‖ * ↑‖y‖ / ⟪x, x⟫_𝕜) • x‖ / ↑‖x‖) • x = (↑‖x‖ * ↑‖y‖ / ⟪x, x⟫_𝕜) • x

Tactic:
simp [norm_smul, inner_self_ofReal_norm, mul_div_cancel_right₀ _ h₀']

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ↑‖y‖ / ↑‖x‖ * ↑‖x‖ ^ 2 = ↑‖x‖ * ↑‖y‖

Tactic:
field_simp [sq, mul_left_comm]

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖

Tactic:
conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ↑‖y‖ / ↑‖x‖ * ↑‖x‖ ^ 2 = ↑‖x‖ * ↑‖y‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ h₀' : x ≠ 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
rw [← norm_ne_zero_iff, Ne, ← @ofReal_eq_zero 𝕜] at h₀'

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
rw [this.resolve_left h₀, h]

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ (↑‖(↑‖x‖ * ↑‖y‖ / ⟪x, x⟫_𝕜) • x‖ / ↑‖x‖) • x = (↑‖x‖ * ↑‖y‖ / ⟪x, x⟫_𝕜) • x

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
⊢ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
  ((@norm_inner_eq_norm_tfae 𝕜 _ _ _ _ x y).out 0 1).1 (by simp [h])

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
this : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ (↑‖y‖ / ↑‖x‖) • x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

Tactic:
constructor <;> intro h

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖
⊢ (↑‖y‖ / ↑‖x‖) • x = y

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬↑‖x‖ = 0
h : (↑‖y‖ / ↑‖x‖) • x = y
⊢ ⟪x, y⟫_𝕜 = ↑‖x‖ * ↑‖y‖