[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
⊢ IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (sign ∘ w))
[PROOFSTEP]
let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
⊢ IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (sign ∘ w))
[PROOFSTEP]
have hu' : ∀ i : ι, (Real.sign (u i) * u i) ^ (-(1 / 2 : ℝ)) ≠ 0 :=
  by
  intro i
  refine' (ne_of_lt (Real.rpow_pos_of_pos (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _) _)).symm
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
⊢ ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
i : ι
⊢ (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
[PROOFSTEP]
refine' (ne_of_lt (Real.rpow_pos_of_pos (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _) _)).symm
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
⊢ IsometryEquiv (weightedSumSquares ℝ w) (weightedSumSquares ℝ (sign ∘ w))
[PROOFSTEP]
convert
  (weightedSumSquares ℝ w).isometryEquivBasisRepr
    ((Pi.basisFun ℝ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hu' i).unit)
[GOAL]
case h.e'_10
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
⊢ weightedSumSquares ℝ (sign ∘ w) =
    basisRepr (weightedSumSquares ℝ w)
      (Basis.unitsSMul (Pi.basisFun ℝ ι) fun i => IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
[PROOFSTEP]
ext1 v
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
⊢ ↑(weightedSumSquares ℝ (sign ∘ w)) v =
    ↑(basisRepr (weightedSumSquares ℝ w)
          (Basis.unitsSMul (Pi.basisFun ℝ ι) fun i => IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))))
      v
[PROOFSTEP]
rw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
⊢ ∑ i : ι, (sign ∘ w) i • (v i * v i) =
    ∑ i : ι,
      w i •
        (Finset.sum univ
            (fun i =>
              v i •
                ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                      IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                  i)
            i *
          Finset.sum univ
            (fun i =>
              v i •
                ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                      IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                  i)
            i)
[PROOFSTEP]
refine' sum_congr rfl fun j hj => _
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ (sign ∘ w) j • (v j * v j) =
    w j •
      (Finset.sum univ
          (fun i =>
            v i •
              ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                    IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                i)
          j *
        Finset.sum univ
          (fun i =>
            v i •
              ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                    IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                i)
          j)
[PROOFSTEP]
have hsum :
  (∑ i : ι, v i • ((isUnit_iff_ne_zero.2 <| hu' i).unit : ℝ) • (Pi.basisFun ℝ ι) i) j =
    v j • (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) :=
  by
  rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec, LinearMap.stdBasis_apply, Pi.smul_apply,
    Pi.smul_apply, Function.update_same, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_one]
  intro i _ hij
  rw [Pi.basisFun_apply, LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply, Function.update_noteq hij.symm,
    Pi.zero_apply, smul_eq_mul, smul_eq_mul, mul_zero, mul_zero]
  intro hj'; exact False.elim (hj' hj)
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
[PROOFSTEP]
rw [Finset.sum_apply, sum_eq_single j, Pi.basisFun_apply, IsUnit.unit_spec, LinearMap.stdBasis_apply, Pi.smul_apply,
  Pi.smul_apply, Function.update_same, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_one]
[GOAL]
case h₀
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ ∀ (b : ι),
    b ∈ univ →
      b ≠ j → (v b • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u b) * ↑(u b)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) b) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) j) j = 0
[PROOFSTEP]
intro i _ hij
[GOAL]
case h₀
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
i : ι
a✝ : i ∈ univ
hij : i ≠ j
⊢ (v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) j) j = 0
[PROOFSTEP]
rw [Pi.basisFun_apply, LinearMap.stdBasis_apply, Pi.smul_apply, Pi.smul_apply, Function.update_noteq hij.symm,
  Pi.zero_apply, smul_eq_mul, smul_eq_mul, mul_zero, mul_zero]
[GOAL]
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) j) j = 0
[PROOFSTEP]
intro hj'
[GOAL]
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hj' : ¬j ∈ univ
⊢ (v j • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) j) j = 0
[PROOFSTEP]
exact False.elim (hj' hj)
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
⊢ (sign ∘ w) j • (v j * v j) =
    w j •
      (Finset.sum univ
          (fun i =>
            v i •
              ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                    IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                i)
          j *
        Finset.sum univ
          (fun i =>
            v i •
              ↑(Basis.unitsSMul (Pi.basisFun ℝ ι) fun i =>
                    IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)))))
                i)
          j)
