awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have rw : ∀
  (h :
    HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) =
      0)
  (hx₀ : ¬x = 0) (this : HPow.hPow (β := ℕ) ‖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
Cleared hypotheses: h, hx₀, this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
rw :
  ∀
    (h :
      HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) =
        0)
    (hx₀ : ¬x = 0) (this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0), y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have ha : 0 ≤ ‖⟪x, y⟫‖
Tactic: rw [← sq_eq_sq₀, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
rw :
  ∀
    (h :
      HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) =
        0)
    (hx₀ : ¬x = 0) (this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0), y = (⟪x, y⟫ / ⟪x, x⟫) • x
ha : 0 ≤ ‖⟪x, y⟫‖
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have hb : 0 ≤ ‖x‖ * ‖y‖
Tactic: rw [← sq_eq_sq₀, mul_pow, ← mul_right_inj' this, eq_comm, ← sub_eq_zero, ← mul_sub] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : HPow.hPow (β := ℕ) ‖x‖ 2 * (HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2 - HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) = 0
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have h₁ : HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
      HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) =
  0
Tactic: simp only [@norm_sq_eq_re_inner 𝕜] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
h :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) -
        HPow.hPow (β := ℕ) ‖⟪x, y⟫‖ 2) =
    0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have h₁ : InnerProductSpace.Core.normSq.{u_1, u_2} (𝕜 := 𝕜) (⟪x, y⟫ • x - ⟪x, x⟫ • y) = 0
Tactic: erw [← InnerProductSpace.Core.cauchy_schwarz_aux (𝕜 := 𝕜) (F := E)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : InnerProductSpace.Core.normSq.{u_1, u_2} (𝕜 := 𝕜) (⟪x, y⟫ • x - ⟪x, x⟫ • y) = 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have h₁ : ⟪x, y⟫ • x = ⟪x, x⟫ • y
Tactic: rw [InnerProductSpace.Core.normSq_eq_zero, sub_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have ha : ⟪x, x⟫ ≠ 0
Tactic: rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
⊢ ⟪x, x⟫ ≠ 0
have ha : x ≠ 0
Tactic: rwa [inner_self_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : 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 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y].TFAE
have tfae_1_to_2 : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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, 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
have tfae_2_to_3 : ∀ (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'⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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‖, x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x, x = 0 ∨ ∃ (r : 𝕜), y = r • x,
      x = 0 ∨ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) y].TFAE
have tfae_3_to_1 : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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, 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
have tfae_3_iff_4 : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1 ↔ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
have mp : ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1 → x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1 ↔ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
have mpr : (x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x) → ‖⟪x, y⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)‖ = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
have hx₀ : x ≠ 0
Tactic: have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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
⊢ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x
have hy₀ : y ≠ 0
Tactic: have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
have mp : ‖⟪x, y⟫‖ / (‖x‖ * ‖y‖) = 1
Tactic: refine ⟨hx₀, (norm_inner_eq_norm_iff hx₀ hy₀).1 <| eq_of_div_eq_one ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫ / HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖r • x‖ : 𝕜)‖ = 1
have mpr : ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1
Tactic: simp only [norm_div, norm_mul, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
have h₀'₁ : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
Tactic: rw [← norm_ne_zero_iff, Ne, ← @ofReal_eq_zero 𝕜] at h₀'
Cleared hypotheses: h₀'
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
have mp : ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) → HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
have mpr : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y → ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
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‖ : 𝕜)
⊢ HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
have this : 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])
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) • x = y
have mp : HDiv.hDiv (α := 𝕜) (↑‖(HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x‖ : 𝕜) (↑‖x‖ : 𝕜) • x =
  (HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) / ⟪x, x⟫) • x
