-- 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
h₂ : ‖x + x‖ = HSMul.hSMul (α := ℕ) 2 ‖x‖
⊢ 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 rw : HPow.hPow (β := ℕ) ‖x‖ 2 =
  4 / (HMul.hMul (α := ℝ) 4 4 + HMul.hMul (α := ℝ) 0 0) *
      (HSMul.hSMul (α := ℕ) 2 ‖x‖ * HSMul.hSMul (α := ℕ) 2 ‖x‖ - HMul.hMul (α := ℝ) 0 0 -
            (HMul.hMul (α := ℝ) 0 0 - 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) *
      (HSMul.hSMul (α := ℕ) 2 ‖x‖ * 0 + 0 * HSMul.hSMul (α := ℕ) 2 ‖x‖ -
            (HMul.hMul (α := ℝ) 0 0 + HMul.hMul (α := ℝ) 0 0) +
          ((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: rw [h₁, h₂]