awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
refine_2 :
  2 * (HMul.hMul (α := ℝ) 1 1 + HMul.hMul (α := ℝ) 1 1) - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2

Tactic:
rw [sq, eq_sub_iff_add_eq.2 (parallelogram_law_with_norm_mul ℝ x y), ← sq ‖x - y‖, hx, hy]

Premises used: Iff.mpr, Norm.norm, parallelogram_law_with_norm_mul, Real, HSub.hSub, eq_sub_iff_add_eq, sq
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
refine_2 : 4 - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
⊢ 2 * (HMul.hMul (α := ℝ) 1 1 + HMul.hMul (α := ℝ) 1 1) - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2

Tactic:
ring_nf
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
refine_2 : 0 ≤ ε
⊢ 4 - HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
rw : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) (inner 𝕜 x x) : ℝ)

Tactic:
rw [← InnerProductSpace.norm_sq_eq_re_inner]

Premises used: InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
rw : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)

Tactic:
rw [← InnerProductSpace.norm_sq_eq_re_inner]

Premises used: InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
hx : ⟪x, x⟫_𝕜 = 0
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) 0 : ℝ) (0 : ℝ)
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = 0

Tactic:
rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero]

Premises used: map_zero, InnerProductSpace.norm_sq_eq_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ = ⟪x, y⟫

Tactic:
c.conj_inner_symm x y

Premises used: PreInnerProductSpace.Core.conj_inner_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
c.re_inner_nonneg _

Premises used: PreInnerProductSpace.Core.re_inner_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : I * HSub.hSub (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ : 𝕜) ⟪x, x⟫ / 2 = (↑0 : 𝕜)
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) (0 : ℝ)

Tactic:
rw [← @ofReal_inj 𝕜, im_eq_conj_sub]

Premises used: RCLike.ofReal_inj, RCLike.im_eq_conj_sub
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ I * HSub.hSub (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, x⟫ : 𝕜) ⟪x, x⟫ / 2 = (↑0 : 𝕜)

Tactic:
simp [inner_conj_symm]

Premises used: InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

Tactic:
c.add_left _ _ _

Premises used: PreInnerProductSpace.Core.add_left
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
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: InnerProductSpace.Core.inner_add_left, map_add, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, x⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪z, x⟫ : 𝕜) =
    ⟪x, y⟫ + ⟪x, z⟫

Tactic:
simp only [inner_conj_symm]

Premises used: InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw :
  Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ∧
    Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
⊢ (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) = ⟪x, x⟫

Tactic:
rw [ext_iff]
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
simp only [ofReal_re, normSq]

Premises used: RCLike.ofReal_re, InnerProductSpace.Core.normSq
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
simp only [inner_self_im, ofReal_im]

Premises used: RCLike.ofReal_im, InnerProductSpace.Core.inner_self_im
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ∧
    Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) (↑(normSq.{u_1, u_3} (𝕜 := 𝕜) x) : 𝕜) : ℝ) ((im : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)

Tactic:
exact ⟨by simp only [ofReal_re, normSq], by simp only [inner_self_im, ofReal_im]⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ ⟪r • x, y⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪x, y⟫

Tactic:
c.smul_left _ _ _

Premises used: PreInnerProductSpace.Core.smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪y, x⟫) = r * ⟪x, y⟫
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_smul_left]

Premises used: InnerProductSpace.Core.inner_smul_left, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪y, x⟫) = r * ⟪x, y⟫

Tactic:
simp only [conj_conj, inner_conj_symm, map_mul]

Premises used: RCLike.conj_conj, map_mul, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0
⊢ ⟪0, x⟫ = 0

Tactic:
rw [← zero_smul 𝕜 (0 : F), inner_smul_left]

Premises used: InnerProductSpace.Core.inner_smul_left, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) ⟪0, x⟫ = 0

Tactic:
simp only [zero_mul, map_zero]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
rw : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)
⊢ ⟪x, 0⟫ = 0

Tactic:
rw [← inner_conj_symm, inner_zero_left]

Premises used: InnerProductSpace.Core.inner_zero_left, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) 0 : 𝕜) (0 : 𝕜)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ inner.{u_1, u_3} 𝕜 (E := F) 0 0 = 0

Tactic:
inner_zero_left _

Premises used: InnerProductSpace.Core.inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ inner.{u_1, u_3} 𝕜 (E := F) 0 0 = 0

Tactic:
exact inner_zero_left _

Premises used: InnerProductSpace.Core.inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ normSq.{u_1, u_3} (𝕜 := 𝕜) (F := F) 0 = 0