Tactic: rw [this.resolve_left h₀, h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
| ⟪x, y⟫
have rw : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
Tactic: rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
have mpr : HDiv.hDiv (α := 𝕜) (↑‖y‖ : 𝕜) (↑‖x‖ : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 =
  HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
Tactic: conv_lhs => rw [← h, inner_smul_right, inner_self_eq_norm_sq_to_K]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪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
have 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
Tactic: rcases eq_or_ne x 0 with (rfl | h₀)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪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
have 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
Tactic: rcases eq_or_ne x 0 with (rfl | h₀)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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, 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
have inr : Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
Tactic: rw [inner_eq_norm_mul_iff_div h₀, div_eq_inv_mul, mul_smul, inv_smul_eq_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h₀ : x ≠ 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
have inr : ¬Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
Tactic: rwa [Ne, ofReal_eq_zero, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
have inr₁ : ¬‖x‖ = 0
Tactic: rwa [Ne, ofReal_eq_zero, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0
have inr₂ : ¬x = 0
Tactic: rwa [Ne, ofReal_eq_zero, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
have mp : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 → x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
have mpr : (x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x) → ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
⊢ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
have hx₀ : x ≠ 0
Tactic: have hx₀ : x ≠ 0 := fun h₀ => by simp [h₀] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1
hx₀ : x ≠ 0
⊢ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x
have hy₀ : y ≠ 0
Tactic: have hy₀ : y ≠ 0 := fun h₀ => by simp [h₀] at h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
have mp : y = (‖y‖ / ‖x‖) • x
Tactic: refine ⟨hx₀, ‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy₀) (norm_pos_iff.2 hx₀), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
have rw : (x ≠ 0 ∧ ∃ (x_1 : ℝ), 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
Tactic: rw [← neg_eq_iff_eq_neg, ← neg_div, ← inner_neg_right, ← norm_neg y,
    real_inner_div_norm_mul_norm_eq_one_iff, (@neg_surjective ℝ _).exists]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ (x_1 : ℝ), 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
have refine : ∀ (r : ℝ), 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
Tactic: refine Iff.rfl.and (exists_congr fun r => ?_)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
have rw : r < 0 ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
Tactic: rw [neg_pos, neg_smul, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
rw : r < 0 ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
have rw₁ : r < 0 ∧ -y = -(r • x) ↔ r < 0 ∧ y = r • x
Tactic: rw [neg_pos, neg_smul, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
rw : r < 0 ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
rw₁ : r < 0 ∧ -y = -(r • x) ↔ r < 0 ∧ y = r • x
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
have rw₂ : r < 0 ∧ y = r • x ↔ r < 0 ∧ y = r • x
Tactic: rw [neg_pos, neg_smul, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = 1 ↔ x = y
have h : 1 = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
Tactic: convert! inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
⊢ ⟪x, y⟫ = 1 ↔ x = y
have h₁ : x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x
Tactic: convert! inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
h₁ : x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x
⊢ ⟪x, y⟫ = 1 ↔ x = y
have h₂ : y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y
Tactic: convert! inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = -1 ↔ x = -y
have rw : -⟪x, y⟫ = 1 ↔ x = -y
Tactic: rw [← neg_eq_iff_eq_neg, ← inner_neg_right, inner_eq_one_iff_of_norm_eq_one hx (norm_neg y ▸ hy)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : -⟪x, y⟫ = 1 ↔ x = -y
⊢ ⟪x, y⟫ = -1 ↔ x = -y
have rw₁ : ⟪x, -y⟫ = 1 ↔ x = -y
Tactic: rw [← neg_eq_iff_eq_neg, ← inner_neg_right, inner_eq_one_iff_of_norm_eq_one hx (norm_neg y ▸ hy)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : -⟪x, y⟫ = 1 ↔ x = -y
rw₁ : ⟪x, -y⟫ = 1 ↔ x = -y
⊢ ⟪x, y⟫ = -1 ↔ x = -y
have rw₂ : x = -y ↔ x = -y
Tactic: rw [← neg_eq_iff_eq_neg, ← inner_neg_right, inner_eq_one_iff_of_norm_eq_one hx (norm_neg y ▸ hy)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_ℝ < 1 ↔ x ≠ y
have h : 1 = ‖x‖ * ‖y‖
Tactic: convert! inner_lt_norm_mul_iff_real (F := F)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = ‖x‖ * ‖y‖
⊢ ⟪x, y⟫_ℝ < 1 ↔ x ≠ y
have h₁ : x = ‖y‖ • x
Tactic: convert! inner_lt_norm_mul_iff_real (F := F)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = ‖x‖ * ‖y‖
h₁ : x = ‖y‖ • x
⊢ ⟪x, y⟫_ℝ < 1 ↔ x ≠ y
have h₂ : y = ‖x‖ • y
Tactic: convert! inner_lt_norm_mul_iff_real (F := F)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
⊢ x = y
have rwa : ∀ (H : x - y = 0), x = y
Tactic: rwa [re_inner_self_nonpos, sub_eq_zero] at H
Cleared hypotheses: H