awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

Premises used: real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

Premises used: real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : (x ≠ 0 ∧ ∃ (x_1 : ℝ), 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
⊢ ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_div, ← inner_neg_right, ← norm_neg y,
    real_inner_div_norm_mul_norm_eq_one_iff, (@neg_surjective ℝ _).exists]

Premises used: neg_div, Function.Surjective.exists, real_inner_div_norm_mul_norm_eq_one_iff, inner_neg_right, neg_eq_iff_eq_neg, neg_surjective, norm_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ (x_1 : ℝ), 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
Iff.rfl.and (exists_congr fun r => ?_)

Premises used: Iff.rfl, exists_congr, Iff.and
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
refine : ∀ (r : ℝ), 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
⊢ (x ≠ 0 ∧ ∃ (x_1 : ℝ), 0 < -x_1 ∧ -y = -x_1 • x) ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
refine Iff.rfl.and (exists_congr fun r => ?_)

Premises used: Iff.rfl, exists_congr, Iff.and
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
r : ℝ
rw : r < 0 ∧ -y = -r • x ↔ r < 0 ∧ y = r • x
rw₁ : r < 0 ∧ -y = -(r • x) ↔ r < 0 ∧ y = r • x
rw₂ rw₃ : r < 0 ∧ y = r • x ↔ r < 0 ∧ y = r • x
⊢ 0 < -r ∧ -y = -r • x ↔ r < 0 ∧ y = r • x

Tactic:
rw [neg_pos, neg_smul, neg_inj]

Premises used: neg_smul, neg_pos, neg_inj
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜) ↔
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y

Tactic:
inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E)

Premises used: inner_eq_norm_mul_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 y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)
h₁ : x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x
h₂ : y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y
⊢ ⟪x, y⟫ = 1 ↔ x = y

Tactic:
convert! inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2

Premises used: inner_eq_norm_mul_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 y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 = HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖y‖ : 𝕜)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖y‖ : 𝕜) x

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖x‖ : 𝕜) y

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
rw : -⟪x, y⟫ = 1 ↔ x = -y
rw₁ : ⟪x, -y⟫ = 1 ↔ x = -y
rw₂ rw₃ : x = -y ↔ x = -y
⊢ ⟪x, y⟫ = -1 ↔ x = -y

Tactic:
rw [← neg_eq_iff_eq_neg, ← inner_neg_right, inner_eq_one_iff_of_norm_eq_one hx (norm_neg y ▸ hy)]

Premises used: inner_neg_right, neg_eq_iff_eq_neg, inner_eq_one_iff_of_norm_eq_one
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_ℝ ≤ 1

Tactic:
simpa [hx, hy] using real_inner_le_norm x y

Premises used: real_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ -1 ≤ ⟪x, y⟫_ℝ

Tactic:
simpa [hx, hy] using neg_le_of_abs_le (abs_real_inner_le_norm x y)

Premises used: abs_real_inner_le_norm, neg_le_of_abs_le
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) ⟪x, y⟫_ℝ

Tactic:
⟨neg_one_le_real_inner_of_norm_eq_one hx hy, real_inner_le_one_of_norm_eq_one hx hy⟩

Premises used: Set.Mem, setOf, real_inner_le_one_of_norm_eq_one, neg_one_le_real_inner_of_norm_eq_one, Set.Icc, And.intro
-- 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
hx : ‖x‖ = 1
⊢ ⟪x, x⟫ = 1

Tactic:
(inner_eq_one_iff_of_norm_eq_one hx hx).mpr rfl

Premises used: Iff.mpr, inner_eq_one_iff_of_norm_eq_one, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y

Tactic:
calc
    ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ ≠ ‖x‖ * ‖y‖ :=
      ⟨ne_of_lt, lt_of_le_of_ne (real_inner_le_norm _ _)⟩
    _ ↔ ‖y‖ • x ≠ ‖x‖ • y := not_congr inner_eq_norm_mul_iff_real

Premises used: Trans.trans, real_inner_le_norm, Iff.intro, inner_eq_norm_mul_iff_real, ne_of_lt, not_congr, lt_of_le_of_ne
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y

Tactic:
inner_lt_norm_mul_iff_real (F := F)

Premises used: inner_lt_norm_mul_iff_real
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : 1 = ‖x‖ * ‖y‖
h₁ : x = ‖y‖ • x
h₂ : y = ‖x‖ • y
⊢ ⟪x, y⟫_ℝ < 1 ↔ x ≠ y

Tactic:
convert! inner_lt_norm_mul_iff_real (F := F)

Premises used: inner_lt_norm_mul_iff_real
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 = ‖x‖ * ‖y‖

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ‖y‖ • x

Tactic:
simp [hx, hy]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ y = ‖x‖ • y

Tactic:
simp [hx, hy]
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
rwa : ∀ (H : x - y = 0), x = y
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : x = y), x = y
⊢ x = y

Tactic:
rwa [re_inner_self_nonpos, sub_eq_zero] at H

Premises used: sub_eq_zero, re_inner_self_nonpos
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
suffices : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)
⊢ x = y

Tactic:
suffices H : re ⟪x - y, x - y⟫ ≤ 0 by rwa [re_inner_self_nonpos, sub_eq_zero] at H
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
ha : 0 ≤ ‖x‖
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
gcongr
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
rwa : (re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) = HPow.hPow (β := ℕ) ‖y‖ 2
rwa₁ rwa₂ rwa₃ rwa₄ : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
rwa [← 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 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
⊢ (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]
-- 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
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
H₂ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
simp : LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) (⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫)) : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) (0 : ℝ)

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 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
H₁ : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) ‖y‖ 2
H₂ : (re : (a : 𝕜) → ℝ) ⟪y, x⟫ = HPow.hPow (β := ℕ) ‖y‖ 2
⊢ LE.le (α := ℝ) ((re : (a : 𝕜) → ℝ) (⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫)) : ℝ) (0 : ℝ)

Tactic:
simpa [h, H₂] using H₁
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
rw : HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔ ‖y‖ • x = ‖x‖ • y
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) (‖x‖ + ‖y‖) 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
        HPow.hPow (β := ℕ) ‖y‖ 2 =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ + HPow.hPow (β := ℕ) ‖y‖ 2 ↔
    ‖y‖ • x = ‖x‖ • y
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) =
      HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ‖x‖ * ‖y‖ ↔
    ‖y‖ • x = ‖x‖ • y
rw₄ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₅ : 2 * ⟪x, y⟫_ℝ = 2 * ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₆ : 2 * ⟪x, y⟫_ℝ = 2 * (‖x‖ * ‖y‖) ↔ ‖y‖ • x = ‖x‖ • y
rw₇ : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y
rw₈ rw₉ : ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y

Tactic:
rw [← pow_left_inj₀ (norm_nonneg _) (Left.add_nonneg (norm_nonneg _) (norm_nonneg _)) two_ne_zero,
    norm_add_sq (𝕜 := ℝ), add_pow_two, add_left_inj, add_right_inj, re_to_real, mul_assoc,
    mul_right_inj' two_ne_zero, ← inner_eq_norm_mul_iff_real]

Premises used: mul_assoc, pow_left_inj₀, RCLike.re_to_real, add_left_inj, add_pow_two, two_ne_zero, norm_add_sq, inner_eq_norm_mul_iff_real, mul_right_inj', add_right_inj, norm_nonneg, Left.add_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y z : G
rw :
  ⟪HAdd.hAdd (α := E) (β := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E), (f : (a : G) → E) z⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
rw₁ rw₂ :
  inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (x + y) : E) ((f : (a : G) → E) z : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) z : E) +
      inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) y : E) ((f : (a : G) → E) z : E)

Tactic:
rw [map_add, inner_add_left]

Premises used: map_add, inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F_1 : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
F : Type u_5
inst_5 : FunLike F G E
inst_6 : LinearMapClass F 𝕜 G E
f : F
this_1 : SeminormedAddCommGroup G := SeminormedAddCommGroup.induced G E f
this : NormedSpace 𝕜 G := NormedSpace.induced 𝕜 G E f
x y : G
r : 𝕜
rw :
  ⟪HSMul.hSMul (β := E) r ((f : (a : G) → E) x : E), (f : (a : G) → E) y⟫_𝕜 =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
