awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp : ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫
⊢ ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Tactic:
simp only [inner_sub_left, inner_sub_right]

Premises used: inner_sub_left, inner_sub_right
-- 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
⊢ ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
simp : ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
simp only [inner_sub_sub_self, this, add_left_inj]

Premises used: add_left_inj, inner_sub_sub_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ

Tactic:
ring
-- 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
simp : ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫) = 2 * (⟪x, x⟫ + ⟪y, y⟫)
⊢ ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2 * (⟪x, x⟫ + ⟪y, y⟫)

Tactic:
simp only [inner_add_add_self, inner_sub_sub_self]

Premises used: inner_add_add_self, inner_sub_sub_self
-- 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
⊢ ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫) = 2 * (⟪x, x⟫ + ⟪y, y⟫)

Tactic:
ring
-- 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
⊢ ‖⟪x, y⟫‖ * ‖⟪y, x⟫‖ ≤ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
letI : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
  InnerProductSpace.Core.inner_mul_inner_self_le x y

Premises used: InnerProductSpace.Core.inner_mul_inner_self_le
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖
⊢ ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖

Tactic:
rw [real_inner_comm y, ← norm_mul]

Premises used: norm_mul, real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- 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
rw : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v⟫ - ⟪v, w⟫ = 0
rw₁ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v⟫ = ⟪v, w⟫
rw₂ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫
rw₃ rw₄ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫ ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v - w⟫ = 0

Tactic:
rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]

Premises used: inner_self_eq_norm_sq_to_K, sub_eq_zero, eq_comm, inner_sub_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
⊢ ⟪v, w⟫_ℝ = HPow.hPow (β := ℕ) ‖v‖ 2 ↔ ⟪v, v - w⟫_ℝ = 0

Tactic:
inner_eq_ofReal_norm_sq_left_iff

Premises used: inner_eq_ofReal_norm_sq_left_iff
-- 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
rw : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ - ⟪w, w⟫ = 0
rw₁ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ = ⟪w, w⟫
rw₂ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2
rw₃ rw₄ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 = ⟪v, w⟫ ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 = ⟪v, w⟫
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v - w, w⟫ = 0

Tactic:
rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]

Premises used: inner_self_eq_norm_sq_to_K, sub_eq_zero, eq_comm, inner_sub_left
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
⊢ ⟪v, w⟫_ℝ = HPow.hPow (β := ℕ) ‖w‖ 2 ↔ ⟪v - w, w⟫_ℝ = 0

Tactic:
inner_eq_ofReal_norm_sq_right_iff

Premises used: inner_eq_ofReal_norm_sq_right_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 : E
rw : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = 0 ↔ x = 0
rw₁ : Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0 ↔ x = 0
rw₂ : ‖x‖ = 0 ↔ x = 0
rw₃ rw₄ : x = 0 ↔ x = 0
⊢ ⟪x, x⟫ = 0 ↔ x = 0

Tactic:
rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, ofReal_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, inner_self_eq_norm_sq_to_K, RCLike.ofReal_eq_zero, sq_eq_zero_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 : E
⊢ ⟪x, x⟫ ≠ 0 ↔ x ≠ 0

Tactic:
inner_self_eq_zero.not

Premises used: Iff.not, inner_self_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 : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
rw₂ : ⟪x - y, x⟫ - ⟪x - y, y⟫ = 0
rw₃ : ⟪x - y, x⟫ = ⟪x - y, y⟫
rw₄ rw₅ : ⟪x - y, y⟫ = ⟪x - y, y⟫
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]

Premises used: sub_eq_zero, HSub.hSub, inner_self_eq_zero, inner_sub_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
⊢ x = y ↔ ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫

Tactic:
⟨fun h _ ↦ h ▸ rfl, ext_inner_left 𝕜⟩

Premises used: Eq.rec, Iff.intro, ext_inner_left, rfl
-- 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 : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
rw₂ : ⟪x, x - y⟫ - ⟪y, x - y⟫ = 0
rw₃ : ⟪x, x - y⟫ = ⟪y, x - y⟫
rw₄ rw₅ : ⟪y, x - y⟫ = ⟪y, x - y⟫
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]

Premises used: sub_eq_zero, HSub.hSub, inner_self_eq_zero, inner_sub_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
⊢ x = y ↔ ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫

Tactic:
⟨fun h _ ↦ h ▸ rfl, ext_inner_right 𝕜⟩

Premises used: Eq.rec, ext_inner_right, Iff.intro, rfl
-- 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
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (0 : ℝ) ↔ x = 0

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 : E
⊢ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ↔ x ≠ 0

Tactic:
simp [sq_pos_iff]

Premises used: sq_pos_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0

Tactic:
re_inner_self_nonpos (𝕜 := ℝ)

