[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
let w i := if h : w' i = 0 then (1 : Units ℂ) else Units.mk0 (w' i) h
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 := by
  intro i hi
  exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
⊢ ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
i : ι
hi : ↑(w i) ^ (-(1 / 2)) = 0
⊢ False
[PROOFSTEP]
exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
⊢ IsometryEquiv (weightedSumSquares ℂ w') (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1)
[PROOFSTEP]
convert
  (weightedSumSquares ℂ w').isometryEquivBasisRepr
    ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit)
[GOAL]
case h.e'_10
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
⊢ (weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1) =
    basisRepr (weightedSumSquares ℂ w')
      (Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2)))))
[PROOFSTEP]
ext1 v
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
⊢ ↑(weightedSumSquares ℂ fun i => if w' i = 0 then 0 else 1) v =
    ↑(basisRepr (weightedSumSquares ℂ w')
          (Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))))
      v
[PROOFSTEP]
erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
⊢ ∑ i : ι, (if w' i = 0 then 0 else 1) • (v i * v i) =
    ∑ i : ι,
      w' i •
        (Finset.sum univ
            (fun i =>
              v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
            i *
          Finset.sum univ
            (fun i =>
              v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j *
        Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j)
[PROOFSTEP]
have hsum :
  (∑ i : ι, v i • ((isUnit_iff_ne_zero.2 <| hw' i).unit : ℂ) • (Pi.basisFun ℂ ι) i) j = v j • w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ∀ (b : ι), b ∈ univ → b ≠ j → (v b • ↑(IsUnit.unit (_ : IsUnit (↑(w b) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) b) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
intro i _ hij
[GOAL]
case h₀
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
i : ι
a✝ : i ∈ univ
hij : i ≠ j
⊢ (v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j = 0
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
⊢ ¬j ∈ univ → (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w j) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) j) j = 0
[PROOFSTEP]
intro hj'
[GOAL]
case h₁
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hj' : ¬j ∈ univ
⊢ (v j • ↑(IsUnit.unit (_ : IsUnit (↑(w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) i)
          j *
        Finset.sum univ
          (fun i =>
            v i • ↑(Basis.unitsSMul (Pi.basisFun ℂ ι) fun i => IsUnit.unit (_ : IsUnit (↑(w 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' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) • (v j * v j) =
    w' j •
      (Finset.sum univ (fun x => v x • IsUnit.unit (_ : IsUnit (↑(w x) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℂ ι) x) j *
        Finset.sum univ (fun x => v x • IsUnit.unit (_ : IsUnit (↑(w x) ^ (-(1 / 2)))) • ↑(Pi.basisFun ℂ ι) x) j)
[PROOFSTEP]
erw [hsum, smul_eq_mul]
[GOAL]
case h.e'_10.H
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
⊢ (if w' j = 0 then 0 else 1) * (v j * v j) = w' j • (v j • ↑(w j) ^ (-(1 / 2)) * v j • ↑(w j) ^ (-(1 / 2)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : w' j = 0
⊢ 0 * (v j * v j) = w' j • (v j • ↑1 ^ (-(1 / 2)) * v j • ↑1 ^ (-(1 / 2)))
[PROOFSTEP]
simp only [h, zero_smul, zero_mul]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
⊢ 1 * (v j * v j) = w' j • (v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)) * v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)))
[PROOFSTEP]
have hww' : w' j = w j := by simp only [dif_neg h, Units.val_mk0]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
⊢ w' j = ↑(w j)
[PROOFSTEP]
simp only [dif_neg h, Units.val_mk0]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ 1 * (v j * v j) = w' j • (v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)) * v j • ↑(Units.mk0 (w' j) h) ^ (-(1 / 2)))
[PROOFSTEP]
simp only [one_mul, Units.val_mk0, smul_eq_mul]
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = w' j * (v j * w' j ^ (-(1 / 2)) * (v j * w' j ^ (-(1 / 2))))
[PROOFSTEP]
rw [hww']
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
suffices v j * v j = w j ^ (-(1 / 2 : ℂ)) * w j ^ (-(1 / 2 : ℂ)) * w j * v j * v j by rw [this]; ring
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
this : v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
⊢ v j * v j = ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
rw [this]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
this : v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
⊢ ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j =
    ↑(w j) * (v j * ↑(w j) ^ (-(1 / 2)) * (v j * ↑(w j) ^ (-(1 / 2))))
[PROOFSTEP]
ring
[GOAL]
case neg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ v j * v j = ↑(w j) ^ (-(1 / 2)) * ↑(w j) ^ (-(1 / 2)) * ↑(w j) * v j * v j
[PROOFSTEP]
rw [← Complex.cpow_add _ _ (w j).ne_zero, show -(1 / 2 : ℂ) + -(1 / 2) = -1 by simp [← two_mul], Complex.cpow_neg_one,
  inv_mul_cancel (w j).ne_zero, one_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w' : ι → ℂ
w : ι → ℂˣ := fun i => if h : w' i = 0 then 1 else Units.mk0 (w' i) h
hw' : ∀ (i : ι), ↑(w i) ^ (-(1 / 2)) ≠ 0
v : ι → ℂ
j : ι
hj : j ∈ univ
hsum :
  Finset.sum univ (fun i => v i • ↑(IsUnit.unit (_ : IsUnit (↑(w i) ^ (-(1 / 2))))) • ↑(Pi.basisFun ℂ ι) i) j =
    v j • ↑(w j) ^ (-(1 / 2))
h : ¬w' j = 0
hww' : w' j = ↑(w j)
⊢ -(1 / 2) + -(1 / 2) = -1
[PROOFSTEP]
simp [← two_mul]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
w : ι → ℂˣ
⊢ IsometryEquiv (weightedSumSquares ℂ w) (weightedSumSquares ℂ 1)
[PROOFSTEP]
simpa using isometryEquivSumSquares ((↑) ∘ w)
