-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_div_norm_mul_norm_eq_one_iff (x y : F) :
    ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r : ℝ, 0 < r ∧ y = r • x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
h₀ : x = 0
⊢ False

Tactic:
simp [h₀] at h

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
h₀ : y = 0
⊢ False

Tactic:
simp [h₀] at h

Result:
no goals

Proof state:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ y = (‖y‖ / ‖x‖) • x

Tactic:
exact ((inner_eq_norm_mul_iff_div hx₀).1 (eq_of_div_eq_one h)).symm

Result:
no goals

Proof state:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
refine ⟨hx₀, ‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy₀) (norm_pos_iff.2 hx₀), ?_⟩

Result:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ y = (‖y‖ / ‖x‖) • x

Proof state:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h

Result:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Proof state:
case mpr.intro.intro.intro
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
constructor

Result:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 → x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

case mpr
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x) → ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1

Proof state:
case mpr
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x) → ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1

Tactic:
rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩

Result:
case mpr.intro.intro.intro
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Proof state:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 → x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
intro h

Result:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Proof state:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h

Result:
case mp
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
⊢ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x