Premises used: re_inner_self_nonpos
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ 0 < ⟪x, x⟫_ℝ ↔ x ≠ 0

Tactic:
re_inner_self_pos (𝕜 := ℝ)

Premises used: re_inner_self_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
rw : ∀ (s : Finset ι) (g : ι → 𝕜), Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent 𝕜 v

Tactic:
rw [linearIndependent_iff']

Premises used: linearIndependent_iff'
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
rw : g i * ⟪v i, v i⟫ = ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫
⊢ g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫

Tactic:
rw [inner_sum]

Premises used: inner_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
symm : ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫
⊢ g i * ⟪v i, v i⟫ = ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ ∑ x ∈ s, ⟪v i, g x • v x⟫ = ⟪v i, g i • v i⟫

Tactic:
Finset.sum_eq_single (M := 𝕜) i ?_ ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
h : g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫
convert_3 : ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0
convert_4 : i ∉ s → ⟪v i, g i • v i⟫ = 0
⊢ ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫

Tactic:
convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
h h₁ : g i * ⟪v i, v i⟫ = g i * ⟪v i, v i⟫
⊢ g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫

Tactic:
rw [inner_smul_right]

Premises used: 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
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
convert_3 : g j * ⟪v i, v j⟫ = 0
convert_3₁ : g j * 0 = 0
convert_3₂ convert_3₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪v i, g j • v j⟫ = 0

Tactic:
rw [inner_smul_right, ho hji.symm, mul_zero]

Premises used: Ne.symm, MulZeroClass.mul_zero, 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
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0

Tactic:
fun h => False.elim (h hi)

Premises used: False.elim
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ i ∉ s → ⟪v i, g i • v i⟫ = 0

Tactic:
exact fun h => False.elim (h hi)

Premises used: False.elim
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫

Tactic:
have h' : g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫ := by
    rw [inner_sum]
    symm
    convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_
    · rw [inner_smul_right]
    · intro j _hj hji
      rw [inner_smul_right, ho hji.symm, mul_zero]
    · exact fun h => False.elim (h hi)
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
h' : g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫
⊢ g i = 0

Tactic:
simpa [hg, hz] using h'
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ‖x‖ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)

Tactic:
calc
    ‖x‖ = √(‖x‖ ^ 2) := (sqrt_sq (norm_nonneg _)).symm
    _ = √(re ⟪x, x⟫) := congr_arg _ (norm_sq_eq_re_inner _)

Premises used: Trans.trans, congr_arg, InnerProductSpace.norm_sq_eq_re_inner, Real.sqrt_sq, Eq.symm, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ ‖x‖ = √⟪x, x⟫_ℝ

Tactic:
@norm_eq_sqrt_re_inner ℝ _ _ _ _ x

Premises used: norm_eq_sqrt_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
rw₁ :
  (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
    √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
rw₂ rw₃ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖

Tactic:
rw [@norm_eq_sqrt_re_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
    sqrt_mul_self inner_self_nonneg]

Premises used: Real.sqrt_mul_self, norm_eq_sqrt_re_inner, inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
rw₁ rw₂ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [pow_two, inner_self_eq_norm_mul_norm]

Premises used: pow_two, inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ (re : (a : ℝ) → ℝ) ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Tactic:
have h := @inner_self_eq_norm_mul_norm ℝ F _ _ _ x
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
h : (re : (a : ℝ) → ℝ) ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
rw : ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
rw₁ rw₂ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [pow_two, real_inner_self_eq_norm_mul_norm]

Premises used: pow_two, real_inner_self_eq_norm_mul_norm
-- 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
rw :
  (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]

Premises used: sq, inner_self_eq_norm_mul_norm
-- 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
rw :
  (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]

Premises used: sq, inner_self_eq_norm_mul_norm
-- 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
rw :
  (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]

Premises used: sq, inner_self_eq_norm_mul_norm
-- 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
repeat' :
  (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
repeat' rw [sq (M := ℝ), ← @inner_self_eq_norm_mul_norm 𝕜]

Premises used: sq, inner_self_eq_norm_mul_norm
-- 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
rw :
  (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
rw [inner_add_add_self, two_mul]

Premises used: two_mul, inner_add_add_self
-- 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
simp : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
⊢ (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
simp only [add_assoc, add_left_inj, add_right_inj, map_add]

Premises used: add_assoc, map_add, add_left_inj, add_right_inj
-- 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
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)

Tactic:
rw [← inner_conj_symm, conj_re]

Premises used: RCLike.conj_re, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have h := @norm_add_sq ℝ _ _ _ _ x y
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h :
  HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simpa using h
-- 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
rw :
  HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq
-- 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
rw :
  HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq
-- 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
rw :
  HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq