VAbs sum sq row eq one

lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :    (VAbs i 0 V) ^ 2 + (VAbs i 1 V) ^ 2 + (VAbs i 2 V) ^ 2 = 1 := by  obtain ⟨V, hV⟩ := Quot.exists_rep V  subst hV  have hV := V.prop  rw [mem_unitaryGroup_iff] at hV  have ht := congrFun (congrFun hV i) i  simp only [mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, Fin.isValue,    one_apply_eq] at ht  rw [mul_conj, mul_conj, mul_conj] at ht  repeat rw [← Complex.sq_norm] at ht  rw [← ofReal_inj]  simp_all only [SetLike.coe_mem, Unitary.mul_star_self_of_mem, Fin.isValue, ofReal_pow, ofReal_add,    ofReal_one]  exact ht