case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1 → x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ (x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x) → ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
constructor
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1 → x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
intro h
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖inner x y‖ / (‖x‖ * ‖y‖) = 1
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x
refine' ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one _⟩
no goals
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖inner x y‖ / (‖x‖ * ‖y‖) = 1
simpa using h
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
h₀ : x = 0
⊢ False
simp [h₀] at h
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h : ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
hx₀ : x ≠ 0
h₀ : y = 0
⊢ False
simp [h₀] at h
case mpr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖inner x (r • x) / (↑‖x‖ * ↑‖r • x‖)‖ = 1
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ (x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x) → ‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1
rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
case mpr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖inner x (r • x)‖ / (‖x‖ * ‖r • x‖) = 1
case mpr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖inner x (r • x) / (↑‖x‖ * ↑‖r • x‖)‖ = 1
simp only [norm_div, norm_mul, norm_ofReal, abs_norm]
no goals
case mpr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3189464
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖inner x (r • x)‖ / (‖x‖ * ‖r • x‖) = 1
exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr