awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Tactic:
re_to_real.symm.trans <|
    re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two x y

Premises used: re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, RCLike.re_to_real, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) (0 : ℝ) ↔ ⟪x, y⟫_ℝ = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_eq_left, mul_eq_zero]

Premises used: mul_eq_zero, add_eq_left, norm_add_mul_self, add_right_cancel_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) (0 : ℝ) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
hy : 0 ≤ ‖x + y‖
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]

Premises used: eq_comm, norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, Real.sqrt_eq_iff_mul_self_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x + y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
rw [@norm_add_mul_self 𝕜, add_right_cancel_iff, add_eq_left, mul_eq_zero]

Premises used: mul_eq_zero, add_eq_left, norm_add_mul_self, add_right_cancel_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
h₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)

Tactic:
simp only [h, zero_re]

Premises used: RCLike.zero_re
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
(norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero x y).2 h

Premises used: Iff.mpr, norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) (0 : ℝ) ↔ ⟪x, y⟫_ℝ = 0
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [@norm_sub_mul_self ℝ, add_right_cancel_iff, sub_eq_add_neg, add_eq_left, neg_eq_zero,
    mul_eq_zero]

Premises used: norm_sub_mul_self, sub_eq_add_neg, neg_eq_zero, mul_eq_zero, add_eq_left, add_right_cancel_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
hy : 0 ≤ ‖x - y‖
⊢ ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]

Premises used: norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, Real.sqrt_eq_iff_mul_self_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x - y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ⟪x, y⟫_ℝ = 0
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
(norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero x y).2 h

Premises used: Iff.mpr, norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
| ‖x‖ = ‖y‖

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Premises used: mul_self_inj_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
conv_rhs : ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖

Tactic:
conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Premises used: mul_self_inj_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
simp : ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖

Tactic:
simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x,
    sub_eq_zero, re_to_real]

Premises used: sub_eq_zero, RCLike.re_to_real, inner_add_left, inner_self_eq_norm_mul_norm, inner_sub_right, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫ = 0
rw : ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖
⊢ ‖w - v‖ = ‖w + v‖

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]

Premises used: mul_self_inj_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫ = 0
⊢ ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖

Tactic:
simp only [h, ← @inner_self_eq_norm_mul_norm 𝕜, sub_neg_eq_add, sub_zero, map_sub, zero_re,
    zero_sub, add_zero, map_add, inner_add_right, inner_sub_left, inner_sub_right, inner_re_symm,
    zero_add]

Premises used: map_sub, sub_zero, map_add, inner_re_symm, RCLike.zero_re, inner_self_eq_norm_mul_norm, zero_add, inner_add_right, inner_sub_left, inner_sub_right, add_zero, sub_neg_eq_add, zero_sub
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : |⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1
⊢ |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1

Tactic:
rw [abs_div, abs_mul, abs_norm, abs_norm]

Premises used: abs_mul, abs_div, abs_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_real_inner_le_norm x y) (by positivity)

Premises used: div_le_one_of_le₀, abs_real_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
rw₁ rw₂ : r * ⟪x, x⟫_ℝ = r * ⟪x, x⟫_ℝ
⊢ ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)

Tactic:
rw [real_inner_smul_left, ← real_inner_self_eq_norm_mul_norm]

Premises used: real_inner_self_eq_norm_mul_norm, real_inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
rw₁ rw₂ : r * ⟪x, x⟫_ℝ = r * ⟪x, x⟫_ℝ
⊢ ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)

Tactic:
rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]

Premises used: inner_smul_right, real_inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
rw :
  ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ =
    √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)
rw₁ rw₂ :
  ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ =
    ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖
⊢ dist (HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x) (HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y) =
    √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)

Tactic:
rw [dist_eq_norm, sqrt_sq (norm_nonneg _)]

Premises used: dist_eq_norm, Real.sqrt_sq, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
simp :
  HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖y‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖x‖ 2) =
    HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2)
⊢ HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2

Tactic:
simp [field, sq, norm_sub_mul_self_real, norm_smul, real_inner_smul_left, inner_smul_right,
          Real.norm_of_nonneg (mul_self_nonneg _), -mul_eq_mul_left_iff]

Premises used: mul_self_nonneg, norm_smul, mul_eq_mul_left_iff, sq, inner_smul_right, real_inner_smul_left, norm_sub_mul_self_real, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖y‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖x‖ 2) =
    HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
rw : 0 ≤ ‖x - y‖
rw₁ : 0 ≤ HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)
hx₁ : 0 ≤ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2
⊢ √(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) =
    HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖) * dist x y

Tactic:
rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm]

Premises used: dist_eq_norm, Real.sqrt_mul, Real.sqrt_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ ‖x - y‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ 0 ≤ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2

Tactic:
positivity
-- 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 : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]
-- 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 : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
have hx' : ‖x‖ ≠ 0 := by simp [hx]
-- 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 : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖r‖ ≠ 0

Tactic:
simp [hr]
-- 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 : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖r‖ ≠ 0

Tactic:
have hr' : ‖r‖ ≠ 0 := by simp [hr]
-- 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 : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul]

Premises used: norm_smul, norm_mul, inner_self_eq_norm_mul_norm, inner_smul_right, inner_self_re_eq_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
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₃ : ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1
rw₄ : ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1
rw₅ : ‖x‖ / ‖x‖ = 1
rw₆ rw₇ : Eq (α := ℝ) 1 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1

Tactic:
rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']

Premises used: mul_assoc, mul_div_cancel_right₀, mul_comm, div_div, div_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
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:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
rw : r * (‖x‖ * ‖x‖) ≠ 0
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_nonneg hr.le, div_self]

Premises used: Norm.norm, norm_smul, abs, mul_assoc, LT.lt.le, mul_comm, abs_of_nonneg, real_inner_smul_self_right, div_self, Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Premises used: Iff.mpr, LT.lt.ne', norm_ne_zero_iff, mul_ne_zero, mul_self_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Premises used: Iff.mpr, LT.lt.ne', norm_ne_zero_iff, mul_ne_zero, mul_self_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
rw : r * (‖x‖ * ‖x‖) ≠ 0
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1

Tactic:
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]

Premises used: Norm.norm, norm_smul, abs, abs_of_neg, mul_assoc, div_neg_eq_neg_div, mul_comm, neg_mul, real_inner_smul_self_right, div_self, Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Premises used: Iff.mpr, norm_ne_zero_iff, mul_ne_zero, mul_self_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Premises used: Iff.mpr, norm_ne_zero_iff, mul_ne_zero, mul_self_ne_zero, LT.lt.ne
-- 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
⊢ ‖⟪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
⊢ 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
⊢ ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
1 → 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
⊢ ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
fun h => or_iff_not_imp_left.2 fun hx₀ => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_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
refine : ∀ (h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖) (hx₀ : ¬x = 0), y = (⟪x, y⟫ / ⟪x, x⟫) • x
⊢ ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_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, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0

Tactic:
have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)
-- 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⟫‖ = ‖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⟫‖
hb : 0 ≤ ‖x‖ * ‖y‖
⊢ 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

Premises used: mul_sub, sub_eq_zero, eq_comm, mul_right_inj', sq_eq_sq₀, mul_pow
-- 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⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ 0 ≤ ‖⟪x, y⟫‖

Tactic:
positivity
-- 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⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ 0 ≤ ‖⟪x, y⟫‖

Tactic:
try positivity
-- 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⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity
-- 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⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
try positivity
-- 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 : 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
⊢ 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

Premises used: InnerProductSpace.norm_sq_eq_re_inner
-- 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
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
⊢ 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

Premises used: InnerProductSpace.Core.cauchy_schwarz_aux
-- 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
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
⊢ ⟪x, y⟫ • x = ⟪x, x⟫ • y

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

Premises used: sub_eq_zero, InnerProductSpace.Core.normSq_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
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
ha : ⟪x, x⟫ ≠ 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x

Tactic:
rw [div_eq_inv_mul, mul_smul, h, inv_smul_smul₀]

Premises used: inv_smul_smul₀, 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
hx₀ : ¬x = 0
this_1 : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore
h : ⟪x, y⟫ • x = ⟪x, x⟫ • y
ha ha₁ ha₂ ha₃ : x ≠ 0
⊢ ⟪x, x⟫ ≠ 0

Tactic:
rwa [inner_self_ne_zero]

Premises used: inner_self_ne_zero