Tactic:
simp [normSq, inner_self_of_eq_zero]

Premises used: InnerProductSpace.Core.normSq, InnerProductSpace.Core.inner_self_of_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ ⟪x, x⟫ ≠ 0 → x ≠ 0

Tactic:
mt inner_self_of_eq_zero

Premises used: mt, InnerProductSpace.Core.inner_self_of_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (↑((re : (a : 𝕜) → ℝ) ⟪x, x⟫) : 𝕜) = ⟪x, x⟫

Tactic:
norm_num [ext_iff, inner_self_im]

Premises used: InnerProductSpace.Core.inner_self_im
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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: InnerProductSpace.Core.inner_smul_left, neg_one_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-1) : 𝕜) ⟪x, y⟫ = -⟪x, y⟫

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫
⊢ ⟪x, -y⟫ = -⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Premises used: InnerProductSpace.Core.inner_neg_left, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (-⟪y, x⟫) = -⟪x, y⟫

Tactic:
simp only [map_neg, inner_conj_symm]

Premises used: map_neg, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Tactic:
simp [sub_eq_add_neg, inner_add_left, inner_neg_left]

Premises used: InnerProductSpace.Core.inner_add_left, InnerProductSpace.Core.inner_neg_left, sub_eq_add_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Tactic:
simp [sub_eq_add_neg, inner_add_right, inner_neg_right]

Premises used: sub_eq_add_neg, InnerProductSpace.Core.inner_neg_right, InnerProductSpace.Core.inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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, InnerProductSpace.Core.inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (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.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (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.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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: InnerProductSpace.Core.inner_add_left, InnerProductSpace.Core.inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫ + ⟪y, x⟫ + (⟪x, y⟫ + ⟪y, y⟫) = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
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: InnerProductSpace.Core.inner_sub_left, InnerProductSpace.Core.inner_sub_right
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
rw : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑t : 𝕜) : 𝕜) ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
rw₁ : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
rw₂ rw₃ : ⟪x, y⟫ * (↑t : 𝕜) = ⟪x, y⟫ * (↑t : 𝕜)
⊢ ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)

Tactic:
rw [inner_smul_left, conj_ofReal, mul_comm]

Premises used: InnerProductSpace.Core.inner_smul_left, RCLike.conj_ofReal, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
rw : (↑t : 𝕜) * ⟪x, y⟫ = ⟪x, y⟫ * (↑t : 𝕜)
rw₁ rw₂ : ⟪x, y⟫ * (↑t : 𝕜) = ⟪x, y⟫ * (↑t : 𝕜)
⊢ ⟪x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) y⟫ = ⟪x, y⟫ * (↑t : 𝕜)

Tactic:
rw [inner_smul_right, mul_comm]

Premises used: InnerProductSpace.Core.inner_smul_right, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
t : ℝ
⊢ (re : (a : 𝕜) → ℝ)
      ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ =
    normSq.{u_1, u_3} (𝕜 := 𝕜) x * t * t

Tactic:
simp [inner_smul_ofReal_left, inner_smul_ofReal_right, normSq]

Premises used: InnerProductSpace.Core.inner_smul_ofReal_right, InnerProductSpace.Core.inner_smul_ofReal_left, InnerProductSpace.Core.normSq
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y⟫ :
      ℝ)

Tactic:
inner_self_nonneg

Premises used: InnerProductSpace.Core.inner_self_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
rw rw₁ :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
            ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
          ⟪y, y⟫) :
      ℝ)
    ((re : (a : 𝕜) → ℝ)
        (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
            ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
          ⟪y, y⟫) :
      ℝ)
⊢ Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x + y⟫ :
      ℝ)
    ((re : (a : 𝕜) → ℝ)
        (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
            ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
          ⟪y, y⟫) :
      ℝ)

Tactic:
rw [inner_add_add_self ((ofReal t : 𝕜) • x) y]

Premises used: RCLike.ofReal, HSMul.hSMul, InnerProductSpace.Core.inner_add_add_self
-- Module: Mathlib.Analysis.InnerProductSpace.Defs
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ (re : (a : 𝕜) → ℝ)
      (⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
            ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ +
          ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ +
        ⟪y, y⟫) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (β := ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ)
          ((re : (a : 𝕜) → ℝ)
              ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ :
            ℝ)
          ((re : (a : 𝕜) → ℝ) ⟪HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x, y⟫ : ℝ))
        ((re : (a : 𝕜) → ℝ) ⟪y, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑t : 𝕜) x⟫ : ℝ))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
simp only [map_add]

Premises used: map_add