awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) (inner_ 𝕜 x x)
have simp : HPow.hPow (β := ℕ) ‖x‖ 2 =
  4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
      (‖x + x‖ * ‖x + x‖ - HMul.hMul (α := ℝ) 0 0 - (‖x - x‖ * ‖x - x‖ - HMul.hMul (α := ℝ) 0 0) +
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
              0) -
        ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
              HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
          (HMul.hMul (α := ℝ) 0 0 +
              HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
            0)) -
    -0 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
      (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              0 +
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) -
        ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
              HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
            0 +
          (HMul.hMul (α := ℝ) 0 0 +
              HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
            ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖))
Tactic: simp only [inner_, normSq_apply, ofNat_re, ofNat_im, map_sub, map_add,
    ofReal_re, ofReal_im, mul_re, inv_re, mul_im, I_re, inv_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * ‖x + x‖ - HMul.hMul (α := ℝ) 0 0 - (‖x - x‖ * ‖x - x‖ - HMul.hMul (α := ℝ) 0 0) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                0) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              0)) -
      -0 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                0 +
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              0 +
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖))
have h₁ : ‖x - x‖ = 0
Tactic: have h₁ : ‖x - x‖ = 0 := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖
have h : x + x = HSMul.hSMul (α := ℕ) 2 x
Tactic: convert! norm_nsmul 𝕜 2 x using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * ‖x + x‖ - HMul.hMul (α := ℝ) 0 0 - (‖x - x‖ * ‖x - x‖ - HMul.hMul (α := ℝ) 0 0) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                0) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              0)) -
      -0 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
        (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
            ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖ -
                  HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
                0 +
              (HMul.hMul (α := ℝ) 0 0 +
                  HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) *
                ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + x‖) -
          ((0 * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖ -
                HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (0 : ℝ)) *
              0 +
            (HMul.hMul (α := ℝ) 0 0 +
                HMul.hMul (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖) *
              ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - x‖))
have h₂ : ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖
Tactic: have h₂ : ‖x + x‖ = 2 • ‖x‖ := by convert! norm_nsmul 𝕜 2 x using 2; module
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner_ 𝕜 y x) = inner_ 𝕜 x y
have simp : 4⁻¹ *
    (HMul.hMul (α := 𝕜) (↑‖y + x‖ : 𝕜) (↑‖y + x‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖y - x‖ : 𝕜) (↑‖y - x‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
      HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
        (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
  4⁻¹ *
    (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: simp only [inner_, map_sub, map_add, map_mul, map_inv₀, map_ofNat, conj_ofReal, conj_I]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖y + x‖ : 𝕜) (↑‖y + x‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖y - x‖ : 𝕜) (↑‖y - x‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have rw : 4⁻¹ *
    (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
      HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
        (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
  4⁻¹ *
    (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 [add_comm y x, norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have pos : ∀ (hI : Eq.{u_1 + 1} (α := 𝕜) I 0),
  4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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: by_cases hI : (I : 𝕜) = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have hI' : HMul.hMul (α := 𝕜) I I = -1
Tactic: have hI' := I_mul_I_of_nonzero hI
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
v : E
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
have rw : norm.{u_1} (E := 𝕜) I * ‖v‖ = ‖v‖
Tactic: rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
v : E
rw : norm.{u_1} (E := 𝕜) I * ‖v‖ = ‖v‖
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
have rw₁ : 1 * ‖v‖ = ‖v‖
Tactic: rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
v : E
rw : norm.{u_1} (E := 𝕜) I * ‖v‖ = ‖v‖
rw₁ : 1 * ‖v‖ = ‖v‖
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
have rw₂ : ‖v‖ = ‖v‖
Tactic: rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
Tactic: have I_smul (v : E) : ‖(I : 𝕜) • v‖ = ‖v‖ := by rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x =
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y)
Tactic: convert! I_smul ((I : 𝕜) • x + y) using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y)
have a : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x + HMul.hMul (α := 𝕜) I I • x -
    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) x) =
  0
Tactic: linear_combination (norm := module) -hI' • x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have h₁ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖
Tactic: have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ := by
    convert! I_smul ((I : 𝕜) • x + y) using 2
    linear_combination (norm := module) -hI' • x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
h₁ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖
⊢ ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖
have h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y =
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x)
Tactic: convert! (I_smul ((I : 𝕜) • y + x)).symm using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
h₁ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x)
have a : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y + HMul.hMul (α := 𝕜) I I • y -
    (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (-1) y) =
  0
Tactic: linear_combination (norm := module) -hI' • y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
hI' : HMul.hMul (α := 𝕜) I I = -1
I_smul : ∀ (v : E), ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I v‖ = ‖v‖
h₁ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜) +
          HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) *
            (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ : 𝕜) -
        HMul.hMul (α := 𝕜) (-I) (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜) *
          (↑‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y - x‖ : 𝕜)) =
    4⁻¹ *
      (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‖ : 𝕜))
have h₂ : ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y + x‖ = ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖
Tactic: have h₂ : ‖(I : 𝕜) • y + x‖ = ‖(I : 𝕜) • x - y‖ := by
    convert! (I_smul ((I : 𝕜) • y + x)).symm using 2
    linear_combination (norm := module) -hI' • y