[STATEMENT]
lemma cinner_basis_enum_of_vec:
  defines "n \<equiv> length (canonical_basis :: 'a::onb_enum list)"
  assumes [simp]: "dim_vec x = n" "dim_vec y = n"
  shows  "(basis_enum_of_vec x :: 'a) \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>(basis_enum_of_vec x :: 'a) \<bullet>\<^sub>C basis_enum_of_vec y
    = (\<Sum>i<n. x$i *\<^sub>C canonical_basis ! i :: 'a) \<bullet>\<^sub>C (\<Sum>i<n. y$i *\<^sub>C canonical_basis ! i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)
[PROOF STEP]
by (auto simp: basis_enum_of_vec_def sum_list_sum_nth atLeast0LessThan simp flip: n_def)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. \<Sum>j<n. cnj (x$i) *\<^sub>C y$j *\<^sub>C ((canonical_basis ! i :: 'a) \<bullet>\<^sub>C (canonical_basis ! j)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
apply (subst cinner_sum_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa<n. x $ xa *\<^sub>C canonical_basis ! xa \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
apply (subst cinner_sum_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>xa<n. \<Sum>ya<n. x $ xa *\<^sub>C canonical_basis ! xa \<bullet>\<^sub>C y $ ya *\<^sub>C canonical_basis ! ya) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))
[PROOF STEP]
by (auto simp: mult_ac)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. x $ i *\<^sub>C canonical_basis ! i) \<bullet>\<^sub>C (\<Sum>i<n. y $ i *\<^sub>C canonical_basis ! i) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. \<Sum>j<n. cnj (x$i) *\<^sub>C y$j *\<^sub>C (if i=j then 1 else 0))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! xa \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0))
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. \<lbrakk>xa \<in> {..<n}; xaa \<in> {..<n}\<rbrakk> \<Longrightarrow> cnj (x $ xa) *\<^sub>C y $ xaa *\<^sub>C (canonical_basis ! xa \<bullet>\<^sub>C canonical_basis ! xaa) = cnj (x $ xa) *\<^sub>C y $ xaa *\<^sub>C (if xa = xaa then 1 else 0)
[PROOF STEP]
by (auto simp: cinner_canonical_basis n_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (canonical_basis ! i \<bullet>\<^sub>C canonical_basis ! j)) = (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0))

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. cnj (x$i) *\<^sub>C y$i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)
[PROOF STEP]
apply (rule sum.cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (\<Sum>j<n. cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0)) = cnj (x $ xa) *\<^sub>C y $ xa
[PROOF STEP]
apply (subst sum_single)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> finite {..<n}
 2. \<And>xa j. \<lbrakk>xa \<in> {..<n}; j \<noteq> ?i3 xa; j \<in> {..<n}\<rbrakk> \<Longrightarrow> cnj (x $ xa) *\<^sub>C y $ j *\<^sub>C (if xa = j then 1 else 0) = 0
 3. \<And>xa. xa \<in> {..<n} \<Longrightarrow> (if ?i3 xa \<in> {..<n} then cnj (x $ xa) *\<^sub>C y $ ?i3 xa *\<^sub>C (if xa = ?i3 xa then 1 else 0) else 0) = cnj (x $ xa) *\<^sub>C y $ xa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. \<Sum>j<n. cnj (x $ i) *\<^sub>C y $ j *\<^sub>C (if i = j then 1 else 0)) = (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i)

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
have \<open>\<dots> = y \<bullet>c x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i) = y \<bullet>c x
[PROOF STEP]
by (smt (z3) assms(2) complex_scaleC_def conjugate_complex_def dim_vec_conjugate lessThan_atLeast0 lessThan_iff mult.commute scalar_prod_def sum.cong vec_index_conjugate)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. cnj (x $ i) *\<^sub>C y $ i) = y \<bullet>c x

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x

goal (1 subgoal):
 1. basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec x \<bullet>\<^sub>C basis_enum_of_vec y = y \<bullet>c x

goal:
No subgoals!
[PROOF STEP]
qed