[PROOFSTEP]
simp_rw [Basis.unitsSMul_apply]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
⊢ (sign ∘ w) j • (v j * v j) =
    w j •
      (Finset.sum univ
          (fun x => v x • IsUnit.unit (_ : IsUnit ((sign ↑(u x) * ↑(u x)) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℝ ι) x) j *
        Finset.sum univ
          (fun x => v x • IsUnit.unit (_ : IsUnit ((sign ↑(u x) * ↑(u x)) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℝ ι) x) j)
[PROOFSTEP]
erw [hsum]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
⊢ (sign ∘ w) j • (v j * v j) =
    w j • (v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)))
[PROOFSTEP]
simp only [Function.comp, smul_eq_mul]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
⊢ sign (w j) * (v j * v j) =
    w j *
      (v j *
          (sign ↑(if h : w j = 0 then 1 else Units.mk0 (w j) h) * ↑(if h : w j = 0 then 1 else Units.mk0 (w j) h)) ^
            (-(1 / 2)) *
        (v j *
          (sign ↑(if h : w j = 0 then 1 else Units.mk0 (w j) h) * ↑(if h : w j = 0 then 1 else Units.mk0 (w j) h)) ^
            (-(1 / 2))))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : w j = 0
⊢ sign (w j) * (v j * v j) = w j * (v j * (sign ↑1 * ↑1) ^ (-(1 / 2)) * (v j * (sign ↑1 * ↑1) ^ (-(1 / 2))))
[PROOFSTEP]
simp only [h, zero_smul, zero_mul, Real.sign_zero]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
⊢ sign (w j) * (v j * v j) =
    w j *
      (v j * (sign ↑(Units.mk0 (w j) h) * ↑(Units.mk0 (w j) h)) ^ (-(1 / 2)) *
        (v j * (sign ↑(Units.mk0 (w j) h) * ↑(Units.mk0 (w j) h)) ^ (-(1 / 2))))
[PROOFSTEP]
have hwu : w j = u j := by simp only [dif_neg h, Units.val_mk0]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
⊢ w j = ↑(u j)
[PROOFSTEP]
simp only [dif_neg h, Units.val_mk0]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
⊢ sign (w j) * (v j * v j) =
    w j *
      (v j * (sign ↑(Units.mk0 (w j) h) * ↑(Units.mk0 (w j) h)) ^ (-(1 / 2)) *
        (v j * (sign ↑(Units.mk0 (w j) h) * ↑(Units.mk0 (w j) h)) ^ (-(1 / 2))))
[PROOFSTEP]
simp only [Units.val_mk0]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
⊢ sign (w j) * (v j * v j) = w j * (v j * (sign (w j) * w j) ^ (-(1 / 2)) * (v j * (sign (w j) * w j) ^ (-(1 / 2))))
[PROOFSTEP]
rw [hwu]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
⊢ sign ↑(u j) * (v j * v j) =
    ↑(u j) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))
[PROOFSTEP]
suffices
  (u j : ℝ).sign * v j * v j =
    (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) * (Real.sign (u j) * u j) ^ (-(1 / 2 : ℝ)) * u j * v j * v j
  by erw [← mul_assoc, this]; ring
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
this :
  sign ↑(u j) * v j * v j =
    (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * ↑(u j) * v j * v j
⊢ sign ↑(u j) * (v j * v j) =
    ↑(u j) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))
[PROOFSTEP]
erw [← mul_assoc, this]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
this :
  sign ↑(u j) * v j * v j =
    (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * ↑(u j) * v j * v j
⊢ (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * ↑(u j) * v j * v j =
    ↑(u j) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (v j * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))))
[PROOFSTEP]
ring
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
⊢ sign ↑(u j) * v j * v j =
    (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2)) * ↑(u j) * v j * v j
[PROOFSTEP]
rw [← Real.rpow_add (sign_mul_pos_of_ne_zero _ <| Units.ne_zero _), show -(1 / 2 : ℝ) + -(1 / 2) = -1 by ring,
  Real.rpow_neg_one, mul_inv, inv_sign, mul_assoc (Real.sign (u j)) (u j)⁻¹, inv_mul_cancel (Units.ne_zero _), mul_one]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℝ
u : ι → ℝˣ := fun i => if h : w i = 0 then 1 else Units.mk0 (w i) h
hu' : ∀ (i : ι), (sign ↑(u i) * ↑(u i)) ^ (-(1 / 2)) ≠ 0
v : ι → ℝ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ
      (fun i => v i • ↑(IsUnit.unit (_ : IsUnit ((sign ↑(u i) * ↑(u i)) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℝ ι) i) j =
    v j • (sign ↑(u j) * ↑(u j)) ^ (-(1 / 2))
h : ¬w j = 0
hwu : w j = ↑(u j)
⊢ -(1 / 2) + -(1 / 2) = -1
[PROOFSTEP]
ring
