awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
⊢ Eq (α := F →ₗ[ℝ] F →ₗ[ℝ] ℝ) (LinearMap.flip (innerₗ F)) (innerₗ F)
have h : ∀ (v w : F),
  Eq (α := ℝ) ((((LinearMap.flip (innerₗ F) : (a : F) → F →ₗ[ℝ] ℝ) v : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
    ((((innerₗ F : (a : F) → F →ₗ[ℝ] ℝ) v : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
Tactic: ext v w
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ⟪0, x⟫ = 0
have rw : ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 0 0, x⟫ = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), inner_smul_left, map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 0 0, x⟫ = 0
⊢ ⟪0, x⟫ = 0
have rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), inner_smul_left, map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 0 0, x⟫ = 0
rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0
⊢ ⟪0, x⟫ = 0
have rw₂ : 0 * ⟪0, x⟫ = 0
Tactic: rw [← zero_smul 𝕜 (0 : E), inner_smul_left, map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 0 0, x⟫ = 0
rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0
rw₂ : 0 * ⟪0, x⟫ = 0
⊢ ⟪0, x⟫ = 0
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← zero_smul 𝕜 (0 : E), inner_smul_left, map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, 0⟫ = 0
have rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪0, x⟫ : 𝕜) (0 : 𝕜)
Tactic: rw [← inner_conj_symm, inner_zero_left, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪0, x⟫ : 𝕜) (0 : 𝕜)
⊢ ⟪x, 0⟫ = 0
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)
Tactic: rw [← inner_conj_symm, inner_zero_left, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪0, x⟫ : 𝕜) (0 : 𝕜)
rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)
⊢ ⟪x, 0⟫ = 0
have rw₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← inner_conj_symm, inner_zero_left, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ⟪x, x⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
have rw : (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
Tactic: rw [← inner_self_ofReal_re, ← norm_sq_eq_re_inner, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
⊢ ⟪x, x⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
have rw₁ : (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
Tactic: rw [← inner_self_ofReal_re, ← norm_sq_eq_re_inner, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
rw₁ : (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
⊢ ⟪x, x⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
have rw₂ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
Tactic: rw [← inner_self_ofReal_re, ← norm_sq_eq_re_inner, ofReal_pow]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
| ‖⟪x, x⟫‖
have rw : Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)
Tactic: rw [← inner_self_ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖⟪x, x⟫‖
have conv_rhs : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)
Tactic: conv_rhs => rw [← inner_self_ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)
have symm : Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = (re : (a : 𝕜) → ℝ) ⟪x, x⟫
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ (↑‖⟪x, x⟫‖ : 𝕜) = ⟪x, x⟫
have rw : (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = ⟪x, x⟫
Tactic: rw [← inner_self_re_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫‖
have rw : Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = ‖⟪y, x⟫‖
Tactic: rw [← inner_conj_symm, norm_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw : Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = ‖⟪y, x⟫‖
⊢ ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖
have rw₁ : ‖⟪y, x⟫‖ = ‖⟪y, x⟫‖
Tactic: rw [← inner_conj_symm, norm_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪-x, y⟫ = -⟪x, y⟫
have rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-1) : 𝕜) ⟪x, y⟫ = -⟪x, y⟫
Tactic: rw [← neg_one_smul 𝕜 x, inner_smul_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, -y⟫ = -⟪x, y⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
Tactic: rw [← inner_conj_symm, inner_neg_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖
have rw : (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)) =
  ‖HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)‖
Tactic: rw [← inner_conj_symm, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫
have simp : ⟪x, x⟫ + ⟪y, x⟫ + (⟪x, y⟫ + ⟪y, y⟫) = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫
Tactic: simp only [inner_add_left, inner_add_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
have rw : (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ
Tactic: rw [← inner_conj_symm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
have this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
Tactic: have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
have simp : ⟪x, x⟫_ℝ + ⟪x, y⟫_ℝ + ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ
Tactic: simp only [inner_add_add_self, this, add_left_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫
have simp : ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫
Tactic: simp only [inner_sub_left, inner_sub_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
have this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
Tactic: have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
have simp : ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ
Tactic: simp only [inner_sub_sub_self, this, add_left_inj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2 * (⟪x, x⟫ + ⟪y, y⟫)
have simp : ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫) = 2 * (⟪x, x⟫ + ⟪y, y⟫)
Tactic: simp only [inner_add_add_self, inner_sub_sub_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ ≤ ‖⟪x, y⟫_ℝ‖ * ‖⟪y, x⟫_ℝ‖
have rw : ⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ ≤ ‖⟪y, x⟫_ℝ * ⟪y, x⟫_ℝ‖
Tactic: rw [real_inner_comm y, ← norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v - w⟫ = 0
have rw : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v⟫ - ⟪v, w⟫ = 0
Tactic: rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v - w⟫ = 0
have rw₁ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v⟫ = ⟪v, w⟫
Tactic: rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v - w⟫ = 0
have rw₂ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫
Tactic: rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 ↔ ⟪v, v - w⟫ = 0
have rw₃ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫ ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 = ⟪v, w⟫
Tactic: rw [inner_sub_right, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v - w, w⟫ = 0
have rw : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ - ⟪w, w⟫ = 0
Tactic: rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v - w, w⟫ = 0
have rw₁ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ = ⟪w, w⟫
Tactic: rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v - w, w⟫ = 0
have rw₂ : ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2
Tactic: rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪v, w⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 ↔ ⟪v - w, w⟫ = 0
have rw₃ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 = ⟪v, w⟫ ↔ HPow.hPow (α := 𝕜) (β := ℕ) (↑‖w‖ : 𝕜) 2 = ⟪v, w⟫
Tactic: rw [inner_sub_left, sub_eq_zero, inner_self_eq_norm_sq_to_K, 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 : E
⊢ ⟪x, x⟫ = 0 ↔ x = 0
have rw : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = 0 ↔ x = 0
Tactic: rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, 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 : E
rw : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = 0 ↔ x = 0
⊢ ⟪x, x⟫ = 0 ↔ x = 0
have rw₁ : Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0 ↔ x = 0
Tactic: rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, 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 : E
rw : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = 0 ↔ x = 0
rw₁ : Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0 ↔ x = 0
⊢ ⟪x, x⟫ = 0 ↔ x = 0
have rw₂ : ‖x‖ = 0 ↔ x = 0
Tactic: rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, 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 : E
rw : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = 0 ↔ x = 0
rw₁ : Eq.{u_1 + 1} (α := 𝕜) (↑‖x‖ : 𝕜) 0 ↔ x = 0
rw₂ : ‖x‖ = 0 ↔ x = 0
⊢ ⟪x, x⟫ = 0 ↔ x = 0
have rw₃ : x = 0 ↔ x = 0
Tactic: rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, 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 : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
rw : x - y = 0
⊢ x = y
have rw₁ : ⟪x - y, x - y⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
⊢ x = y
have rw₂ : ⟪x - y, x⟫ - ⟪x - y, y⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪v, x⟫ = ⟪v, y⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
rw₂ : ⟪x - y, x⟫ - ⟪x - y, y⟫ = 0
⊢ x = y
have rw₃ : ⟪x - y, x⟫ = ⟪x - y, y⟫
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
-- 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 : ∀ (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⟫
⊢ x = y
have rw₄ : ⟪x - y, y⟫ = ⟪x - y, y⟫
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
rw : x - y = 0
⊢ x = y
have rw₁ : ⟪x - y, x - y⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
⊢ x = y
have rw₂ : ⟪x, x - y⟫ - ⟪y, x - y⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
-- 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 : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
rw : x - y = 0
rw₁ : ⟪x - y, x - y⟫ = 0
rw₂ : ⟪x, x - y⟫ - ⟪y, x - y⟫ = 0
⊢ x = y
have rw₃ : ⟪x, x - y⟫ = ⟪y, x - y⟫
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
-- 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 : ∀ (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⟫
⊢ x = y
have rw₄ : ⟪y, x - y⟫ = ⟪y, x - y⟫
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
-- 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
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
⊢ LinearIndependent 𝕜 v
have rw : ∀ (s : Finset ι) (g : ι → 𝕜), Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: rw [linearIndependent_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
ι : 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⟫
have rw : g i * ⟪v i, v i⟫ = ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫
Tactic: rw [inner_sum]
-- 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
ι : 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⟫ = ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫
have symm : ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫
Tactic: symm
-- 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
ι : 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_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫
have h : g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫
Tactic: convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_
-- 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
ι : 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⟫
⊢ ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫
have convert_3 : ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0
Tactic: convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_