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 z : E
rw :
  HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪z, x⟫ : 𝕜) =
    ⟪x, y⟫ + ⟪x, z⟫
⊢ ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Tactic:
rw [← inner_conj_symm, inner_add_left, map_add]

Premises used: map_add, inner_add_left, inner_conj_symm
-- 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 z : E
⊢ HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪z, x⟫ : 𝕜) =
    ⟪x, y⟫ + ⟪x, z⟫

Tactic:
simp only [inner_conj_symm]

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

Tactic:
rw [← inner_conj_symm, conj_re]

Premises used: RCLike.conj_re, inner_conj_symm
-- 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 (α := ℝ) ((im : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ)

Tactic:
rw [← inner_conj_symm, conj_im]

Premises used: RCLike.conj_im, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw :
  ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₁ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r : 𝕜) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₂ :
  HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ =
    HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫
rw₃ : HMul.hMul (α := 𝕜) (star ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₄ : HMul.hMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₅ : HSMul.hSMul (α := 𝕜) ((algebraMap 𝕝 𝕜 : (a : 𝕝) → 𝕜) (star r) : 𝕜) ⟪x, y⟫ = star r • ⟪x, y⟫
rw₆ rw₇ : star r • ⟪x, y⟫ = star r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫

Tactic:
rw [← algebraMap_smul 𝕜 r, InnerProductSpace.smul_left, starRingEnd_apply, starRingEnd_apply,
    ← algebraMap_star_comm, ← smul_eq_mul, algebraMap_smul]

Premises used: InnerProductSpace.smul_left, algebraMap_smul, starRingEnd_apply, smul_eq_mul, algebraMap_star_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
inst_9 : TrivialStar 𝕝
x y : E
r : 𝕝
rw : HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪x, y⟫ = r • ⟪x, y⟫
rw₁ : star r • ⟪x, y⟫ = r • ⟪x, y⟫
rw₂ rw₃ : r • ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪r • x, y⟫ = r • ⟪x, y⟫

Tactic:
rw [inner_smul_left_eq_star_smul, starRingEnd_apply, star_trivial]

Premises used: inner_smul_left_eq_star_smul, TrivialStar.star_trivial, starRingEnd_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst_3 : CommSemiring 𝕝
inst_4 : StarRing 𝕝
inst_5 : Algebra 𝕝 𝕜
inst_6 : Module 𝕝 E
inst_7 : IsScalarTower 𝕝 𝕜 E
inst_8 : StarModule 𝕝 𝕜
x y : E
r : 𝕝
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪r • y, x⟫ = r • ⟪x, y⟫
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₂ : star (HSMul.hSMul (α := 𝕝) ((starRingEnd 𝕝 : (a : 𝕝) → 𝕝) r : 𝕝) ⟪y, x⟫) = r • ⟪x, y⟫
rw₃ : star (star r • ⟪y, x⟫) = r • ⟪x, y⟫
rw₄ : star (star r) • star ⟪y, x⟫ = r • ⟪x, y⟫
rw₅ : r • star ⟪y, x⟫ = r • ⟪x, y⟫
rw₆ : HSMul.hSMul (β := 𝕜) r ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = r • ⟪x, y⟫
rw₇ rw₈ : r • ⟪x, y⟫ = r • ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r • ⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_smul_left_eq_star_smul, starRingEnd_apply, starRingEnd_apply,
    star_smul, star_star, ← starRingEnd_apply, inner_conj_symm]

Premises used: inner_smul_left_eq_star_smul, star_star, StarModule.star_smul, starRingEnd_apply, inner_conj_symm
-- 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
r : 𝕜
⊢ ⟪r • x, y⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x, y⟫

Tactic:
inner_smul_left_eq_star_smul ..

Premises used: inner_smul_left_eq_star_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ

Tactic:
inner_smul_left _ _ _

Premises used: inner_smul_left
-- 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
r : ℝ
rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) ⟪x, y⟫ = r • ⟪x, y⟫
rw₁ : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
rw₂ rw₃ : (↑r : 𝕜) * ⟪x, y⟫ = HMul.hMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) r : 𝕜) ⟪x, y⟫
⊢ ⟪HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x, y⟫ = r • ⟪x, y⟫

Tactic:
rw [inner_smul_left, conj_ofReal, Algebra.smul_def]

Premises used: RCLike.conj_ofReal, Algebra.smul_def, inner_smul_left
-- 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
r : 𝕜
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫

Tactic:
inner_smul_right_eq_smul ..

Premises used: inner_smul_right_eq_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
⊢ ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ

Tactic:
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 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
rw : (↑r : 𝕜) * ⟪x, y⟫ = r • ⟪x, y⟫
rw₁ rw₂ : (↑r : 𝕜) * ⟪x, y⟫ = HMul.hMul (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) r : 𝕜) ⟪x, y⟫
⊢ ⟪x, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) y⟫ = r • ⟪x, y⟫

Tactic:
rw [inner_smul_right, Algebra.smul_def]

Premises used: inner_smul_right, Algebra.smul_def
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := (a : E) → 𝕜) (⇑((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) v : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) fun (w : E) ↦ ⟪v, w⟫

Tactic:
rfl

Premises used: rfl
-- 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
⊢ (((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) v : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) w = ⟪v, w⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
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 : ℝ)
⊢ Eq (α := F →ₗ[ℝ] F →ₗ[ℝ] ℝ) (LinearMap.flip (innerₗ F)) (innerₗ F)

Tactic:
ext v w
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
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:
real_inner_comm v w

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
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:
exact real_inner_comm v w

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
⊢ (((innerₗ F : (a : F) → F →ₗ[ℝ] ℝ) v : F →ₗ[ℝ] ℝ) : (a : F) → ℝ) w = ⟪v, w⟫_ℝ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
f : ι → E
x : E
⊢ ⟪∑ i ∈ s, f i, x⟫ = ∑ i ∈ s, ⟪f i, x⟫

Tactic:
map_sum ((innerₛₗ 𝕜).flip x) _ _

Premises used: map_sum, innerₛₗ, LinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
s : Finset ι
f : ι → E
x : E
⊢ ⟪x, ∑ i ∈ s, f i⟫ = ∑ i ∈ s, ⟪x, f i⟫

Tactic:
map_sum (innerₛₗ 𝕜 x) _ _

Premises used: map_sum, innerₛₗ, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
M : Type u_5
inst_3 : Zero M
l : ι →₀ M
v : ι → M → E
x : E
⊢ ⟪l.sum v, x⟫ = l.sum fun (i : ι) (a : M) ↦ ⟪v i a, x⟫

Tactic:
simp [sum, sum_inner]

Premises used: Finsupp.sum, sum_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
M : Type u_5
inst_3 : Zero M
l : ι →₀ M
v : ι → M → E
x : E
⊢ ⟪x, l.sum v⟫ = l.sum fun (i : ι) (a : M) ↦ ⟪x, v i a⟫

Tactic:
simp [sum, inner_sum]

Premises used: inner_sum, Finsupp.sum
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
α : ι → Type u_5
inst_4 : (i : ι) → AddZeroClass (α i)
inst_5 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ ⟪l.sum (β := α) f, x⟫ = l.sum (β := α) fun (i : ι) (a : α i) ↦ ⟪f i a, x⟫

Tactic:
simp +contextual only [DFinsupp.sum, sum_inner]

Premises used: sum_inner, DFinsupp.sum
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : DecidableEq ι
α : ι → Type u_5
inst_4 : (i : ι) → AddZeroClass (α i)
inst_5 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ ⟪x, l.sum (β := α) f⟫ = l.sum (β := α) fun (i : ι) (a : α i) ↦ ⟪x, f i a⟫

Tactic:
simp +contextual only [DFinsupp.sum, inner_sum]

Premises used: inner_sum, DFinsupp.sum
-- 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 : ⟪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
rw₃ rw₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪0, x⟫ = 0

Tactic:
rw [← zero_smul 𝕜 (0 : E), inner_smul_left, map_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, map_zero, zero_smul, OfNat.ofNat, inner_smul_left
-- 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
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪0, x⟫ : ℝ) (0 : ℝ)

Tactic:
simp only [inner_zero_left, map_zero]

Premises used: map_zero, inner_zero_left
-- 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 : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪0, x⟫ : 𝕜) (0 : 𝕜)
rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)
rw₂ rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪x, 0⟫ = 0

Tactic:
rw [← inner_conj_symm, inner_zero_left, map_zero]

Premises used: map_zero, inner_zero_left, inner_conj_symm
-- 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
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, 0⟫ : ℝ) (0 : ℝ)

Tactic:
simp only [inner_zero_right, map_zero]

Premises used: map_zero, inner_zero_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 : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
PreInnerProductSpace.toCore.re_inner_nonneg x

Premises used: PreInnerProductSpace.toCore, PreInnerProductSpace.Core.re_inner_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ 0 ≤ ⟪x, x⟫_ℝ

Tactic:
@inner_self_nonneg ℝ F _ _ _ x

Premises used: 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
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = ⟪x, x⟫

Tactic:
((RCLike.is_real_TFAE (⟪x, x⟫ : 𝕜)).out 2 3).2 (inner_self_im (𝕜 := 𝕜) x)

