awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
h3 : ‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
h4 : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
h5 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖)
h6 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖)
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ + ‖z‖ * ‖z‖)

Tactic:
have h7 := parallelogram_identity ((I : 𝕜) • y + z) z
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
h3 : ‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
h4 : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
h5 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖)
h6 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖)
h7 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ + ‖z‖ * ‖z‖)
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ + ‖z‖ * ‖z‖)

Tactic:
have h8 := parallelogram_identity ((I : 𝕜) • y - z) z
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y z : E
h1 :
  ‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖ =
    2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
h2 :
  ‖x + y - z + (x + z)‖ * ‖x + y - z + (x + z)‖ + ‖x + y - z - (x + z)‖ * ‖x + y - z - (x + z)‖ =
    2 * (‖x + y - z‖ * ‖x + y - z‖ + ‖x + z‖ * ‖x + z‖)
h3 : ‖y + z + z‖ * ‖y + z + z‖ + ‖y + z - z‖ * ‖y + z - z‖ = 2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖)
h4 : ‖y - z + z‖ * ‖y - z + z‖ + ‖y - z - z‖ * ‖y - z - z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)
h5 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) + z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - z‖)
h6 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z + (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ *
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z - (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z)‖ =
    2 *
      (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (x + y) - z‖ +
        ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + z‖)
h7 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + z‖ + ‖z‖ * ‖z‖)
h8 :
  ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z + z‖ +
      ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z - z‖ =
    2 * (‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - z‖ + ‖z‖ * ‖z‖)
⊢ Eq (α := 𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (‖x + y + z + (x - z)‖ * ‖x + y + z + (x - z)‖ + ‖x + y + z - (x - z)‖ * ‖x + y + z - (x - z)‖) :
      𝕜)
    ((𝓚 : (a : ℝ) → 𝕜) (2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)) : 𝕜)

Tactic:
apply_fun 𝓚 at h1 h2 h3 h4 h5 h6 h7 h8
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : ℚ
x y : E
a b : 𝕜
⊢ (fun (r : 𝕜) ↦ inner_ 𝕜 (r • x) y) (a + b) =
    HAdd.hAdd (α := 𝕜) ((fun (r : 𝕜) ↦ inner_ 𝕜 (r • x) y) a) ((fun (r : 𝕜) ↦ inner_ 𝕜 (r • x) y) b)

Tactic:
simpa [add_smul] using add_left (a • x) (b • x) y

Premises used: InnerProductSpaceable.add_left, add_smul, HSMul.hSMul
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : ℚ
x y : E
hom : 𝕜 →ₗ[ℚ] 𝕜 := AddMonoidHom.toRatLinearMap (AddMonoidHom.mk' (fun (r : 𝕜) ↦ inner_ 𝕜 (r • x) y) ⋯)
⊢ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
simpa [hom, Rat.smul_def] using map_smul hom r 1

Premises used: OfNat.ofNat, Rat.smul_def, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : ℝ
x y : E
revert :
  ∀ (r : ℝ),
    inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y =
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)
⊢ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
revert r
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
rw :
  Eq.{max 1 (u_1 + 1)} (α := (x : ℝ) → 𝕜) (fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y)
    fun (r : ℝ) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)
⊢ ∀ (r : ℝ),
    inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y =
      HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
rw [← funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
⊢ Eq.{max 1 (u_1 + 1)} (α := (x : ℝ) → 𝕜) (fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y)
    fun (r : ℝ) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
Rat.isDenseEmbedding_coe_real.dense.equalizer ?_ ?_ (funext fun X => ?_)

Premises used: IsDenseEmbedding.toIsDenseInducing, DenseRange.equalizer, Rat.isDenseEmbedding_coe_real, funext, IsDenseInducing.dense
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
refine_1 : Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y
refine_2 :
  Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)
refine_3 :
  ∀ (X : ℚ),
    Eq.{u_1 + 1} (α := 𝕜) (((fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y) ∘ Rat.cast) X)
      (((fun (r : ℝ) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)) ∘ Rat.cast) X)
⊢ Eq.{max 1 (u_1 + 1)} (α := (x : ℝ) → 𝕜) (fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y)
    fun (r : ℝ) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
refine Rat.isDenseEmbedding_coe_real.dense.equalizer ?_ ?_ (funext fun X => ?_)

Premises used: IsDenseEmbedding.toIsDenseInducing, DenseRange.equalizer, Rat.isDenseEmbedding_coe_real, funext, IsDenseInducing.dense
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y

Tactic:
(continuous_ofReal.smul continuous_const).inner_ continuous_const

Premises used: continuous_const, RCLike.continuous_ofReal, Continuous.smul, Continuous.inner_
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y

Tactic:
exact (continuous_ofReal.smul continuous_const).inner_ continuous_const

Premises used: continuous_const, RCLike.continuous_ofReal, Continuous.smul, Continuous.inner_
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
(continuous_conj.comp continuous_ofReal).mul continuous_const

Premises used: Continuous.comp, continuous_const, RCLike.continuous_ofReal, Continuous.mul, RCLike.continuous_conj
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
⊢ Continuous.{0, u_1} (Y := 𝕜) fun (r : ℝ) ↦
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)

Tactic:
exact (continuous_conj.comp continuous_ofReal).mul continuous_const

Premises used: Continuous.comp, continuous_const, RCLike.continuous_ofReal, Continuous.mul, RCLike.continuous_conj
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
x y : E
X : ℚ
⊢ Eq.{u_1 + 1} (α := 𝕜) (((fun (r : ℝ) ↦ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) x) y) ∘ Rat.cast) X)
    (((fun (r : ℝ) ↦ HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (↑r : 𝕜) : 𝕜) (inner_ 𝕜 x y)) ∘ Rat.cast) X)

Tactic:
simp only [Function.comp_apply, RCLike.ofReal_ratCast, rat_prop _ _]

Premises used: Function.comp_apply, _private.0.InnerProductSpaceable.rat_prop, RCLike.ofReal_ratCast
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
pos : ∀ (hI : Eq.{u_1 + 1} (α := 𝕜) I 0), innerProp'.{u_1, u_2} (𝕜 := 𝕜) E I
neg : ∀ (hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0), innerProp'.{u_1, u_2} (𝕜 := 𝕜) E I
⊢ innerProp'.{u_1, u_2} (𝕜 := 𝕜) E I

Tactic:
by_cases hI : (I : 𝕜) = 0

Premises used: RCLike.I
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : Eq.{u_1 + 1} (α := 𝕜) I 0
pos : innerProp'.{u_1, u_2} (𝕜 := 𝕜) E 0
⊢ innerProp'.{u_1, u_2} (𝕜 := 𝕜) E I

Tactic:
rw [hI]
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ innerProp'.{u_1, u_2} (𝕜 := 𝕜) E 0

Tactic:
simpa using real_prop (𝕜 := 𝕜) 0

Premises used: _private.0.InnerProductSpaceable.real_prop, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
⊢ HMul.hMul (α := 𝕜) I I = -1

Tactic:
have hI' := I_mul_I_of_nonzero hI
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
neg :
  4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
⊢ inner_ 𝕜 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x) y =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) I : 𝕜) (inner_ 𝕜 x y)

Tactic:
rw [conj_I, inner_, inner_, mul_left_comm, smul_smul, hI', neg_one_smul]

Premises used: neg_one_smul, _private.0.inner_, smul_smul, mul_left_comm, RCLike.conj_I
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
rw : ‖-(x + y)‖ = ‖x + y‖
rw₁ rw₂ : ‖x + y‖ = ‖x + y‖
⊢ ‖-x - y‖ = ‖x + y‖

Tactic:
rw [← neg_add', norm_neg]

Premises used: neg_add', norm_neg
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
⊢ ‖-x - y‖ = ‖x + y‖

Tactic:
have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
rw : ‖-x + y‖ = ‖-(y - x)‖
rw₁ : ‖-x + y‖ = ‖y - x‖
rw₂ rw₃ : ‖-x + y‖ = ‖-x + y‖
⊢ ‖-x + y‖ = ‖x - y‖

Tactic:
rw [← neg_sub, norm_neg, sub_eq_neg_add]

Premises used: neg_sub, sub_eq_neg_add, norm_neg
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ‖-x + y‖ = ‖x - y‖

Tactic:
have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
neg :
  4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))

Tactic:
rw [h₁, h₂]