case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖ → x = 0 ∨ y = (inner x y / inner x x) • x

𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
tfae_have 1 → 2
case tfae_2_to_3
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
⊢ x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x

𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
tfae_have 2 → 3
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
case tfae_2_to_3
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
⊢ x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x

𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
exact fun h => h.imp_right fun h' => ⟨_, h'⟩
case tfae_3_to_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖

𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
tfae_have 3 → 1
case tfae_3_iff_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}

𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
tfae_3_iff_4 : (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
tfae_have 3 ↔ 4
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
tfae_3_iff_4 : (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}
⊢ List.TFAE
    [‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}]
tfae_finish
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖
hx₀ : ¬x = 0
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖ → x = 0 ∨ y = (inner x y / inner x x) • x
refine' fun h => or_iff_not_imp_left.2 fun hx₀ => _
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖
hx₀ : ¬x = 0
⊢ y = (inner x y / inner x x) • x
have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
h : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2 - ‖inner x y‖ ^ 2) = 0
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
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‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (inner x y / inner x x) • x
rw [← sq_eq_sq (norm_nonneg _) (mul_nonneg (norm_nonneg _) (norm_nonneg _)), mul_pow, ←
  mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
h : ↑re (inner x x) * (↑re (inner x x) * ↑re (inner y y) - ‖inner x y‖ ^ 2) = 0
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
h : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2 - ‖inner x y‖ ^ 2) = 0
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ y = (inner x y / inner x x) • x
simp only [@norm_sq_eq_inner 𝕜] at h
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
h : ↑re (inner x x) * (↑re (inner x x) * ↑re (inner y y) - ‖inner x y‖ ^ 2) = 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
h : ↑re (inner x x) * (↑re (inner x x) * ↑re (inner y y) - ‖inner x y‖ ^ 2) = 0
⊢ y = (inner x y / inner x x) • x
letI : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : inner x y • x = inner x x • y
⊢ y = (inner x y / inner x x) • x
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
h : ↑re (inner x x) * (↑re (inner x x) * ↑re (inner y y) - ‖inner x y‖ ^ 2) = 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
⊢ y = (inner x y / inner x x) • x
erw [← InnerProductSpace.Core.cauchy_schwarz_aux, InnerProductSpace.Core.normSq_eq_zero,
  sub_eq_zero] at h
case tfae_1_to_2.hc
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : inner x y • x = inner x x • y
⊢ inner x x ≠ 0
case tfae_1_to_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : inner x y • x = inner x x • y
⊢ y = (inner x y / inner x x) • x
rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
no goals
case tfae_1_to_2.hc
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
h✝ : ‖x‖ ^ 2 * (‖x‖ ^ 2 * ‖y‖ ^ 2) = ‖x‖ ^ 2 * ‖inner x y‖ ^ 2
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : inner x y • x = inner x x • y
⊢ inner x x ≠ 0
rwa [inner_self_ne_zero]
no goals
case tfae_3_to_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
⊢ (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
rintro (rfl | ⟨r, rfl⟩) <;>
simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K, inner_self_eq_norm_mul_norm,
  sq, mul_left_comm]
no goals
case tfae_3_iff_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3166004
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
tfae_1_to_2 : ‖inner x y‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (inner x y / inner x x) • x
tfae_2_to_3 : x = 0 ∨ y = (inner x y / inner x x) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖inner x y‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}
simp only [Submodule.mem_span_singleton, eq_comm]