-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_inner_eq_norm_tfae (x y : E) :
    List.TFAE [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖,
      x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x,
      x = 0 ∨ ∃ r : 𝕜, y = r • x,
      x = 0 ∨ y ∈ 𝕜 ∙ x]

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

Tactic:
have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)

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

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

Tactic:
rw [← sq_eq_sq₀, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h <;>
  try positivity

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

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
⊢ (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖

Tactic:
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]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Tactic:
tfae_have 2 → 3 := fun h => h.imp_right fun h' => ⟨_, h'⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Tactic:
tfae_have 3 → 1 := by
  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]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}

Tactic:
simp only [Submodule.mem_span_singleton, eq_comm]

Result:
no goals

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

Tactic:
simp only [@norm_sq_eq_inner 𝕜] at h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
h : re ⟪x, x⟫_𝕜 * (re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜 - ‖⟪x, y⟫_𝕜‖ ^ 2) = 0
⊢ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Tactic:
tfae_have 1 → 2 := by
  refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_
  have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)
  rw [← sq_eq_sq₀, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h <;>
    try positivity
  simp only [@norm_sq_eq_inner 𝕜] at h
  letI : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
  erw [← InnerProductSpace.Core.cauchy_schwarz_aux (𝕜 := 𝕜) (F := E)] at h
  rw [InnerProductSpace.Core.normSq_eq_zero, sub_eq_zero] at h
  rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
  rwa [inner_self_ne_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Proof state:
case hb
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : ‖x‖ ^ 2 ≠ 0
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖ → x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x
tfae_2_to_3 : x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x → x = 0 ∨ ∃ r, y = r • x
tfae_3_to_1 : (x = 0 ∨ ∃ r, y = r • x) → ‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖
tfae_3_iff_4 : (x = 0 ∨ ∃ r, y = r • x) ↔ x = 0 ∨ y ∈ Submodule.span 𝕜 {x}
⊢ [‖⟪x, y⟫_𝕜‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : InnerProductSpace.Core.normSq (⟪x, y⟫_𝕜 • x - ⟪x, x⟫_𝕜 • y) = 0
⊢ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x

Tactic:
rw [InnerProductSpace.Core.normSq_eq_zero, sub_eq_zero] at h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this✝ : ‖x‖ ^ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫_𝕜 • x = ⟪x, x⟫_𝕜 • y
⊢ y = (⟪x, y⟫_𝕜 / ⟪x, x⟫_𝕜) • x