rw₁ rw₂ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E)) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))
⊢ inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) (r • x) : E) ((f : (a : G) → E) y : E) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      (inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) x : E) ((f : (a : G) → E) y : E))

Tactic:
rw [map_smul, inner_smul_left]

Premises used: map_smul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : AddCommGroup G
inst_4 : Module 𝕜 G
g₁ g₂ : G
f : G →ₗ[𝕜] E
⊢ inner 𝕜 g₁ g₂ = inner.{u_1, u_2} 𝕜 (E := E) ((f : (a : G) → E) g₁ : E) ((f : (a : G) → E) g₂ : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x : 𝕜
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : 𝕜)
rw₃ rw₄ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (x * star x)

Tactic:
rw [star_def, mul_conj, ← ofReal_pow, ofReal_re]

Premises used: RCLike.star_def, RCLike.ofReal_re, RCLike.mul_conj, RCLike.ofReal_pow
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y : 𝕜
rw :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (HMul.hMul (β := 𝕜) x ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₁ :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) : 𝕜) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₂ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) y =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
rw₃ rw₄ :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) =
    HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x * star y) = y * star x

Tactic:
rw [star_def, map_mul, starRingEnd_self_apply, mul_comm]

Premises used: RCLike.star_def, map_mul, mul_comm, starRingEnd_self_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (x + y) : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
rw₁ :
  z * HAdd.hAdd (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
rw₂ rw₃ :
  HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜) =
    HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) +
      HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) y : 𝕜)
⊢ z * star (x + y) = z * star x + z * star y

Tactic:
rw [star_def, map_add, mul_add]

Premises used: RCLike.star_def, map_add, mul_add
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
rw :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z • x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₁ :
  HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (z * x) : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₂ :
  y * HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
rw₃ rw₄ :
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)) =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)
      (HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜))
⊢ y * star (z • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜) (y * star x)

Tactic:
rw [star_def, smul_eq_mul, map_mul, mul_left_comm]

Premises used: RCLike.star_def, mul_left_comm, map_mul, smul_eq_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x y : 𝕜
⊢ ⟪x, y⟫ = HMul.hMul (β := 𝕜) y ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
x y : 𝕜
⊢ ⟪x, y⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜) y

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x + y, z⟫_ℝ = ⟪x, z⟫_ℝ + ⟪y, z⟫_ℝ

Tactic:
simp +instances only [Inner.rclikeToReal, inner_add_left, map_add]

Premises used: map_add, inner_add_left, Inner.rclikeToReal
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ r • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x

Tactic:
have : r • x = (r : 𝕜) • x := rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
G : Type u_4
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
r : ℝ
this_1 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : r • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x
⊢ ⟪r • x, y⟫_ℝ = HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪x, y⟫_ℝ

Tactic:
simp +instances only [Inner.rclikeToReal, this, conj_trivial, inner_smul_left, conj_ofReal,
        re_ofReal_mul]

Premises used: RCLike.conj_ofReal, conj_trivial, Inner.rclikeToReal, RCLike.re_ofReal_mul, 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
⊢ ⟪x, y⟫_ℝ = (re : (a : 𝕜) → ℝ) ⟪x, y⟫

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
x : E
⊢ ⟪x, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x⟫_ℝ = 0

Tactic:
simp [real_inner_eq_re_inner 𝕜, inner_smul_right]

Premises used: real_inner_eq_re_inner, inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
w z : ℂ
⊢ ⟪w, z⟫_ℝ = (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
x y z : 𝕜
simp :
  HMul.hMul (α := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ)) -
      HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) x : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) x : ℝ) +
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) z : ℝ) ((re : (a : 𝕜) → ℝ) y : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) z : ℝ) (-(im : (a : 𝕜) → ℝ) y : ℝ))
⊢ (re : (a : 𝕜) → ℝ) (z * star (x + y)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) (z * star x) : ℝ) ((re : (a : 𝕜) → ℝ) (z * star y) : ℝ)

Tactic:
simp only [star_def, map_add, mul_re, conj_re, conj_im]

Premises used: RCLike.conj_re, RCLike.star_def, map_add, RCLike.conj_im, RCLike.mul_re