Premises used: Iff.mpr, RCLike.is_real_TFAE, Inner.inner, inner_self_im, List.TFAE.out, OfNat.ofNat
-- 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⟫) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
rw₁ : (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜) = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
rw₂ rw₃ : HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2
⊢ ⟪x, x⟫ = HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2

Tactic:
rw [← inner_self_ofReal_re, ← norm_sq_eq_re_inner, ofReal_pow]

Premises used: inner_self_ofReal_re, RCLike.ofReal_pow, InnerProductSpace.norm_sq_eq_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 : Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)
| ‖⟪x, x⟫‖

Tactic:
rw [← inner_self_ofReal_re]

Premises used: inner_self_ofReal_re
-- 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
conv_rhs : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖⟪x, x⟫‖

Tactic:
conv_rhs => rw [← inner_self_ofReal_re]

Premises used: inner_self_ofReal_re
-- 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
symm : Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = (re : (a : 𝕜) → ℝ) ⟪x, x⟫
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜)

Tactic:
symm
-- 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
⊢ Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = (re : (a : 𝕜) → ℝ) ⟪x, x⟫

Tactic:
norm_of_nonneg inner_self_nonneg

Premises used: inner_self_nonneg, RCLike.norm_of_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
⊢ Norm.norm.{u_1} (E := 𝕜) (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = (re : (a : 𝕜) → ℝ) ⟪x, x⟫

Tactic:
exact norm_of_nonneg 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⟫
⊢ (↑‖⟪x, x⟫‖ : 𝕜) = ⟪x, x⟫

Tactic:
rw [← inner_self_re_eq_norm]

Premises used: inner_self_re_eq_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 : E
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = ⟪x, x⟫

Tactic:
inner_self_ofReal_re _

Premises used: inner_self_ofReal_re
-- 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
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = ⟪x, x⟫

Tactic:
exact inner_self_ofReal_re _

Premises used: inner_self_ofReal_re
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ |⟪x, x⟫_ℝ| = ⟪x, x⟫_ℝ

Tactic:
@inner_self_ofReal_norm ℝ F _ _ _ x

Premises used: abs, inner_self_ofReal_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 : Norm.norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) = ‖⟪y, x⟫‖
rw₁ rw₂ : ‖⟪y, x⟫‖ = ‖⟪y, x⟫‖
⊢ ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖

Tactic:
rw [← inner_conj_symm, norm_conj]

Premises used: RCLike.norm_conj, inner_conj_symm
-- 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 : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-1) : 𝕜) ⟪x, y⟫ = -⟪x, y⟫
⊢ ⟪-x, y⟫ = -⟪x, y⟫

Tactic:
rw [← neg_one_smul 𝕜 x, inner_smul_left]

Premises used: neg_one_smul, inner_smul_left
-- 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
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-1) : 𝕜) ⟪x, y⟫ = -⟪x, y⟫

Tactic:
simp
-- 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 : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
⊢ ⟪x, -y⟫ = -⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Premises used: inner_conj_symm, inner_neg_left
-- 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
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫

Tactic:
simp only [map_neg, inner_conj_symm]

Premises used: map_neg, inner_conj_symm
-- 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⟫ = ⟪x, y⟫

Tactic:
simp
-- 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
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ = ⟪x, x⟫

Tactic:
inner_conj_symm _ _

Premises used: inner_conj_symm
-- 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 z : E
⊢ ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Tactic:
simp [sub_eq_add_neg, inner_add_left]

Premises used: sub_eq_add_neg, inner_add_left
-- 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 z : E
⊢ ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Tactic:
simp [sub_eq_add_neg, inner_add_right]

Premises used: sub_eq_add_neg, inner_add_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
rw :
  (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)) =
    ‖HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)‖
⊢ (re : (a : 𝕜) → ℝ) (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Tactic:
rw [← inner_conj_symm, mul_comm]

Premises used: mul_comm, inner_conj_symm
-- 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
⊢ (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)) =
    ‖HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)‖

Tactic:
re_eq_norm_of_mul_conj ⟪y, x⟫

Premises used: Inner.inner, RCLike.re_eq_norm_of_mul_conj
-- 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
⊢ (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)) =
    ‖HMul.hMul (β := 𝕜) ⟪y, x⟫ ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜)‖

Tactic:
exact re_eq_norm_of_mul_conj ⟪y, x⟫
-- 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_add_left, inner_add_right]

Premises used: inner_add_left, inner_add_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
rw : (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ (starRingEnd ℝ : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
-- 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_add_add_self, this, add_left_inj]

Premises used: add_left_inj, inner_add_add_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