awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

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_re_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]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ x = 0 ∨ ∃ (r : 𝕜), y = r • x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x

Tactic:
tfae_have 2 → 3 := fun h => h.imp_right fun h' => ⟨_, h'⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
⊢ x = 0 ∨ ∃ (r : 𝕜), y = r • x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
⊢ ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
⊢ ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
y : E
tfae_1_to_2 :
  ∀ (a : ‖⟪0, y⟫‖ = Norm.norm.{u_2} (E := E) 0 * ‖y‖),
    Eq.{u_2 + 1} (α := E) 0 0 ∨ y = HSMul.hSMul (β := E) (⟪0, y⟫ / inner.{u_1, u_2} 𝕜 (E := E) 0 0) 0
tfae_2_to_3 :
  ∀ (a : Eq.{u_2 + 1} (α := E) 0 0 ∨ y = HSMul.hSMul (β := E) (⟪0, y⟫ / inner.{u_1, u_2} 𝕜 (E := E) 0 0) 0),
    Eq.{u_2 + 1} (α := E) 0 0 ∨ ∃ (r : 𝕜), y = HSMul.hSMul (β := E) r 0
⊢ ‖⟪0, y⟫‖ = Norm.norm.{u_2} (E := E) 0 * ‖y‖

Tactic:
simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K,
      sq, mul_left_comm]

Premises used: norm_smul, inner_self_eq_norm_sq_to_K, sq, mul_left_comm, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
r : 𝕜
tfae_1_to_2 : ∀ (a : ‖⟪x, r • x⟫‖ = ‖x‖ * ‖r • x‖), x = 0 ∨ r • x = (⟪x, r • x⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ r • x = (⟪x, r • x⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r_1 : 𝕜), r • x = r_1 • x
⊢ ‖⟪x, r • x⟫‖ = ‖x‖ * ‖r • x‖

Tactic:
simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K,
      sq, mul_left_comm]

Premises used: norm_smul, inner_self_eq_norm_sq_to_K, sq, mul_left_comm, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
⊢ ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖

Tactic:
tfae_have 3 → 1 := by
    rintro (rfl | ⟨r, rfl⟩) <;>
    simp [inner_smul_right, norm_smul, inner_self_eq_norm_sq_to_K,
      sq, mul_left_comm]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ x = 0 ∨ ∃ (r : 𝕜), y = r • x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ (r : 𝕜), y = r • x) ↔ x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y

Tactic:
3 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ (r : 𝕜), y = r • x) ↔ x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y

Tactic:
simp only [Submodule.mem_span_singleton, eq_comm]

Premises used: Submodule.mem_span_singleton, eq_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
⊢ (x = 0 ∨ ∃ (r : 𝕜), y = r • x) ↔ x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y

Tactic:
tfae_have 3 ↔ 4 := by simp only [Submodule.mem_span_singleton, eq_comm]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
tfae_1_to_2 : ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
tfae_2_to_3 : ∀ (a : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x), x = 0 ∨ ∃ (r : 𝕜), y = r • x
tfae_3_to_1 : ∀ (a : x = 0 ∨ ∃ (r : 𝕜), y = r • x), ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
tfae_3_iff_4 : (x = 0 ∨ ∃ (r : 𝕜), y = r • x) ↔ x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y
⊢ [‖⟪x, y⟫‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ (r : 𝕜), y = r • x,
      x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

Tactic:
calc
    ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖ ↔ x = 0 ∨ ∃ r : 𝕜, y = r • x :=
      (norm_inner_eq_norm_tfae 𝕜 x y).out 0 2
    _ ↔ ∃ r : 𝕜, y = r • x := or_iff_right hx₀
    _ ↔ ∃ r : 𝕜, r ≠ 0 ∧ y = r • x :=
      ⟨fun ⟨r, h⟩ => ⟨r, fun hr₀ => hy₀ <| h.symm ▸ smul_eq_zero.2 <| Or.inl hr₀, h⟩,
        fun ⟨r, _hr₀, h⟩ => ⟨r, h⟩⟩

Premises used: Trans.trans, Exists, Ne, norm_inner_eq_norm_tfae, And, List.TFAE.out, And.intro, Iff.intro, Exists.intro, or_iff_right, HSMul.hSMul, OfNat.ofNat, _private.0.norm_inner_eq_norm_iff.match_1, Eq, _private.0.norm_inner_eq_norm_iff.match_2
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
mp : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1 → x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
mpr : (x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x) → ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
⊢ ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1 ↔ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
h₀ : x = 0
⊢ False

Tactic:
simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
⊢ x ≠ 0

Tactic:
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
hx₀ : x ≠ 0
h₀ : y = 0
⊢ False

Tactic:
simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
hx₀ : x ≠ 0
⊢ y ≠ 0

Tactic:
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

Tactic:
⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩

Premises used: eq_of_div_eq_one, norm_inner_eq_norm_iff, And.intro, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
mp : ‖⟪x, y⟫‖ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

Tactic:
refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ ‖⟪x, y⟫‖ / (‖x‖ * ‖y‖) = 1

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
mpr : ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1
⊢ ‖⟪x, r • x⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖r • x‖ : 𝕜)‖ = 1

Tactic:
simp only [norm_div, norm_mul, norm_ofReal, abs_norm]

Premises used: RCLike.norm_ofReal, norm_mul, norm_div, abs_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

Premises used: norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
hx : x ≠ 0
r : 𝕜
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

Premises used: norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), r ≠ 0 ∧ y = r • x

Tactic:
@norm_inner_div_norm_mul_norm_eq_one_iff ℝ F _ _ _ x y

Premises used: norm_inner_div_norm_mul_norm_eq_one_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ x ≠ 0

Tactic:
have h₀' := h₀
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ h₀' : x ≠ 0
⊢ ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0

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

Premises used: Ne, norm_ne_zero_iff, RCLike.ofReal_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
mp : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) → HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
mpr : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y → ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
⊢ ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖

Tactic:
simp [h]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
⊢ x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
have : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫ : 𝕜) • x :=
      ((norm_inner_eq_norm_tfae 𝕜 x y).out 0 1).1 (by simp [h])
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
this : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
mp :
  HDiv.hDiv (α := 𝕜) (↑‖(HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x‖ : 𝕜) (↑‖x‖ : 𝕜) • x =
    (HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x
⊢ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y

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

Premises used: Or.resolve_left
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
this : x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ HDiv.hDiv (α := 𝕜) (↑‖(HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x‖ : 𝕜) (↑‖x‖ : 𝕜) • x =
    (HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x

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

Premises used: norm_smul, mul_div_cancel_right₀
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
rw : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
| ⟪x, y⟫

Tactic:
rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]

Premises used: inner_self_eq_norm_sq_to_K, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
mpr :
  HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 =
    HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)

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

Premises used: inner_self_eq_norm_sq_to_K, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
h₀' : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
h : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
⊢ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 =
    HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)

Tactic:
field
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
inl :
  ⟪0, y⟫ = HMul.hMul (α := 𝕜) (↑(Norm.norm.{u_2} (E := E) 0) : 𝕜) (↑‖y‖ : 𝕜) ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑‖y‖ : 𝕜) 0 =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Norm.norm.{u_2} (E := E) 0) : 𝕜) y
inr :
  ∀ (h₀ : x ≠ 0),
    ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y

Tactic:
rcases eq_or_ne x 0 with (rfl | h₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
y : E
⊢ ⟪0, y⟫ = HMul.hMul (α := 𝕜) (↑(Norm.norm.{u_2} (E := E) 0) : 𝕜) (↑‖y‖ : 𝕜) ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑‖y‖ : 𝕜) 0 =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Norm.norm.{u_2} (E := E) 0) : 𝕜) y

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
inr : Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y

Tactic:
rw [inner_eq_norm_mul_iff_div h₀, div_eq_inv_mul, mul_smul, inv_smul_eq_iff₀]

Premises used: inner_eq_norm_mul_iff_div, inv_smul_eq_iff₀, div_eq_inv_mul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
inr : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
inr₁ : ¬‖x‖ = 0
inr₂ inr₃ inr₄ inr₅ : ¬x = 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0

Tactic:
rwa [Ne, ofReal_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, Ne, RCLike.ofReal_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y

Tactic:
inner_eq_norm_mul_iff

Premises used: inner_eq_norm_mul_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
mp : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 → x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
mpr : (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) → ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
h₀ : x = 0
⊢ False

Tactic:
simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0

Tactic:
have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
h₀ : y = 0
⊢ False

Tactic:
simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
⊢ y ≠ 0

Tactic:
have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : 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:
⟨hx₀, ‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy₀) (norm_pos_iff.2 hx₀), ?_⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, HDiv.hDiv, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
mp : y = (‖y‖ / ‖x‖) • x
⊢ 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₀), ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ y = (‖y‖ / ‖x‖) • x

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

Premises used: eq_of_div_eq_one, inner_eq_norm_mul_iff_div, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : 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

Premises used: eq_of_div_eq_one, inner_eq_norm_mul_iff_div, Iff.mp, Eq.symm