Theory Hilbert_Space_Tensor_Product

section ‹‹Hilbert_Space_Tensor_Product› -- Tensor product of Hilbert Spaces›

theory Hilbert_Space_Tensor_Product
  imports Complex_Bounded_Operators.Complex_L2 Misc_Tensor_Product
    Strong_Operator_Topology Polynomial_Interpolation.Ring_Hom
    Positive_Operators Weak_Star_Topology Spectral_Theorem Trace_Class
begin

unbundle cblinfun_syntax
hide_const (open) Determinants.trace
hide_fact (open) Determinants.trace_def

subsection ‹Tensor product on \<^typ>‹_ ell2››

lift_definition tensor_ell2 :: ‹'a ell2 ⇒ 'b ell2 ⇒ ('a×'b) ell2› (infixr "⊗⇩s" 70) is
  ‹λψ φ (i,j). ψ i * φ j›
proof -
  fix ψ :: ‹'a ⇒ complex› and φ :: ‹'b ⇒ complex›
  assume ‹has_ell2_norm ψ› ‹has_ell2_norm φ›
  from ‹has_ell2_norm φ› have φ_sum: ‹(λj. (ψ i * φ j)⇧2) abs_summable_on UNIV› for i
    by (metis ell2_norm_smult(1) has_ell2_norm_def)
  have double_sum: ‹(λi. ∑⇩∞j. cmod ((ψ i * φ j)⇧2)) abs_summable_on UNIV›
    unfolding norm_mult power_mult_distrib infsum_cmult_right'
    by (rule summable_on_cmult_left) (use ‹has_ell2_norm ψ› in ‹auto simp: has_ell2_norm_def›)
  have ‹(λ(i,j). (ψ i * φ j)⇧2) abs_summable_on UNIV × UNIV›
    by (rule abs_summable_on_Sigma_iff[THEN iffD2]) (use φ_sum double_sum in auto)
  then show ‹has_ell2_norm (λ(i, j). ψ i * φ j)›
    by (auto simp add: has_ell2_norm_def case_prod_beta)
qed

lemma tensor_ell2_add1: ‹tensor_ell2 (a + b) c = tensor_ell2 a c + tensor_ell2 b c›
  by transfer (auto simp: case_prod_beta vector_space_over_itself.scale_left_distrib)

lemma tensor_ell2_add2: ‹tensor_ell2 a (b + c) = tensor_ell2 a b + tensor_ell2 a c›
  by transfer (auto simp: case_prod_beta algebra_simps)

lemma tensor_ell2_scaleC1: ‹tensor_ell2 (c *⇩C a) b = c *⇩C tensor_ell2 a b›
  by transfer (auto simp: case_prod_beta)

lemma tensor_ell2_scaleC2: ‹tensor_ell2 a (c *⇩C b) = c *⇩C tensor_ell2 a b›
  by transfer (auto simp: case_prod_beta)

lemma tensor_ell2_diff1: ‹tensor_ell2 (a - b) c = tensor_ell2 a c - tensor_ell2 b c›
  by transfer (auto simp: case_prod_beta ordered_field_class.sign_simps)

lemma tensor_ell2_diff2: ‹tensor_ell2 a (b - c) = tensor_ell2 a b - tensor_ell2 a c›
  by transfer (auto simp: case_prod_beta ordered_field_class.sign_simps)

lemma tensor_ell2_inner_prod[simp]: ‹tensor_ell2 a b ∙⇩C tensor_ell2 c d = (a ∙⇩C c) * (b ∙⇩C d)›
  apply (rule local_defE[where y=‹tensor_ell2 a b›], rename_tac ab)
  apply (rule local_defE[where y=‹tensor_ell2 c d›], rename_tac cd)
proof (transfer, hypsubst_thin)
  fix a c :: ‹'a ⇒ complex› and b d :: ‹'b ⇒ complex›

  assume assms: ‹has_ell2_norm (λ(i, j). a i * b j)› ‹has_ell2_norm (λ(i, j). c i * d j)›

  have *: ‹(λxy. cnj (a (fst xy) * b (snd xy)) * (c (fst xy) * d (snd xy))) abs_summable_on UNIV›
    apply (rule abs_summable_product)
    subgoal
      by (metis (mono_tags, lifting) assms(1) complex_mod_cnj has_ell2_norm_def norm_power split_def summable_on_cong)
    subgoal
      by (metis (mono_tags, lifting) assms(2) case_prod_unfold has_ell2_norm_def summable_on_cong)
    done

  then have *: ‹(λ(x, y). cnj (a x * b y) * (c x * d y)) summable_on UNIV × UNIV›
    using abs_summable_summable by (auto simp: case_prod_unfold)

  have ‹(∑⇩∞i. cnj (case i of (i, j) ⇒ a i * b j) * (case i of (i, j) ⇒ c i * d j))
     = (∑⇩∞(i,j)∈UNIV×UNIV. cnj (a i * b j) * (c i * d j))› (is ‹?lhs = _›)
    by (simp add: case_prod_unfold)
  also have ‹… = (∑⇩∞i. ∑⇩∞j. cnj (a i * b j) * (c i * d j))›
    by (subst infsum_Sigma'_banach[symmetric]) (use * in auto)
  also have ‹… = (∑⇩∞i. cnj (a i) * c i) * (∑⇩∞j. cnj (b j) * (d j))› (is ‹_ = ?rhs›)
    by (subst infsum_cmult_left'[symmetric])
       (auto intro!: infsum_cong simp flip: infsum_cmult_right')
  finally show ‹?lhs = ?rhs› .
qed

lemma norm_tensor_ell2: ‹norm (a ⊗⇩s b) = norm a * norm b›
  by (simp add: norm_eq_sqrt_cinner[where 'a=‹(_::type) ell2›] norm_mult real_sqrt_mult)

lemma clinear_tensor_ell21: "clinear (λb. a ⊗⇩s b)"
  by (rule clinearI; transfer)
     (auto simp add: case_prod_beta cond_case_prod_eta algebra_simps fun_eq_iff)

lemma bounded_clinear_tensor_ell21: "bounded_clinear (λb. a ⊗⇩s b)"
  by (auto intro!: bounded_clinear.intro clinear_tensor_ell21
           simp: bounded_clinear_axioms_def norm_tensor_ell2 mult.commute[of "norm a"])

lemma clinear_tensor_ell22: "clinear (λa. a ⊗⇩s b)"
  by (rule clinearI; transfer) (auto simp: case_prod_beta algebra_simps)

lemma bounded_clinear_tensor_ell22: "bounded_clinear (λa. tensor_ell2 a b)"
  by (auto intro!: bounded_clinear.intro clinear_tensor_ell22
           simp: bounded_clinear_axioms_def norm_tensor_ell2)

lemma tensor_ell2_ket: "tensor_ell2 (ket i) (ket j) = ket (i,j)"
  by transfer auto

lemma tensor_ell2_0_left[simp]: ‹0 ⊗⇩s x = 0›
  by transfer auto

lemma tensor_ell2_0_right[simp]: ‹x ⊗⇩s 0 = 0›
  by transfer auto

lemma tensor_ell2_sum_left: ‹(∑x∈X. a x) ⊗⇩s b = (∑x∈X. a x ⊗⇩s b)›
  by (induction X rule:infinite_finite_induct) (auto simp: tensor_ell2_add1)

lemma tensor_ell2_sum_right: ‹a ⊗⇩s (∑x∈X. b x) = (∑x∈X. a ⊗⇩s b x)›
  by (induction X rule:infinite_finite_induct) (auto simp: tensor_ell2_add2)

lemma tensor_ell2_dense:
  fixes S :: ‹'a ell2 set› and T :: ‹'b ell2 set›
  assumes ‹closure (cspan S) = UNIV› and ‹closure (cspan T) = UNIV›
  shows ‹closure (cspan {a⊗⇩sb | a b. a∈S ∧ b∈T}) = UNIV›
proof -
  define ST where ‹ST = {a⊗⇩sb | a b. a∈S ∧ b∈T}›
  from assms have 1: ‹bounded_clinear F ⟹ bounded_clinear G ⟹ (∀x∈S. F x = G x) ⟹ F = G› for F G :: ‹'a ell2 ⇒ complex›
    using bounded_clinear_eq_on_closure[of F G S] by auto
  from assms have 2: ‹bounded_clinear F ⟹ bounded_clinear G ⟹ (∀x∈T. F x = G x) ⟹ F = G› for F G :: ‹'b ell2 ⇒ complex›
    using bounded_clinear_eq_on_closure[of F G T] by auto
  have ‹F = G› 
    if [simp]: ‹bounded_clinear F› ‹bounded_clinear G› and eq: ‹∀x∈ST. F x = G x›
    for F G :: ‹('a×'b) ell2 ⇒ complex›
  proof -
    from eq have eq': ‹F (s ⊗⇩s t) = G (s ⊗⇩s t)› if ‹s ∈ S› and ‹t ∈ T› for s t
      using ST_def that by blast
    have eq'': ‹F (s ⊗⇩s ket t) = G (s ⊗⇩s ket t)› if ‹s ∈ S› for s t
      by (rule fun_cong[where x=‹ket t›], rule 2)
         (use eq' that in ‹auto simp: bounded_clinear_compose bounded_clinear_tensor_ell21›)
    have eq''': ‹F (ket s ⊗⇩s ket t) = G (ket s ⊗⇩s ket t)› for s t
      by (rule fun_cong[where x=‹ket s›], rule 1)
         (use eq'' in ‹auto simp: bounded_clinear_compose bounded_clinear_tensor_ell21
                            intro: bounded_clinear_compose[OF _  bounded_clinear_tensor_ell22]›)
    show "F = G"
      by (rule bounded_clinear_equal_ket) (use eq''' in ‹auto simp: tensor_ell2_ket›)
  qed
  then show ‹closure (cspan ST) = UNIV›
    using separating_dense_span by blast
qed

definition assoc_ell2 :: ‹(('a×'b)×'c) ell2 ⇒⇩C⇩L ('a×('b×'c)) ell2› where
  ‹assoc_ell2 = classical_operator (Some o (λ((a,b),c). (a,(b,c))))›

lemma unitary_assoc_ell2[simp]: ‹unitary assoc_ell2›
  unfolding assoc_ell2_def
  by (rule unitary_classical_operator, rule o_bij[of ‹(λ(a,(b,c)). ((a,b),c))›]) auto

lemma assoc_ell2_tensor: ‹assoc_ell2 *⇩V ((a ⊗⇩s b) ⊗⇩s c) = (a ⊗⇩s (b ⊗⇩s c))›
proof -
  note [simp] = bounded_clinear_compose[OF bounded_clinear_tensor_ell21]
    bounded_clinear_compose[OF bounded_clinear_tensor_ell22]
    bounded_clinear_cblinfun_apply
  have ‹assoc_ell2 *⇩V ((ket a ⊗⇩s ket b) ⊗⇩s ket c) = (ket a ⊗⇩s (ket b ⊗⇩s ket c))› for a :: 'a and b :: 'b and c :: 'c
    by (simp add: inj_def assoc_ell2_def classical_operator_ket classical_operator_exists_inj tensor_ell2_ket)
  then have ‹assoc_ell2 *⇩V ((ket a ⊗⇩s ket b) ⊗⇩s c) = (ket a ⊗⇩s (ket b ⊗⇩s c))› for a :: 'a and b :: 'b
    apply -
    apply (rule fun_cong[where x=c])
    apply (rule bounded_clinear_equal_ket)
    by auto
  then have ‹assoc_ell2 *⇩V ((ket a ⊗⇩s b) ⊗⇩s c) = (ket a ⊗⇩s (b ⊗⇩s c))› for a :: 'a
    apply -
    apply (rule fun_cong[where x=b])
    apply (rule bounded_clinear_equal_ket)
    by auto
  then show ‹assoc_ell2 *⇩V ((a ⊗⇩s b) ⊗⇩s c) = (a ⊗⇩s (b ⊗⇩s c))›
    apply -
    apply (rule fun_cong[where x=a])
    apply (rule bounded_clinear_equal_ket)
    by auto
qed

lemma assoc_ell2'_tensor: ‹assoc_ell2* *⇩V tensor_ell2 a (tensor_ell2 b c) = tensor_ell2 (tensor_ell2 a b) c›
  by (metis (no_types, opaque_lifting) assoc_ell2_tensor cblinfun_apply_cblinfun_compose id_cblinfun.rep_eq unitaryD1 unitary_assoc_ell2)

lemma assoc_ell2'_inv: "assoc_ell2 o⇩C⇩L assoc_ell2* = id_cblinfun"
  by (auto intro: equal_ket)

lemma assoc_ell2_inv: "assoc_ell2* o⇩C⇩L assoc_ell2 = id_cblinfun"
  by (auto intro: equal_ket)


definition swap_ell2 :: ‹('a×'b) ell2 ⇒⇩C⇩L ('b×'a) ell2› where
  ‹swap_ell2 = classical_operator (Some o prod.swap)›

lemma unitary_swap_ell2[simp]: ‹unitary swap_ell2›
  unfolding swap_ell2_def by (rule unitary_classical_operator) auto

lemma swap_ell2_tensor[simp]: ‹swap_ell2 *⇩V (a ⊗⇩s b) = b ⊗⇩s a› for a :: ‹'a ell2› and b :: ‹'b ell2›
proof -
  note [simp] = bounded_clinear_compose[OF bounded_clinear_tensor_ell21]
    bounded_clinear_compose[OF bounded_clinear_tensor_ell22]
    bounded_clinear_cblinfun_apply
  have ‹swap_ell2 *⇩V (ket a ⊗⇩s ket b) = (ket b ⊗⇩s ket a)› for a :: 'a and b :: 'b
    by (simp add: inj_def swap_ell2_def classical_operator_ket classical_operator_exists_inj tensor_ell2_ket)
  then have ‹swap_ell2 *⇩V (ket a ⊗⇩s b) = (b ⊗⇩s ket a)› for a :: 'a
    apply -
    apply (rule fun_cong[where x=b])
    apply (rule bounded_clinear_equal_ket)
    by auto
  then show ‹swap_ell2 *⇩V (a ⊗⇩s b) = (b ⊗⇩s a)›
    apply -
    apply (rule fun_cong[where x=a])
    apply (rule bounded_clinear_equal_ket)
    by auto
qed

lemma swap_ell2_ket[simp]: ‹(swap_ell2 :: ('a×'b) ell2 ⇒⇩C⇩L _)*⇩V ket (x,y) = ket (y,x)›
  by (metis swap_ell2_tensor tensor_ell2_ket)

lemma adjoint_swap_ell2[simp]: ‹swap_ell2* = swap_ell2›
  by (simp add: swap_ell2_def inv_map_total)

lemma tensor_ell2_extensionality:
  assumes "(⋀s t. a *⇩V (s ⊗⇩s t) = b *⇩V (s ⊗⇩s t))"
  shows "a = b"
  using assms by (auto intro: equal_ket simp flip: tensor_ell2_ket)

lemma tensor_ell2_nonzero: ‹a ⊗⇩s b ≠ 0› if ‹a ≠ 0› and ‹b ≠ 0›
  by (use that in transfer) (auto simp: fun_eq_iff)

lemma swap_ell2_selfinv[simp]: ‹swap_ell2 o⇩C⇩L swap_ell2 = id_cblinfun›
  by (metis adjoint_swap_ell2 unitary_def unitary_swap_ell2)

lemma bounded_cbilinear_tensor_ell2[bounded_cbilinear]: ‹bounded_cbilinear (⊗⇩s)›
proof standard
  fix a a' :: "'a ell2" and b b' :: "'b ell2" and r :: complex
  show ‹tensor_ell2 (a + a') b = tensor_ell2 a b + tensor_ell2 a' b›
    by (meson tensor_ell2_add1)
  show ‹tensor_ell2 a (b + b') = tensor_ell2 a b + tensor_ell2 a b'›
    by (simp add: tensor_ell2_add2)  
  show ‹tensor_ell2 (r *⇩C a) b = r *⇩C tensor_ell2 a b›
    by (simp add: tensor_ell2_scaleC1)
  show ‹tensor_ell2 a (r *⇩C b) = r *⇩C tensor_ell2 a b›
    by (simp add: tensor_ell2_scaleC2)
  show ‹∃K. ∀a b. norm (tensor_ell2 a b) ≤ norm a * norm b * K ›
    by (rule exI[of _ 1]) (simp add: norm_tensor_ell2)
qed

lemma ket_pair_split: ‹ket x = tensor_ell2 (ket (fst x)) (ket (snd x))›
  by (simp add: tensor_ell2_ket)



lemma tensor_ell2_is_ortho_set:
  assumes ‹is_ortho_set A› ‹is_ortho_set B›
  shows ‹is_ortho_set {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B}›
  unfolding is_ortho_set_def
proof safe
  fix a a' b b'
  assume ab: "a ∈ A" "a' ∈ A" "b ∈ B" "b' ∈ B" "a ⊗⇩s b ≠ a' ⊗⇩s b'"
  hence "a ≠ a' ∨ b ≠ b'"
    by auto
  hence "is_orthogonal a a' ∨ is_orthogonal b b'"
    using assms is_ortho_setD ab by metis
  thus "is_orthogonal (a ⊗⇩s b) (a' ⊗⇩s b')"
    by auto
next
  fix a b
  assume ab: "a ∈ A" "b ∈ B" "0 = a ⊗⇩s b"
  hence "a ≠ 0" "b ≠ 0"
    using assms unfolding is_ortho_set_def by blast+
  thus False using ab
    using tensor_ell2_nonzero[of a b] by simp
qed

lemma tensor_ell2_dense': ‹ccspan {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B} = ⊤› if ‹ccspan A = ⊤› and ‹ccspan B = ⊤›
proof -
  from that have Adense: ‹closure (cspan A) = UNIV›
    by (transfer' fixing: A) simp
  from that have Bdense: ‹closure (cspan B) = UNIV›
    by (transfer' fixing: B) simp
  show ‹ccspan {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B} = ⊤›
    by (transfer fixing: A B) (use Adense Bdense in ‹rule tensor_ell2_dense›)
qed

lemma tensor_ell2_is_onb:
  assumes ‹is_onb A› ‹is_onb B›
  shows ‹is_onb {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B}›
proof (subst is_onb_def, intro conjI ballI)
  show ‹is_ortho_set {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B}›
    by (rule tensor_ell2_is_ortho_set) (use assms in ‹auto simp: is_onb_def›)
  show ‹ccspan {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B} = ⊤›
    by (rule tensor_ell2_dense') (use ‹is_onb A› ‹is_onb B› in ‹simp_all add: is_onb_def›)
  show ‹ab ∈ {a ⊗⇩s b |a b. a ∈ A ∧ b ∈ B} ⟹ norm ab = 1› for ab
    using ‹is_onb A› ‹is_onb B› by (auto simp: is_onb_def norm_tensor_ell2)
qed

lemma continuous_tensor_ell2: ‹continuous_on UNIV (λ(x::'a ell2, y::'b ell2). x ⊗⇩s y)›
proof -
  have cont: ‹continuous_on UNIV (λt. t ⊗⇩s x)› for x :: ‹'b ell2›
    by (intro linear_continuous_on bounded_clinear.bounded_linear bounded_clinear_tensor_ell22)
  have lip: ‹local_lipschitz (UNIV :: 'a ell2 set) (UNIV :: 'b ell2 set) (⊗⇩s)›
  proof (rule local_lipschitzI)
    fix t :: ‹'a ell2› and x :: ‹'b ell2›
    define u L :: real where ‹u = 1› and ‹L = norm t + u›
    have ‹u > 0›
      by (simp add: u_def)
    have [simp]: ‹L ≥ 0›
      by (simp add: L_def u_def)
    have *: ‹norm s ≤ L› if ‹s∈cball t u› for s :: ‹'a ell2›
      using that unfolding L_def mem_cball by norm
    have ‹L-lipschitz_on (cball x u) ((⊗⇩s) s)› if ‹s∈cball t u› for s :: ‹'a ell2›
      by (rule lipschitz_onI)
         (auto intro!: mult_right_mono *[OF that]
               simp add: dist_norm norm_tensor_ell2 simp flip: tensor_ell2_diff2)
    with ‹u > 0› show ‹∃u>0. ∃L. ∀s∈cball t u ∩ UNIV. L-lipschitz_on (cball x u ∩ UNIV) ((⊗⇩s) s)›
      by force
  qed
  show ?thesis
    by (subst UNIV_Times_UNIV[symmetric]) (use lip cont in ‹rule Lipschitz.continuous_on_TimesI›)
qed

lemma summable_on_tensor_ell2_right: ‹φ summable_on A ⟹ (λx. ψ ⊗⇩s φ x) summable_on A›
  by (rule summable_on_bounded_linear[where h=‹λx. ψ ⊗⇩s x›]) (intro bounded_linear_intros)

lemma summable_on_tensor_ell2_left: ‹φ summable_on A ⟹ (λx. φ x ⊗⇩s ψ) summable_on A›
  by (rule summable_on_bounded_linear[where h=‹λx. x ⊗⇩s ψ›]) (intro bounded_linear_intros)

lift_definition tensor_ell2_left :: ‹'a ell2 ⇒ ('b ell2 ⇒⇩C⇩L ('a×'b) ell2)› is
  ‹λψ φ. ψ ⊗⇩s φ›
  by (simp add: bounded_cbilinear.bounded_clinear_right bounded_cbilinear_tensor_ell2)

lemma tensor_ell2_left_apply[simp]: ‹tensor_ell2_left ψ *⇩V φ = ψ ⊗⇩s φ›
  by (transfer fixing: ψ φ) simp

lift_definition tensor_ell2_right :: ‹'a ell2 ⇒ ('b ell2 ⇒⇩C⇩L ('b×'a) ell2)› is
  ‹λψ φ. φ ⊗⇩s ψ›
  by (simp add: bounded_clinear_tensor_ell22)

lemma tensor_ell2_right_apply[simp]: ‹tensor_ell2_right ψ *⇩V φ = φ ⊗⇩s ψ›
  by (transfer fixing: ψ φ) simp

lemma isometry_tensor_ell2_right: ‹isometry (tensor_ell2_right ψ)› if ‹norm ψ = 1›
  by (rule norm_preserving_isometry) (simp add: norm_tensor_ell2 that)

lemma isometry_tensor_ell2_left: ‹isometry (tensor_ell2_left ψ)› if ‹norm ψ = 1›
  by (rule norm_preserving_isometry) (simp add: norm_tensor_ell2 that)

lemma tensor_ell2_right_scale: ‹tensor_ell2_right (a *⇩C ψ) = a *⇩C tensor_ell2_right ψ›
  by transfer (auto simp: tensor_ell2_scaleC2)
lemma tensor_ell2_left_scale: ‹tensor_ell2_left (a *⇩C ψ) = a *⇩C tensor_ell2_left ψ›
  by transfer (auto simp: tensor_ell2_scaleC1)

lemma tensor_ell2_right_0[simp]: ‹tensor_ell2_right 0 = 0›
  by (auto intro!: cblinfun_eqI)

lemma tensor_ell2_left_0[simp]: ‹tensor_ell2_left 0 = 0›
  by (auto intro!: cblinfun_eqI)

lemma tensor_ell2_right_adj_apply[simp]: ‹(tensor_ell2_right ψ*) *⇩V (α ⊗⇩s β) = (ψ ∙⇩C β) *⇩C α›
  by (rule cinner_extensionality) (simp add: cinner_adj_right)
lemma tensor_ell2_left_adj_apply[simp]: ‹(tensor_ell2_left ψ*) *⇩V (α ⊗⇩s β) = (ψ ∙⇩C α) *⇩C β›
  by (rule cinner_extensionality) (simp add: cinner_adj_right)


lemma infsum_tensor_ell2_right: ‹ψ ⊗⇩s (∑⇩∞x∈A. φ x) = (∑⇩∞x∈A. ψ ⊗⇩s φ x)›
proof -
  consider (summable) ‹φ summable_on A› | (summable') ‹ψ ≠ 0› ‹(λx. ψ ⊗⇩s φ x) summable_on A›
    | (ψ0) ‹ψ = 0›
    | (not_summable) ‹¬ φ summable_on A› ‹¬ (λx. ψ ⊗⇩s φ x) summable_on A›
    by auto
  then show ?thesis
  proof cases
    case summable
    then show ?thesis
      by (rule infsum_bounded_linear[symmetric, unfolded o_def, rotated])
         (intro bounded_linear_intros)
  next
    case summable'
    then have *: ‹(ψ /⇩R (norm ψ)⇧2) ∙⇩C ψ = 1›
      by (simp add: scaleR_scaleC cdot_square_norm)
    from summable'(2) have ‹(λx. (tensor_ell2_left (ψ /⇩R (norm ψ)⇧2))* *⇩V (ψ ⊗⇩s φ x)) summable_on A›
      by (rule summable_on_bounded_linear[unfolded o_def, rotated])
         (intro bounded_linear_intros)
    with * have ‹φ summable_on A›
      by simp
    then show ?thesis
      by (rule infsum_bounded_linear[symmetric, unfolded o_def, rotated])
         (intro bounded_linear_intros)
  next
    case ψ0
    then show ?thesis
      by simp
  next
    case not_summable
    then show ?thesis 
      by (simp add: infsum_not_exists)
  qed
qed

lemma infsum_tensor_ell2_left: ‹(∑⇩∞x∈A. φ x) ⊗⇩s ψ = (∑⇩∞x∈A. φ x ⊗⇩s ψ)›
proof -
  from infsum_tensor_ell2_right
  have ‹swap_ell2 *⇩V (ψ ⊗⇩s (∑⇩∞x∈A. φ x)) = swap_ell2 *⇩V (∑⇩∞x∈A. ψ ⊗⇩s φ x)›
    by metis
  then show ?thesis
    by (simp add: invertible_cblinfun_isometry flip: infsum_cblinfun_apply_invertible)
qed

lemma tensor_ell2_extensionality3:
  assumes "(⋀s t u. a *⇩V (s ⊗⇩s t ⊗⇩s u) = b *⇩V (s ⊗⇩s t ⊗⇩s u))"
  shows "a = b"
  by (rule equal_ket) (use assms in ‹auto simp flip: tensor_ell2_ket›)

lemma cblinfun_cinner_tensor_eqI:
  assumes ‹⋀ψ φ. (ψ ⊗⇩s φ) ∙⇩C (A *⇩V (ψ ⊗⇩s φ)) = (ψ ⊗⇩s φ) ∙⇩C (B *⇩V (ψ ⊗⇩s φ))›
  shows ‹A = B›
proof -
  define C where ‹C = A - B›
  from assms have assmC: ‹(ψ ⊗⇩s φ) ∙⇩C (C *⇩V (ψ ⊗⇩s φ)) = 0› for ψ φ
    by (simp add: C_def cblinfun.diff_left cinner_simps(3))

  have ‹(x ⊗⇩s y) ∙⇩C (C *⇩V (z ⊗⇩s w)) = 0› for x y z w
    
  proof -
    define d e f g h j k l m n p q
      where defs: ‹d = (x ⊗⇩s y) ∙⇩C (C *⇩V z ⊗⇩s w)›
        ‹e = (z ⊗⇩s y) ∙⇩C (C *⇩V x ⊗⇩s y)›
        ‹f = (x ⊗⇩s w) ∙⇩C (C *⇩V x ⊗⇩s y)›
        ‹g = (z ⊗⇩s w) ∙⇩C (C *⇩V x ⊗⇩s y)›
        ‹h = (x ⊗⇩s y) ∙⇩C (C *⇩V z ⊗⇩s y)›
        ‹j = (x ⊗⇩s w) ∙⇩C (C *⇩V z ⊗⇩s y)›
        ‹k = (z ⊗⇩s w) ∙⇩C (C *⇩V z ⊗⇩s y)›
        ‹l = (z ⊗⇩s w) ∙⇩C (C *⇩V x ⊗⇩s w)›
        ‹m = (x ⊗⇩s y) ∙⇩C (C *⇩V x ⊗⇩s w)›
        ‹n = (z ⊗⇩s y) ∙⇩C (C *⇩V x ⊗⇩s w)›
        ‹p = (z ⊗⇩s y) ∙⇩C (C *⇩V z ⊗⇩s w)›
        ‹q = (x ⊗⇩s w) ∙⇩C (C *⇩V z ⊗⇩s w)›

    have constraint: ‹cnj α * e + cnj β * f + cnj β * cnj α * g + α * h + α * cnj β * j +
          α * cnj β * cnj α * k + β * m + β * cnj α * n + β * cnj β * cnj α * l +
          β * α * d + β * α * cnj α * p + β * α * cnj β * q = 0›
      (is ‹?lhs = _›) for α β
    proof -
      from assms 
      have ‹0 = ((x + α *⇩C z) ⊗⇩s (y + β *⇩C w)) ∙⇩C (C *⇩V ((x + α *⇩C z) ⊗⇩s (y + β *⇩C w)))›
        by (simp add: assmC)
      also have ‹… = ?lhs›
        by (simp add: tensor_ell2_add1 tensor_ell2_add2 cinner_add_right cinner_add_left
              cblinfun.add_right tensor_ell2_scaleC1 tensor_ell2_scaleC2 semiring_class.distrib_left
              cblinfun.scaleC_right assmC defs flip: add.assoc mult.assoc)
      finally show ?thesis
        by simp
    qed

    have aux1: ‹a = 0 ⟹ b = 0 ⟹ a + b = 0› for a b :: complex
      by auto
    have aux2: ‹a = 0 ⟹ b = 0 ⟹ a - b = 0› for a b :: complex
      by auto
    have aux4: ‹2 * a = 0 ⟷ a = 0› for a :: complex
      by auto
    have aux5: ‹8 = 2 * 2 * (2::complex)›
      by simp

    from constraint[of 1 0]
    have 1: ‹e + h = 0›
      by simp
    from constraint[of 𝗂 0]
    have 2: ‹h = e›
      by simp
    from 1 2
    have [simp]: ‹e = 0› ‹h = 0›
      by auto
    from constraint[of 0 1]
    have 3: ‹f + m = 0›
      by simp
    from constraint[of 0 𝗂]
    have 4: ‹m = f›
      by simp
    from 3 4
    have [simp]: ‹m = 0› ‹f = 0›
      by auto
    from constraint[of 1 1]
    have 5: ‹g + j + k + n + l + d + p + q = 0›
      by simp
    from constraint[of 1 ‹-1›]
    have 6: ‹- g - j - k - n + l - d - p + q = 0›
      by simp
    from aux1[OF 5 6]
    have 7: ‹l + q = 0›
      by algebra
    from aux2[OF 5 7]
    have 8: ‹g + j + k + n + d + p = 0›
      by (simp add: algebra_simps)
    from constraint[of 1 𝗂]
    have 9: ‹- (𝗂 * g) - 𝗂 * j - 𝗂 * k + 𝗂 * n + l + 𝗂 * d + 𝗂 * p + q = 0›
      by simp
    from constraint[of 1 ‹-𝗂›]
    have 10: ‹𝗂 * g + 𝗂 * j + 𝗂 * k - 𝗂 * n + l - 𝗂 * d - 𝗂 * p + q = 0›
      by simp
    from aux2[OF 9 10]
    have 11: ‹n + d + p - k - j - g = 0›
      using i_squared by algebra
    from aux2[OF 8 11]
    have 12: ‹g + j + k = 0›
      by algebra
    from aux1[OF 8 11]
    have 13: ‹n + d + p = 0›
      by algebra
    from constraint[of 𝗂 1]
    have 14: ‹𝗂 * j - 𝗂 * g + k - 𝗂 * n - 𝗂 * l + 𝗂 * d + p + 𝗂 * q = 0›
      by simp
    from constraint[of 𝗂 ‹-1›]
    have 15: ‹𝗂 * g - 𝗂 * j - k + 𝗂 * n - 𝗂 * l - 𝗂 * d - p + 𝗂 * q = 0›
      by simp
    from aux1[OF 14 15]
    have [simp]: ‹q = l›
      by simp
    from 7
    have [simp]: ‹q = 0› ‹l = 0›
      by auto
    from 14
    have 16: ‹𝗂 * j - 𝗂 * g + k - 𝗂 * n + 𝗂 * d + p = 0›
      by simp
    from constraint[of ‹-𝗂› 1]
    have 17: ‹𝗂 * g - 𝗂 * j + k + 𝗂 * n - 𝗂 * d + p = 0›
      by simp
    from aux1[OF 16 17]
    have [simp]: ‹k = - p›
      by algebra
    from aux2[OF 16 17]
    have 18: ‹j + d - n - g = 0›
      using i_squared by algebra
    from constraint[of ‹-𝗂› 1]
    have 19: ‹𝗂 * g - 𝗂 * j + 𝗂 * n - 𝗂 * d = 0›
      by (simp add: algebra_simps)
    from constraint[of ‹-𝗂› ‹-1›]
    have 20: ‹𝗂 * j - 𝗂 * g - 𝗂 * n + 𝗂 * d = 0›
      by (simp add: algebra_simps)
    from constraint[of 𝗂 𝗂]
    have 21: ‹j - g + n - d + 2 * 𝗂 * p = 0›
      by (simp add: algebra_simps)
    from constraint[of 𝗂 ‹-𝗂›]
    have 22: ‹g - j - n + d - 2 * 𝗂 * p = 0›
      by (simp add: algebra_simps)
    from constraint[of 2 1]
    have 23: ‹g + j + n + d = 0›
      using 12 13 ‹k = -p› by algebra
    from aux2[OF 23 18]
    have [simp]: ‹g = - n›
      by algebra
    from 23
    have [simp]: ‹j = - d›
      by (simp add: add_eq_0_iff2)
    have "8 * (𝗂 * p) + (4 * (𝗂 * d) + 4 * (𝗂 * n)) = 0"
      using constraint[of 2 𝗂] by simp
    hence 24: ‹2 * p + d + n = 0›
      using complex_i_not_zero by algebra
    from aux2[OF 24 13]
    have [simp]: ‹p = 0›
      by simp
    then have [simp]: ‹k = 0›
      by auto
    from 12
    have ‹g = - j›
      by simp
    from 21
    have ‹d = - g›
      by auto

    show ‹d = 0›
      using refl[of d]
      apply (subst (asm) ‹d = - g›)
      apply (subst (asm) ‹g = - j›)
      apply (subst (asm) ‹j = - d›)
      by simp
  qed
  then show ?thesis
    by (auto intro!: equal_ket cinner_ket_eqI
        simp: C_def cblinfun.diff_left cinner_diff_right
        simp flip: tensor_ell2_ket)
qed

lemma unitary_tensor_ell2_right_CARD_1:
  fixes ψ :: ‹'a :: {CARD_1,enum} ell2›
  assumes ‹norm ψ = 1›
  shows ‹unitary (tensor_ell2_right ψ)›
proof (rule unitaryI)
  show ‹tensor_ell2_right ψ* o⇩C⇩L tensor_ell2_right ψ = id_cblinfun›
    by (simp add: assms isometry_tensor_ell2_right)
  have *: ‹(ψ ∙⇩C φ) * (φ ∙⇩C ψ) = φ ∙⇩C φ› for φ
  proof -
    define ψ' φ' where ‹ψ' = 1 ∙⇩C ψ› and ‹φ' = 1 ∙⇩C φ›
    have ψ: ‹ψ = ψ' *⇩C 1›
      by (metis ψ'_def one_cinner_a_scaleC_one)
  have φ: ‹φ = φ' *⇩C 1›
      by (metis φ'_def one_cinner_a_scaleC_one)
    show ?thesis
      unfolding ψ φ
      by (metis (no_types, lifting) Groups.mult_ac(1) ψ assms cinner_simps(5) cinner_simps(6)
             norm_one of_complex_def of_complex_inner_1 power2_norm_eq_cinner)
  qed
  show ‹tensor_ell2_right ψ o⇩C⇩L tensor_ell2_right ψ* = id_cblinfun›
    by (rule cblinfun_cinner_tensor_eqI) (simp add: *)
qed



subsection ‹Tensor product of operators on \<^typ>‹_ ell2››

definition tensor_op :: ‹('a ell2, 'b ell2) cblinfun ⇒ ('c ell2, 'd ell2) cblinfun
      ⇒ (('a×'c) ell2, ('b×'d) ell2) cblinfun› (infixr "⊗⇩o" 70) where
  ‹tensor_op M N = cblinfun_extension (range ket) (λk. case (inv ket k) of (x,y) ⇒ tensor_ell2 (M *⇩V ket x) (N *⇩V ket y))›

lemma  
  ― ‹Loosely following \<^cite>‹‹Section IV.1› in takesaki››
  fixes a :: ‹'a› and b :: ‹'b› and c :: ‹'c› and d :: ‹'d› and M :: ‹'a ell2 ⇒⇩C⇩L 'b ell2› and N :: ‹'c ell2 ⇒⇩C⇩L 'd ell2›
  shows tensor_op_ell2: ‹(M ⊗⇩o N) *⇩V (ψ ⊗⇩s φ) = (M *⇩V ψ) ⊗⇩s (N *⇩V φ)›
  and tensor_op_norm: ‹norm (M ⊗⇩o N) = norm M * norm N›
proof -
  define S1 :: ‹('a×'d) ell2 set› and f1 g1 extg1 
    where ‹S1 = range ket› 
      and ‹f1 k = (case (inv ket k) of (x,y) ⇒ tensor_ell2 (M *⇩V ket x) (ket y))›
      and ‹g1 = cconstruct S1 f1› and ‹extg1 = cblinfun_extension (cspan S1) g1›
    for k
  define S2 :: ‹('a×'c) ell2 set› and f2 g2 extg2
    where ‹S2 = range ket› 
      and ‹f2 k = (case (inv ket k) of (x,y) ⇒ tensor_ell2 (ket x) (N *⇩V ket y))›
      and ‹g2 = cconstruct S2 f2› and ‹extg2 = cblinfun_extension (cspan S2) g2›
    for k
  define tensorMN where ‹tensorMN = extg1 o⇩C⇩L extg2›

  have extg1_ket: ‹extg1 *⇩V ket (x,y) = (M *⇩V ket x) ⊗⇩s ket y›
    and norm_extg1: ‹norm extg1 ≤ norm M› for x y
  proof -
    have [simp]: ‹cindependent S1›
      using S1_def cindependent_ket by blast
    have [simp]: ‹closure (cspan S1) = UNIV›
      by (simp add: S1_def)
    have [simp]: ‹ket (x, y) ∈ cspan S1› for x y
      by (simp add: S1_def complex_vector.span_base)
    have g1_f1: ‹g1 (ket (x,y)) = f1 (ket (x,y))› for x y
      by (metis S1_def ‹cindependent S1› complex_vector.construct_basis g1_def rangeI)
    have [simp]: ‹clinear g1›
      unfolding g1_def using ‹cindependent S1› by (rule complex_vector.linear_construct)
    then have g1_add: ‹g1 (x + y) = g1 x + g1 y› if ‹x ∈ cspan S1› and ‹y ∈ cspan S1› for x y
      using clinear_iff by blast
    from ‹clinear g1› have g1_scale: ‹g1 (c *⇩C x) = c *⇩C g1 x› if ‹x ∈ cspan S1› for x c
      by (simp add: complex_vector.linear_scale)

    have g1_bounded: ‹norm (g1 ψ) ≤ norm M * norm ψ› if ‹ψ ∈ cspan S1› for ψ
    proof -
      from that obtain t r where ‹finite t› and ‹t ⊆ range ket› and ψ_tr: ‹ψ = (∑a∈t. r a *⇩C a)›
        by (smt (verit) complex_vector.span_explicit mem_Collect_eq S1_def)
      define X Y where ‹X = fst ` inv ket ` t› and ‹Y = snd ` inv ket ` t›
      have g1_ket: ‹g1 (ket (x,y)) = (M *⇩V ket x) ⊗⇩s ket y› for x y
        by (simp add: g1_def S1_def complex_vector.construct_basis f1_def)
      define ξ where ‹ξ y = (∑x∈X. if (ket (x,y) ∈ t) then r (ket (x,y)) *⇩C ket x else 0)› for y
      have ψξ: ‹ψ = (∑y∈Y. ξ y ⊗⇩s ket y)›
      proof -
        have ‹(∑y∈Y. ξ y ⊗⇩s ket y) = (∑xy∈X × Y. if ket xy ∈ t then r (ket xy) *⇩C ket xy else 0)›
          unfolding ξ_def tensor_ell2_sum_left
          by (subst sum.swap)
             (auto simp: sum.cartesian_product tensor_ell2_scaleC1 tensor_ell2_ket intro!: sum.cong)
        also have ‹… = (∑xy∈ket ` (X × Y). if xy ∈ t then r xy *⇩C xy else 0)›
          by (subst sum.reindex) (auto simp add: inj_on_def)
        also have ‹… = ψ›
          unfolding ψ_tr
        proof (rule sum.mono_neutral_cong_right, goal_cases)
          case 2
          show "t ⊆ ket ` (X × Y)"
          proof
            fix x assume "x ∈ t"
            with ‹t ⊆ range ket› obtain a b where ab: "x = ket (a, b)"
              by fast
            also have "ket (a, b) ∈ ket ` (X × Y)"
              by (metis X_def Y_def ‹x ∈ t› ab f_inv_into_f fst_conv image_eqI
                        ket_injective mem_Sigma_iff rangeI snd_conv)
            finally show "x ∈ ket ` (X × Y)" .
          qed
        qed (auto simp add: X_def Y_def ‹finite t›)
        finally show ?thesis
          by simp
      qed
      have ‹(norm (g1 ψ))⇧2 = (norm (∑y∈Y. (M *⇩V ξ y) ⊗⇩s ket y))⇧2›
        by (auto simp: ψξ complex_vector.linear_sum ξ_def tensor_ell2_sum_left 
            complex_vector.linear_scale g1_ket tensor_ell2_scaleC1
            complex_vector.linear_0 tensor_ell2_ket
            intro!: sum.cong arg_cong[where f=norm])
      also have ‹… = (∑y∈Y. (norm ((M *⇩V ξ y) ⊗⇩s ket y))⇧2)›
        unfolding Y_def by (rule pythagorean_theorem_sum) (use ‹finite t› in auto)
      also have ‹… = (∑y∈Y. (norm (M *⇩V ξ y))⇧2)›
        by (simp add: norm_tensor_ell2)
      also have ‹… ≤ (∑y∈Y. (norm M * norm (ξ y))⇧2)›
        by (meson norm_cblinfun norm_ge_zero power_mono sum_mono)
      also have ‹… = (norm M)⇧2 * (∑y∈Y. (norm (ξ y ⊗⇩s ket y))⇧2)›
        by (simp add: power_mult_distrib norm_tensor_ell2 flip: sum_distrib_left)
      also have ‹… = (norm M)⇧2 * (norm (∑y∈Y. ξ y ⊗⇩s ket y))⇧2›
        unfolding Y_def
        by (subst pythagorean_theorem_sum) (use ‹finite t› in auto)
      also have ‹… = (norm M)⇧2 * (norm ψ)⇧2›
        using ψξ by fastforce
      finally show ‹norm (g1 ψ) ≤ norm M * norm ψ›
        by (metis mult_nonneg_nonneg norm_ge_zero power2_le_imp_le power_mult_distrib)
    qed

    have extg1_exists: ‹cblinfun_extension_exists (cspan S1) g1›
      by (rule cblinfun_extension_exists_bounded_dense[where B=‹norm M›])
         (use g1_add g1_scale g1_bounded in auto)

    then show ‹extg1 *⇩V ket (x,y) = (M *⇩V ket x) ⊗⇩s ket y› for x y
      by (simp add: extg1_def cblinfun_extension_apply g1_f1 f1_def)

    from g1_add g1_scale g1_bounded
    show ‹norm extg1 ≤ norm M›
      by (auto simp: extg1_def intro!: cblinfun_extension_norm_bounded_dense)
  qed

  have extg1_apply: ‹extg1 *⇩V (ψ ⊗⇩s φ) = (M *⇩V ψ) ⊗⇩s φ› for ψ φ
  proof -
    have 1: ‹bounded_clinear (λa. extg1 *⇩V (a ⊗⇩s ket y))› for y
      by (intro bounded_clinear_cblinfun_apply bounded_clinear_tensor_ell22)
    have 2: ‹bounded_clinear (λa. (M *⇩V a) ⊗⇩s ket y)› for y :: 'd
      by (auto intro!: bounded_clinear_tensor_ell22[THEN bounded_clinear_compose] bounded_clinear_cblinfun_apply)
    have 3: ‹bounded_clinear (λa. extg1 *⇩V (ψ ⊗⇩s a))›
      by (intro bounded_clinear_cblinfun_apply bounded_clinear_tensor_ell21)
    have 4: ‹bounded_clinear ((⊗⇩s) (M *⇩V ψ))›
      by (auto intro!: bounded_clinear_tensor_ell21[THEN bounded_clinear_compose] bounded_clinear_cblinfun_apply)

    have eq_ket: ‹extg1 *⇩V tensor_ell2 ψ (ket y) = tensor_ell2 (M *⇩V ψ) (ket y)› for y
      by (rule bounded_clinear_eq_on_closure[where t=ψ and G=‹range ket›])
         (use 1 2 extg1_ket in ‹auto simp: tensor_ell2_ket›)
    show ?thesis 
      by (rule bounded_clinear_eq_on_closure[where t=φ and G=‹range ket›])
         (use 3 4 eq_ket in auto)
  qed

  have extg2_ket: ‹extg2 *⇩V ket (x,y) = ket x ⊗⇩s (N *⇩V ket y)›
    and norm_extg2: ‹norm extg2 ≤ norm N› for x y
  proof -
    have [simp]: ‹cindependent S2›
      using S2_def cindependent_ket by blast
    have [simp]: ‹closure (cspan S2) = UNIV›
      by (simp add: S2_def)
    have [simp]: ‹ket (x, y) ∈ cspan S2› for x y
      by (simp add: S2_def complex_vector.span_base)
    have g2_f2: ‹g2 (ket (x,y)) = f2 (ket (x,y))› for x y
      by (metis S2_def ‹cindependent S2› complex_vector.construct_basis g2_def rangeI)
    have [simp]: ‹clinear g2›
      unfolding g2_def using ‹cindependent S2› by (rule complex_vector.linear_construct)
    then have g2_add: ‹g2 (x + y) = g2 x + g2 y› if ‹x ∈ cspan S2› and ‹y ∈ cspan S2› for x y
      using clinear_iff by blast
    from ‹clinear g2› have g2_scale: ‹g2 (c *⇩C x) = c *⇩C g2 x› if ‹x ∈ cspan S2› for x c
      by (simp add: complex_vector.linear_scale)

    have g2_bounded: ‹norm (g2 ψ) ≤ norm N * norm ψ› if ‹ψ ∈ cspan S2› for ψ
    proof -
      from that obtain t r where ‹finite t› and ‹t ⊆ range ket› and ψ_tr: ‹ψ = (∑a∈t. r a *⇩C a)›
        by (smt (verit) complex_vector.span_explicit mem_Collect_eq S2_def)
      define X Y where ‹X = fst ` inv ket ` t› and ‹Y = snd ` inv ket ` t›
      have g2_ket: ‹g2 (ket (x,y)) = ket x ⊗⇩s (N *⇩V ket y)› for x y
        by (auto simp add: f2_def complex_vector.construct_basis g2_def S2_def)
      define ξ where ‹ξ x = (∑y∈Y. if (ket (x,y) ∈ t) then r (ket (x,y)) *⇩C ket y else 0)› for x
      have ψξ: ‹ψ = (∑x∈X. ket x ⊗⇩s ξ x)›
      proof -
        have ‹(∑x∈X. ket x ⊗⇩s ξ x) = (∑xy∈X × Y. if ket xy ∈ t then r (ket xy) *⇩C ket xy else 0)›
          by (auto simp: ξ_def tensor_ell2_sum_right sum.cartesian_product tensor_ell2_scaleC2 tensor_ell2_ket intro!: sum.cong)
        also have ‹… = (∑xy∈ket ` (X × Y). if xy ∈ t then r xy *⇩C xy else 0)›
          by (subst sum.reindex) (auto simp add: inj_on_def)
        also have ‹… = ψ›
          unfolding ψ_tr
        proof (rule sum.mono_neutral_cong_right, goal_cases)
          case 2
          show "t ⊆ ket ` (X × Y)"
          proof
            fix x assume "x ∈ t"
            with ‹t ⊆ range ket› obtain a b where ab: "x = ket (a, b)"
              by fast
            also have "ket (a, b) ∈ ket ` (X × Y)"
              by (metis X_def Y_def ‹x ∈ t› ab f_inv_into_f fst_conv image_eqI
                        ket_injective mem_Sigma_iff rangeI snd_conv)
            finally show "x ∈ ket ` (X × Y)" .
          qed
        qed (auto simp add: X_def Y_def ‹finite t›)
        finally show ?thesis
          by simp
      qed
      have ‹(norm (g2 ψ))⇧2 = (norm (∑x∈X. ket x ⊗⇩s (N *⇩V ξ x)))⇧2›
        by (auto simp: ψξ complex_vector.linear_sum ξ_def tensor_ell2_sum_right
            complex_vector.linear_scale g2_ket tensor_ell2_scaleC2
            complex_vector.linear_0 tensor_ell2_ket
            intro!: sum.cong arg_cong[where f=norm])
      also have ‹… = (∑x∈X. (norm (ket x ⊗⇩s (N *⇩V ξ x)))⇧2)›
        unfolding X_def by (rule pythagorean_theorem_sum) (use ‹finite t› in auto)
      also have ‹… = (∑x∈X. (norm (N *⇩V ξ x))⇧2)›
        by (simp add: norm_tensor_ell2)
      also have ‹… ≤ (∑x∈X. (norm N * norm (ξ x))⇧2)›
        by (meson norm_cblinfun norm_ge_zero power_mono sum_mono)
      also have ‹… = (norm N)⇧2 * (∑x∈X. (norm (ket x ⊗⇩s ξ x))⇧2)›
        by (simp add: power_mult_distrib norm_tensor_ell2 flip: sum_distrib_left)
      also have ‹… = (norm N)⇧2 * (norm (∑x∈X. ket x ⊗⇩s ξ x))⇧2›
        unfolding X_def by (subst pythagorean_theorem_sum) (use ‹finite t› in auto)
      also have ‹… = (norm N)⇧2 * (norm ψ)⇧2›
        using ψξ by fastforce
      finally show ‹norm (g2 ψ) ≤ norm N * norm ψ›
        by (metis mult_nonneg_nonneg norm_ge_zero power2_le_imp_le power_mult_distrib)
    qed

    have extg2_exists: ‹cblinfun_extension_exists (cspan S2) g2›
      by (rule cblinfun_extension_exists_bounded_dense[where B=‹norm N›])
         (use g2_add g2_scale g2_bounded in auto)

    then show ‹extg2 *⇩V ket (x,y) = ket x ⊗⇩s N *⇩V ket y› for x y
      by (simp add: extg2_def cblinfun_extension_apply g2_f2 f2_def)

    from g2_add g2_scale g2_bounded
    show ‹norm extg2 ≤ norm N›
      by (auto simp: extg2_def intro!: cblinfun_extension_norm_bounded_dense)
  qed

  have extg2_apply: ‹extg2 *⇩V (ψ ⊗⇩s φ) = ψ ⊗⇩s (N *⇩V φ)› for ψ φ
  proof -
    have 1: ‹bounded_clinear (λa. extg2 *⇩V (ket x ⊗⇩s a))› for x
      by (intro bounded_clinear_cblinfun_apply bounded_clinear_tensor_ell21)
    have 2: ‹bounded_clinear (λa. ket x ⊗⇩s (N *⇩V a))› for x :: 'a
      by (auto intro!: bounded_clinear_tensor_ell21[THEN bounded_clinear_compose] bounded_clinear_cblinfun_apply)
    have 3: ‹bounded_clinear (λa. extg2 *⇩V (a ⊗⇩s φ))›
      by (intro bounded_clinear_cblinfun_apply bounded_clinear_tensor_ell22)
    have 4: ‹ bounded_clinear (λa. a ⊗⇩s (N *⇩V φ))›
      by (auto intro!: bounded_clinear_tensor_ell22[THEN bounded_clinear_compose] bounded_clinear_cblinfun_apply)

    have eq_ket: ‹extg2 *⇩V (ket x ⊗⇩s φ) = ket x ⊗⇩s (N *⇩V φ)› for x
      by (rule bounded_clinear_eq_on_closure[where t=φ and G=‹range ket›])
         (use 1 2 extg2_ket in ‹auto simp: tensor_ell2_ket›)
    show ?thesis 
      by (rule bounded_clinear_eq_on_closure[where t=ψ and G=‹range ket›])
         (use 3 4 eq_ket in auto)
  qed

  have tensorMN_apply: ‹tensorMN *⇩V (ψ ⊗⇩s φ) = (M *⇩V ψ) ⊗⇩s (N *⇩V φ)› for ψ φ
    by (simp add: extg1_apply extg2_apply tensorMN_def)

  have ‹cblinfun_extension_exists (range ket) (λk. case inv ket k of (x, y) ⇒ (M *⇩V ket x) ⊗⇩s (N *⇩V ket y))›
    by (rule cblinfun_extension_existsI[where B=tensorMN])
       (use tensorMN_apply[of ‹ket _› ‹ket _›] in ‹auto simp: tensor_ell2_ket›)

  then have otimes_ket: ‹(M ⊗⇩o N) *⇩V (ket (a,c)) = (M *⇩V ket a) ⊗⇩s (N *⇩V ket c)› for a c
    by (simp add: tensor_op_def cblinfun_extension_apply)

  have tensorMN_otimes: ‹M ⊗⇩o N = tensorMN›
    by (rule equal_ket)
       (use tensorMN_apply[of ‹ket _› ‹ket _›] in ‹auto simp: otimes_ket tensor_ell2_ket›)

  show otimes_apply: ‹(M ⊗⇩o N) *⇩V (ψ ⊗⇩s φ) = (M *⇩V ψ) ⊗⇩s (N *⇩V φ)› for ψ φ
    by (simp add: tensorMN_apply tensorMN_otimes)

  show ‹norm (M ⊗⇩o N) = norm M * norm N›
  proof (rule order.antisym)
    show ‹norm (M ⊗⇩o N) ≤ norm M * norm N›
      unfolding tensorMN_otimes tensorMN_def
      by (smt (verit, best) mult_mono norm_cblinfun_compose norm_extg1 norm_extg2 norm_ge_zero)
    have ‹norm (M ⊗⇩o N) ≥ norm M * norm N * ε› if ‹ε < 1› and ‹ε > 0› for ε
    proof -
      obtain ψa where 1: ‹norm (M *⇩V ψa) ≥ norm M * sqrt ε› and ‹norm ψa = 1›
        by (atomize_elim, rule cblinfun_norm_approx_witness_mult[where ε=‹sqrt ε› and A=M])
           (use ‹ε < 1› in auto)
      obtain ψb where 2: ‹norm (N *⇩V ψb) ≥ norm N * sqrt ε› and ‹norm ψb = 1›
        by (atomize_elim, rule cblinfun_norm_approx_witness_mult[where ε=‹sqrt ε› and A=N])
           (use ‹ε < 1› in auto)
      have ‹norm ((M ⊗⇩o N) *⇩V (ψa ⊗⇩s ψb)) / norm (ψa ⊗⇩s ψb) = norm ((M ⊗⇩o N) *⇩V (ψa ⊗⇩s ψb))›
        using ‹norm ψa = 1› ‹norm ψb = 1›
        by (simp add: norm_tensor_ell2) 
      also have ‹… = norm (M *⇩V ψa) * norm (N *⇩V ψb)›
        by (simp add: norm_tensor_ell2 otimes_apply)
      also from 1 2 have ‹… ≥ (norm M * sqrt ε) * (norm N * sqrt ε)› (is ‹_ ≥ …›)
        by (rule mult_mono') (use ‹ε > 0› in auto)
      also have ‹… = norm M * norm N * ε›
        using ‹ε > 0› by force
      finally show ?thesis
        using cblinfun_norm_geqI by blast
    qed
    then show ‹norm (M ⊗⇩o N) ≥ norm M * norm N›
      by (metis field_le_mult_one_interval mult.commute)
  qed
qed

lemma tensor_op_ket: ‹tensor_op M N *⇩V (ket (a,c)) = tensor_ell2 (M *⇩V ket a) (N *⇩V ket c)›
  by (metis tensor_ell2_ket tensor_op_ell2)

lemma comp_tensor_op: "(tensor_op a b) o⇩C⇩L (tensor_op c d) = tensor_op (a o⇩C⇩L c) (b o⇩C⇩L d)"
  for a :: "'e ell2 ⇒⇩C⇩L 'c ell2" and b :: "'f ell2 ⇒⇩C⇩L 'd ell2" and
      c :: "'a ell2 ⇒⇩C⇩L 'e ell2" and d :: "'b ell2 ⇒⇩C⇩L 'f ell2"
  by (rule equal_ket) (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma tensor_op_left_add: ‹(x + y) ⊗⇩o b = x ⊗⇩o b + y ⊗⇩o b›
  for x y :: ‹'a ell2 ⇒⇩C⇩L 'c ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
  by (auto intro!: equal_ket simp: tensor_op_ket plus_cblinfun.rep_eq tensor_ell2_add1)

lemma tensor_op_right_add: ‹b ⊗⇩o (x + y) = b ⊗⇩o x + b ⊗⇩o y›
  for x y :: ‹'a ell2 ⇒⇩C⇩L 'c ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
  by (auto intro!: equal_ket simp: tensor_op_ket plus_cblinfun.rep_eq tensor_ell2_add2)

lemma tensor_op_scaleC_left: ‹(c *⇩C x) ⊗⇩o b = c *⇩C (x ⊗⇩o b)›
  for x :: ‹'a ell2 ⇒⇩C⇩L 'c ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
  by (auto intro!: equal_ket simp: tensor_op_ket tensor_ell2_scaleC1)

lemma tensor_op_scaleC_right: ‹b ⊗⇩o (c *⇩C x) = c *⇩C (b ⊗⇩o x)›
  for x :: ‹'a ell2 ⇒⇩C⇩L 'c ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
  by (auto intro!: equal_ket simp: tensor_op_ket tensor_ell2_scaleC2)

lemma tensor_op_bounded_cbilinear[simp]: ‹bounded_cbilinear tensor_op›
  by (auto intro!: bounded_cbilinear.intro exI[of _ 1]
      simp: tensor_op_left_add tensor_op_right_add tensor_op_scaleC_left tensor_op_scaleC_right tensor_op_norm)

lemma tensor_op_cbilinear[simp]: ‹cbilinear tensor_op›
  by (simp add: bounded_cbilinear.add_left bounded_cbilinear.add_right cbilinear_def clinearI tensor_op_scaleC_left tensor_op_scaleC_right)

lemma tensor_butter: ‹butterfly (ket i) (ket j) ⊗⇩o butterfly (ket k) (ket l) = butterfly (ket (i,k)) (ket (j,l))›
  by (rule equal_ket)
     (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2 butterfly_def tensor_ell2_scaleC1 tensor_ell2_scaleC2)

lemma cspan_tensor_op_butter: ‹cspan {tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))| (i::_::finite) (j::_::finite) (k::_::finite) (l::_::finite). True} = UNIV›
  unfolding tensor_butter
  by (subst cspan_butterfly_ket[symmetric]) (metis surj_pair)

lemma cindependent_tensor_op_butter: ‹cindependent {tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))| i j k l. True}›
  unfolding tensor_butter
  using cindependent_butterfly_ket
  by (smt (z3) Collect_mono_iff complex_vector.independent_mono)

lift_definition right_amplification :: ‹('a ell2 ⇒⇩C⇩L 'b ell2) ⇒⇩C⇩L (('a×'c) ell2 ⇒⇩C⇩L ('b×'c) ell2)› is
  ‹λa. a ⊗⇩o id_cblinfun›
  by (simp add: bounded_cbilinear.bounded_clinear_left)

lift_definition left_amplification :: ‹('a ell2 ⇒⇩C⇩L 'b ell2) ⇒⇩C⇩L (('c×'a) ell2 ⇒⇩C⇩L ('c×'b) ell2)› is
  ‹λa. id_cblinfun ⊗⇩o a›
  by (simp add: bounded_cbilinear.bounded_clinear_right)



lemma sandwich_tensor_ell2_right: ‹sandwich (tensor_ell2_right ψ*) *⇩V a ⊗⇩o b = (ψ ∙⇩C (b *⇩V ψ)) *⇩C a›
  by (rule cblinfun_eqI) (simp add: sandwich_apply tensor_op_ell2)
lemma sandwich_tensor_ell2_left: ‹sandwich (tensor_ell2_left ψ*) *⇩V a ⊗⇩o b = (ψ ∙⇩C (a *⇩V ψ)) *⇩C b›
  by (rule cblinfun_eqI) (simp add: sandwich_apply tensor_op_ell2)

lemma tensor_op_adjoint: ‹(tensor_op a b)* = tensor_op (a*) (b*)›
  by (rule cinner_ket_adjointI[symmetric])
     (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2 cinner_adj_left)

lemma has_sum_id_tensor_butterfly_ket: ‹((λi. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ) has_sum ψ) UNIV›
proof -
  have *: ‹(∑i∈F. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ) = trunc_ell2 (UNIV × F) ψ› if ‹finite F› for F
  proof (rule Rep_ell2_inject[THEN iffD1], rule ext, rename_tac xy)
    fix xy :: ‹'b × 'a›
    obtain x y where xy: ‹xy = (x,y)›
      by fastforce
    have ‹Rep_ell2 (∑i∈F. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ) xy
       = ket xy ∙⇩C (∑i∈F. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ)›
      by (simp add: cinner_ket_left)
    also have ‹... = (∑i∈F. ket xy ∙⇩C ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ))›
      using cinner_sum_right by blast
    also have ‹… = (∑i∈F. ket xy ∙⇩C ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i))* *⇩V ψ))›
      by (simp add: tensor_op_adjoint)
    also have ‹… = (∑i∈F. ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ket xy) ∙⇩C ψ)›
      by (meson cinner_adj_right)
    also have ‹… = of_bool (y∈F) * (ket xy ∙⇩C ψ)›
      by (subst sum_single[where i=y])
         (auto simp: xy tensor_op_ell2 cinner_ket that simp flip: tensor_ell2_ket)
    also have ‹… = of_bool (y∈F) * (Rep_ell2 ψ xy)›
      by (simp add: cinner_ket_left)
    also have ‹… = Rep_ell2 (trunc_ell2 (UNIV × F) ψ) xy›
      by (simp add: trunc_ell2.rep_eq xy)
    finally show ‹Rep_ell2 (∑i∈F. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ) xy = …›
      by -
  qed

  have ‹((λF. trunc_ell2 F ψ) ⤏ trunc_ell2 UNIV ψ) (filtermap ((×)UNIV) (finite_subsets_at_top UNIV))›
    by (rule trunc_ell2_lim_general)
       (auto simp add: filterlim_def le_filter_def eventually_finite_subsets_at_top
          eventually_filtermap intro!: exI[where x=‹snd ` _›])
  then have ‹((λF. trunc_ell2 (UNIV×F) ψ) ⤏ ψ) (finite_subsets_at_top UNIV)›
    by (simp add: filterlim_def filtermap_filtermap)
  then have ‹((λF. (∑i∈F. (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) *⇩V ψ)) ⤏ ψ) (finite_subsets_at_top UNIV)›
    by (rule Lim_transform_eventually)
       (simp add: * eventually_finite_subsets_at_top_weakI)
  then show ?thesis
    by (simp add: has_sum_def)
qed


lemma tensor_op_dense: ‹cstrong_operator_topology closure_of (cspan {a ⊗⇩o b | a b. True}) = UNIV›
  ― ‹\<^cite>‹‹p.185 (10)› in takesaki›, but we prove it directly.›
proof (intro order.antisym subset_UNIV subsetI)
  fix c :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('c × 'd) ell2›
  define c' where ‹c' i j = (tensor_ell2_right (ket i))* o⇩C⇩L c o⇩C⇩L tensor_ell2_right (ket j)› for i j
  define AB :: ‹(('a × 'b) ell2 ⇒⇩C⇩L ('c × 'd) ell2) set› where
    ‹AB = cstrong_operator_topology closure_of (cspan {a ⊗⇩o b | a b. True})›

  have [simp]: ‹closedin cstrong_operator_topology AB›
    by (simp add: AB_def)
  have [simp]: ‹csubspace AB›
    using AB_def sot_closure_is_csubspace' by blast

  have *: ‹c' i j ⊗⇩o butterfly (ket i) (ket j) = (id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) o⇩C⇩L c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j))› for i j
  proof (rule equal_ket, rule cinner_ket_eqI, rename_tac a b)
    fix a :: ‹'a × 'b› and b :: ‹'c × 'd›
    obtain bi bj ai aj where b: ‹b = (bi,bj)› and a: ‹a = (ai,aj)›
      by (meson surj_pair)
    have ‹ket b ∙⇩C ((c' i j ⊗⇩o butterfly (ket i) (ket j)) *⇩V ket a) = of_bool (j = aj ∧ bj = i) * ((ket bi ⊗⇩s ket i) ∙⇩C (c *⇩V ket ai ⊗⇩s ket aj))›
      by (auto simp add: a b tensor_op_ell2 cinner_ket c'_def cinner_adj_right
          simp flip: tensor_ell2_ket)
    also have ‹… = ket b ∙⇩C ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i) o⇩C⇩L c o⇩C⇩L id_cblinfun ⊗⇩o butterfly (ket j) (ket j)) *⇩V ket a)›
      apply (subst asm_rl[of ‹id_cblinfun ⊗⇩o butterfly (ket i) (ket i) = (id_cblinfun ⊗⇩o butterfly (ket i) (ket i))*›])
      subgoal
        by (simp add: tensor_op_adjoint)
      subgoal
        by (auto simp: a b tensor_op_ell2 cinner_adj_right cinner_ket
            simp flip: tensor_ell2_ket)
      done
    finally show ‹ket b ∙⇩C ((c' i j ⊗⇩o butterfly (ket i) (ket j)) *⇩V ket a) =
           ket b ∙⇩C ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i) o⇩C⇩L c o⇩C⇩L id_cblinfun ⊗⇩o butterfly (ket j) (ket j)) *⇩V ket a)›
      by -
  qed

  have ‹c' i j ⊗⇩o butterfly (ket i) (ket j) ∈ AB› for i j
  proof -
    have ‹c' i j ⊗⇩o butterfly (ket i) (ket j) ∈ {a ⊗⇩o b | a b. True}›
      by auto
    also have ‹… ⊆ cspan …›
      by (simp add: complex_vector.span_superset)
    also have ‹… ⊆ cstrong_operator_topology closure_of …›
      by (rule closure_of_subset) simp
    also have ‹… = AB›
      by (simp add: AB_def)
    finally show ?thesis
      by simp
  qed
  with * have AB1: ‹(id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) o⇩C⇩L c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j)) ∈ AB› for i j
    by simp
  have ‹((λi. ((id_cblinfun ⊗⇩o butterfly (ket i) (ket i)) o⇩C⇩L c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j))) *⇩V ψ)
            has_sum (c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j))) *⇩V ψ) UNIV› for j ψ
    by (simp add: has_sum_id_tensor_butterfly_ket)
  then have AB2: ‹(c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j))) ∈ AB› for j
    by (rule has_sum_closed_cstrong_operator_topology[rotated -1]) (use AB1 in auto)

  have ‹((λj. (c o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket j) (ket j))) *⇩V ψ) has_sum c *⇩V ψ) UNIV› for ψ
    by (simp add: has_sum_cblinfun_apply has_sum_id_tensor_butterfly_ket)
  then show AB3: ‹c ∈ AB›
    by (rule has_sum_closed_cstrong_operator_topology[rotated -1]) (use AB2 in auto)
qed


lemma tensor_extensionality_finite:
  fixes F G :: ‹((('a::finite × 'b::finite) ell2) ⇒⇩C⇩L (('c::finite × 'd::finite) ell2)) ⇒ 'e::complex_vector›
  assumes [simp]: "clinear F" "clinear G"
  assumes tensor_eq: "(⋀a b. F (tensor_op a b) = G (tensor_op a b))"
  shows "F = G"
proof (rule ext, rule complex_vector.linear_eq_on_span[where f=F and g=G])
  show ‹clinear F› and ‹clinear G›
    using assms by (simp_all add: cbilinear_def)
  show ‹x ∈ cspan  {tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))| i j k l. True}› 
    for x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('c × 'd) ell2›
    using cspan_tensor_op_butter by auto
  show ‹F x = G x› if ‹x ∈ {tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)) |i j k l. True}› for x
    using that by (auto simp: tensor_eq)
qed

lemma tensor_id[simp]: ‹tensor_op id_cblinfun id_cblinfun = id_cblinfun›
  by (rule equal_ket) (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma tensor_butterfly: "tensor_op (butterfly ψ ψ') (butterfly φ φ') = butterfly (tensor_ell2 ψ φ) (tensor_ell2 ψ' φ')"
  by (rule equal_ket)
     (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2 butterfly_def tensor_ell2_scaleC1 tensor_ell2_scaleC2)

definition tensor_lift :: ‹(('a1::finite ell2 ⇒⇩C⇩L 'a2::finite ell2) ⇒ ('b1::finite ell2 ⇒⇩C⇩L 'b2::finite ell2) ⇒ 'c)
                        ⇒ ((('a1×'b1) ell2 ⇒⇩C⇩L ('a2×'b2) ell2) ⇒ 'c::complex_normed_vector)› where
  "tensor_lift F2 = (SOME G. clinear G ∧ (∀a b. G (tensor_op a b) = F2 a b))"

lemma 
  fixes F2 :: "'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2
            ⇒ 'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2
            ⇒ 'e::complex_normed_vector"
  assumes "cbilinear F2"
  shows tensor_lift_clinear: "clinear (tensor_lift F2)"
    and tensor_lift_correct:  ‹(λa b. tensor_lift F2 (a ⊗⇩o b)) = F2›
proof -
  define F2' t4 φ where
    ‹F2' = tensor_lift F2› and
    ‹t4 = (λ(i,j,k,l). tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)))› and
    ‹φ m = (let (i,j,k,l) = inv t4 m in F2 (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)))› for m
  have t4inj: "x = y" if "t4 x = t4 y" for x y
  proof (rule ccontr)
    obtain i  j  k  l  where x: "x = (i,j,k,l)" by (meson prod_cases4) 
    obtain i' j' k' l' where y: "y = (i',j',k',l')" by (meson prod_cases4) 
    have 1: "bra (i,k) *⇩V t4 x *⇩V ket (j,l) = 1"
      by (auto simp: t4_def x tensor_op_ell2 butterfly_def cinner_ket simp flip: tensor_ell2_ket)
    assume ‹x ≠ y›
    then have 2: "bra (i,k) *⇩V t4 y *⇩V ket (j,l) = 0"
      by (auto simp: t4_def x y tensor_op_ell2 butterfly_def cinner_ket
               simp flip: tensor_ell2_ket)
    from 1 2 that
    show False
      by auto
  qed
  have ‹φ (tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))) = F2 (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))› for i j k l
    apply (subst asm_rl[of ‹tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)) = t4 (i,j,k,l)›])
    subgoal by (simp add: t4_def)
    subgoal by (auto simp add: injI t4inj inv_f_f φ_def)
    done

  have *: ‹range t4 = {tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)) |i j k l. True}›
    by (force simp: case_prod_beta t4_def image_iff)

  have "cblinfun_extension_exists (range t4) φ"
    by (rule cblinfun_extension_exists_finite_dim)
       (use * cindependent_tensor_op_butter cspan_tensor_op_butter in auto)

  then obtain G where G: ‹G *⇩V (t4 (i,j,k,l)) = F2 (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))› for i j k l
    unfolding cblinfun_extension_exists_def
    by (metis (no_types, lifting) t4inj φ_def f_inv_into_f rangeI split_conv)

  have *: ‹G *⇩V tensor_op (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l)) = F2 (butterfly (ket i) (ket j)) (butterfly (ket k) (ket l))› for i j k l
    using G by (auto simp: t4_def)
  have *: ‹G *⇩V tensor_op a (butterfly (ket k) (ket l)) = F2 a (butterfly (ket k) (ket l))› for a k l
    apply (rule complex_vector.linear_eq_on_span[where g=‹λa. F2 a _› and B=‹{butterfly (ket k) (ket l)|k l. True}›])
    unfolding cspan_butterfly_ket
    using * apply (auto intro!: clinear_compose[unfolded o_def, where f=‹λa. tensor_op a _› and g=‹(*⇩V) G›])
     apply (metis cbilinear_def tensor_op_cbilinear)
    using assms unfolding cbilinear_def by blast
  have G_F2: ‹G *⇩V tensor_op a b = F2 a b› for a b
    apply (rule complex_vector.linear_eq_on_span[where g=‹F2 a› and B=‹{butterfly (ket k) (ket l)|k l. True}›])
    unfolding cspan_butterfly_ket
    using * apply (auto simp: cblinfun.add_right clinearI
                        intro!: clinear_compose[unfolded o_def, where f=‹tensor_op a› and g=‹(*⇩V) G›])
    apply (meson cbilinear_def tensor_op_cbilinear)
    using assms unfolding cbilinear_def by blast

  have ‹clinear F2' ∧ (∀a b. F2' (tensor_op a b) = F2 a b)›
    unfolding F2'_def tensor_lift_def 
    apply (rule someI[where x=‹(*⇩V) G› and P=‹λG. clinear G ∧ (∀a b. G (tensor_op a b) = F2 a b)›])
    using G_F2 by (simp add: cblinfun.add_right clinearI)

  then show ‹clinear F2'› and ‹(λa b. tensor_lift F2 (tensor_op a b)) = F2›
    unfolding F2'_def by auto
qed


lemma tensor_op_nonzero:
  fixes a :: ‹'a ell2 ⇒⇩C⇩L 'c ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
  assumes ‹a ≠ 0› and ‹b ≠ 0›
  shows ‹a ⊗⇩o b ≠ 0›
proof -
  from ‹a ≠ 0› obtain i where i: ‹a *⇩V ket i ≠ 0›
    by (metis cblinfun.zero_left equal_ket)
  from ‹b ≠ 0› obtain j where j: ‹b *⇩V ket j ≠ 0›
    by (metis cblinfun.zero_left equal_ket)
  from i j have ijneq0: ‹(a *⇩V ket i) ⊗⇩s (b *⇩V ket j) ≠ 0›
    by (simp add: tensor_ell2_nonzero)
  have ‹(a *⇩V ket i) ⊗⇩s (b *⇩V ket j) = (a ⊗⇩o b) *⇩V ket (i,j)›
    by (simp add: tensor_op_ket)
  with ijneq0 show ‹a ⊗⇩o b ≠ 0›
    by force
qed

lemma inj_tensor_ell2_left: ‹inj (λa::'a ell2. a ⊗⇩s b)› if ‹b ≠ 0› for b :: ‹'b ell2›
proof (rule injI, rule ccontr)
  fix x y :: ‹'a ell2›
  assume eq: ‹x ⊗⇩s b = y ⊗⇩s b›
  assume neq: ‹x ≠ y›
  define a where ‹a = x - y›
  from neq a_def have neq0: ‹a ≠ 0›
    by auto
  with ‹b ≠ 0› have ‹a ⊗⇩s b ≠ 0›
    by (simp add: tensor_ell2_nonzero)
  then have ‹x ⊗⇩s b ≠ y ⊗⇩s b›
    unfolding a_def
    by (metis add_cancel_left_left diff_add_cancel tensor_ell2_add1)
  with eq show False
    by auto
qed

lemma inj_tensor_ell2_right: ‹inj (λb::'b ell2. a ⊗⇩s b)› if ‹a ≠ 0› for a :: ‹'a ell2›
proof (rule injI, rule ccontr)
  fix x y :: ‹'b ell2›
  assume eq: ‹a ⊗⇩s x = a ⊗⇩s y›
  assume neq: ‹x ≠ y›
  define b where ‹b = x - y›
  from neq b_def have neq0: ‹b ≠ 0›
    by auto
  with ‹a ≠ 0› have ‹a ⊗⇩s b ≠ 0›
    by (simp add: tensor_ell2_nonzero)
  then have ‹a ⊗⇩s x ≠ a ⊗⇩s y›
    unfolding b_def
    by (metis add_cancel_left_left diff_add_cancel tensor_ell2_add2)
  with eq show False
    by auto
qed

lemma inj_tensor_left: ‹inj (λa::'a ell2 ⇒⇩C⇩L 'c ell2. a ⊗⇩o b)› if ‹b ≠ 0› for b :: ‹'b ell2 ⇒⇩C⇩L 'd ell2›
proof (rule injI, rule ccontr)
  fix x y :: ‹'a ell2 ⇒⇩C⇩L 'c ell2›
  assume eq: ‹x ⊗⇩o b = y ⊗⇩o b›
  assume neq: ‹x ≠ y›
  define a where ‹a = x - y›
  from neq a_def have neq0: ‹a ≠ 0›
    by auto
  with ‹b ≠ 0› have ‹a ⊗⇩o b ≠ 0›
    by (simp add: tensor_op_nonzero)
  then have ‹x ⊗⇩o b ≠ y ⊗⇩o b›
    unfolding a_def
    by (metis add_cancel_left_left diff_add_cancel tensor_op_left_add) 
  with eq show False
    by auto
qed

lemma inj_tensor_right: ‹inj (λb::'b ell2 ⇒⇩C⇩L 'c ell2. a ⊗⇩o b)› if ‹a ≠ 0› for a :: ‹'a ell2 ⇒⇩C⇩L 'd ell2›
proof (rule injI, rule ccontr)
  fix x y :: ‹'b ell2 ⇒⇩C⇩L 'c ell2›
  assume eq: ‹a ⊗⇩o x = a ⊗⇩o y›
  assume neq: ‹x ≠ y›
  define b where ‹b = x - y›
  from neq b_def have neq0: ‹b ≠ 0›
    by auto
  with ‹a ≠ 0› have ‹a ⊗⇩o b ≠ 0›
    by (simp add: tensor_op_nonzero)
  then have ‹a ⊗⇩o x ≠ a ⊗⇩o y›
    unfolding b_def
    by (metis add_cancel_left_left diff_add_cancel tensor_op_right_add) 
  with eq show False
    by auto
qed

lemma tensor_ell2_almost_injective:
  assumes ‹tensor_ell2 a b = tensor_ell2 c d›
  assumes ‹a ≠ 0›
  shows ‹∃γ. b = γ *⇩C d›
proof -
  from ‹a ≠ 0› obtain i where i: ‹cinner (ket i) a ≠ 0›
    by (metis cinner_eq_zero_iff cinner_ket_left ell2_pointwise_ortho)
  have ‹cinner (ket i ⊗⇩s ket j) (a ⊗⇩s b) = cinner (ket i ⊗⇩s ket j) (c ⊗⇩s d)› for j
    using assms by simp
  then have eq2: ‹(cinner (ket i) a) * (cinner (ket j) b) = (cinner (ket i) c) * (cinner (ket j) d)› for j
    by (metis tensor_ell2_inner_prod)
  then obtain γ where ‹cinner (ket i) c = γ * cinner (ket i) a›
    by (metis i eq_divide_eq)
  with eq2 have ‹(cinner (ket i) a) * (cinner (ket j) b) = (cinner (ket i) a) * (γ * cinner (ket j) d)› for j
    by simp
  then have ‹cinner (ket j) b = cinner (ket j) (γ *⇩C d)› for j
    using i by force
  then have ‹b = γ *⇩C d›
    by (simp add: cinner_ket_eqI)
  then show ?thesis
    by auto
qed


lemma tensor_op_almost_injective:
  fixes a c :: ‹'a ell2 ⇒⇩C⇩L 'b ell2›
    and b d :: ‹'c ell2 ⇒⇩C⇩L 'd ell2›
  assumes ‹tensor_op a b = tensor_op c d›
  assumes ‹a ≠ 0›
  shows ‹∃γ. b = γ *⇩C d›
proof (cases ‹d = 0›)
  case False
  from ‹a ≠ 0› obtain ψ where ψ: ‹a *⇩V ψ ≠ 0›
    by (metis cblinfun.zero_left cblinfun_eqI)
  have ‹(a ⊗⇩o b) (ψ ⊗⇩s φ) = (c ⊗⇩o d) (ψ ⊗⇩s φ)› for φ
    using assms by simp
  then have eq2: ‹(a ψ) ⊗⇩s (b φ) = (c ψ) ⊗⇩s (d φ)› for φ
    by (simp add: tensor_op_ell2)
  then have eq2': ‹(d φ) ⊗⇩s (c ψ) = (b φ) ⊗⇩s (a ψ)› for φ
    by (metis swap_ell2_tensor)
  from False obtain φ0 where φ0: ‹d φ0 ≠ 0›
    by (metis cblinfun.zero_left cblinfun_eqI)
  obtain γ where ‹c ψ = γ *⇩C a ψ›
    apply atomize_elim
    using eq2' φ0 by (rule tensor_ell2_almost_injective)
  with eq2 have ‹(a ψ) ⊗⇩s (b φ) = (a ψ) ⊗⇩s (γ *⇩C d φ)› for φ
    by (simp add: tensor_ell2_scaleC1 tensor_ell2_scaleC2)
  then have ‹b φ = γ *⇩C d φ› for φ
    by (smt (verit, best) ψ complex_vector.scale_cancel_right tensor_ell2_almost_injective tensor_ell2_nonzero tensor_ell2_scaleC2)
  then have ‹b = γ *⇩C d›
    by (simp add: cblinfun_eqI)
  then show ?thesis
    by auto
next
  case True
  then have ‹c ⊗⇩o d = 0›
    by (metis add_cancel_right_left tensor_op_right_add)
  then have ‹a ⊗⇩o b = 0›
    using assms(1) by presburger
  with ‹a ≠ 0› have ‹b = 0›
    by (meson tensor_op_nonzero)
  then show ?thesis
    by auto
qed

lemma clinear_tensor_left[simp]: ‹clinear (λa. a ⊗⇩o b :: _ ell2 ⇒⇩C⇩L _ ell2)›
  apply (rule clinearI)
   apply (rule tensor_op_left_add)
  by (rule tensor_op_scaleC_left)

lemma clinear_tensor_right[simp]: ‹clinear (λb. a ⊗⇩o b :: _ ell2 ⇒⇩C⇩L _ ell2)›
  apply (rule clinearI)
   apply (rule tensor_op_right_add)
  by (rule tensor_op_scaleC_right)

lemma tensor_op_0_left[simp]: ‹tensor_op 0 x = (0 :: ('a*'b) ell2 ⇒⇩C⇩L ('c*'d) ell2)›
  apply (rule equal_ket)
  by (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma tensor_op_0_right[simp]: ‹tensor_op x 0 = (0 :: ('a*'b) ell2 ⇒⇩C⇩L ('c*'d) ell2)›
  apply (rule equal_ket)
  by (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma bij_tensor_ell2_one_dim_left:
  assumes ‹ψ ≠ 0›
  shows ‹bij (λx::'b ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
proof (rule bijI)
  show ‹inj (λx::'b ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
    using assms by (rule inj_tensor_ell2_right)
  have ‹∃x. ψ ⊗⇩s x = φ› for φ :: ‹('a*'b) ell2›
  proof (use assms in transfer)
    fix ψ :: ‹'a ⇒ complex› and φ :: ‹'a*'b ⇒ complex›
    assume ‹has_ell2_norm φ› and ‹ψ ≠ (λ_. 0)›
    define c where ‹c = ψ undefined›
    then have ‹ψ a = c› for a 
      by (subst everything_the_same[of _ undefined]) simp
    with ‹ψ ≠ (λ_. 0)› have ‹c ≠ 0›
      by auto

    define x where ‹x j = φ (undefined, j) / c› for j
    have ‹(λ(i, j). ψ i * x j) = φ›
    proof (rule ext, safe)
      fix a :: 'a and b :: 'b
      show "ψ a * x b = φ (a, b)"
        using ‹c ≠ 0› by (simp add: c_def x_def everything_the_same[of a undefined])
    qed
    moreover have ‹has_ell2_norm x›
    proof -
      have ‹(λ(i,j). (φ (i,j))⇧2) abs_summable_on UNIV›
        using ‹has_ell2_norm φ› has_ell2_norm_def by auto
      then have ‹(λ(i,j). (φ (i,j))⇧2) abs_summable_on Pair undefined ` UNIV›
        using summable_on_subset_banach by blast
      then have ‹(λj. (φ (undefined,j))⇧2) abs_summable_on UNIV›
        by (subst (asm) summable_on_reindex) (auto simp: o_def inj_def)
      then have ‹(λj. (φ (undefined,j) / c)⇧2) abs_summable_on UNIV›
        by (simp add: divide_inverse power_mult_distrib norm_mult summable_on_cmult_left)
      then have ‹(λj. (x j)⇧2) abs_summable_on UNIV›
        by (simp add: x_def)
      then show ?thesis
        using has_ell2_norm_def by blast
    qed
    ultimately show ‹∃x∈Collect has_ell2_norm. (λ(i, j). ψ i * x j) = φ›
      by (intro bexI[where x=x]) auto
  qed

  then show ‹surj (λx::'b ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
    by (metis surj_def)
qed

lemma bij_tensor_op_one_dim_left:
  fixes a :: ‹'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2›
  assumes ‹a ≠ 0›
  shows ‹bij (λx::'c ell2 ⇒⇩C⇩L 'd ell2. a ⊗⇩o x)›
proof -
  have [simp]: ‹bij (Pair (undefined::'a))›
    by (rule o_bij[of snd]) auto
  have [simp]: ‹bij (Pair (undefined::'b))›
    by (rule o_bij[of snd]) auto
  define t where ‹t x = a ⊗⇩o x› for x :: ‹'c ell2 ⇒⇩C⇩L 'd ell2›
  define u :: ‹'c ell2 ⇒⇩C⇩L ('a×'c) ell2› where ‹u = classical_operator (Some o Pair undefined)›
  define v :: ‹'d ell2 ⇒⇩C⇩L ('b×'d) ell2› where ‹v = classical_operator (Some o Pair undefined)›
  have [simp]: ‹unitary u› ‹unitary v›
    by (simp_all add: u_def v_def)
  have u_ket[simp]: ‹u *⇩V ket x = ket (undefined, x)› for x
    by (simp add: u_def classical_operator_ket classical_operator_exists_inj inj_def)
  have uadj_ket[simp]: ‹u* *⇩V ket (z, x) = ket x› for x z
    by (subst everything_the_same[of _ undefined])
       (metis (no_types, opaque_lifting) u_ket cinner_adj_right cinner_ket_eqI cinner_ket_same orthogonal_ket prod.inject)
  have v_ket[simp]: ‹v *⇩V ket x = ket (undefined, x)› for x
    by (simp add: v_def classical_operator_ket classical_operator_exists_inj inj_def)
  have [simp]: ‹v *⇩V x = ket undefined ⊗⇩s x› for x
    by (rule fun_cong[where x=x], rule bounded_clinear_equal_ket)
       (auto simp add: bounded_clinear_tensor_ell21 cblinfun.bounded_clinear_right tensor_ell2_ket)
  define a' :: complex where ‹a' = one_dim_iso a›
  from assms have ‹a' ≠ 0›
    using a'_def one_dim_iso_of_zero' by auto
  have a_a': ‹a = of_complex a'›
    by (simp add: a'_def) 
  have ‹t x *⇩V ket (i,j) = (a' *⇩C v o⇩C⇩L x o⇩C⇩L u*) *⇩V ket (i,j)› for x i j
    apply (simp add: t_def)
    apply (simp add: ket_CARD_1_is_1 tensor_op_ell2 flip: tensor_ell2_ket)
    by (metis a'_def one_cblinfun_apply_one one_dim_scaleC_1 scaleC_cblinfun.rep_eq tensor_ell2_scaleC1) 
  then have t: ‹t x = (a' *⇩C v o⇩C⇩L x o⇩C⇩L u*)› for x
    by (intro equal_ket) auto
  define s where ‹s y = (inverse a' *⇩C (v)* o⇩C⇩L y o⇩C⇩L u)› for y
  have ‹s (t x) = (a' * inverse a') *⇩C (((v)* o⇩C⇩L v) o⇩C⇩L x o⇩C⇩L (u* o⇩C⇩L u))› for x
    apply (simp add: s_def t cblinfun_compose_assoc)
    by (simp flip: cblinfun_compose_assoc)?
  also have ‹… x = x› for x
    using ‹a' ≠ 0› by simp
  finally have ‹s o t = id›
    by auto
  have ‹t (s y) = (a' * inverse a') *⇩C ((v o⇩C⇩L (v)*) o⇩C⇩L y o⇩C⇩L (u o⇩C⇩L u*))› for y
    apply (simp add: s_def t cblinfun_compose_assoc)
    by (simp flip: cblinfun_compose_assoc)?
  also have ‹… y = y› for y
    using ‹a' ≠ 0› by simp
  finally have ‹t o s = id›
    by auto
  from ‹s o t = id› ‹t o s = id›
  show ‹bij t›
    using o_bij by blast
qed

lemma bij_tensor_op_one_dim_right:
  assumes ‹b ≠ 0›
  shows ‹bij (λx::'c ell2 ⇒⇩C⇩L 'd ell2. x ⊗⇩o (b :: 'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2))›
    (is ‹bij ?f›)
proof -
  let ?sf = ‹(λx. swap_ell2 o⇩C⇩L (?f x) o⇩C⇩L swap_ell2)›
  let ?s = ‹(λx. swap_ell2 o⇩C⇩L x o⇩C⇩L swap_ell2)›
  let ?g = ‹(λx::'c ell2 ⇒⇩C⇩L 'd ell2. (b :: 'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2) ⊗⇩o x)›
  have ‹?sf = ?g›
    by (auto intro!: ext tensor_ell2_extensionality simp add: swap_ell2_tensor tensor_op_ell2)
  have ‹bij ?g›
    using assms by (rule bij_tensor_op_one_dim_left)
  have ‹?s o ?sf = ?f›
    apply (auto intro!: ext simp: cblinfun_assoc_left)
    by (auto simp: cblinfun_assoc_right)?
  also have ‹bij ?s›
    apply (rule o_bij[where g=‹(λx. swap_ell2 o⇩C⇩L x o⇩C⇩L swap_ell2)›])
     apply (auto intro!: ext simp: cblinfun_assoc_left)
    by (auto simp: cblinfun_assoc_right)?
  show ‹bij ?f›
    apply (subst ‹?s o ?sf = ?f›[symmetric], subst ‹?sf = ?g›)
    using ‹bij ?g› ‹bij ?s› by (rule bij_comp)
qed

lemma overlapping_tensor:
  fixes a23 :: ‹('a2*'a3) ell2 ⇒⇩C⇩L ('b2*'b3) ell2›
    and b12 :: ‹('a1*'a2) ell2 ⇒⇩C⇩L ('b1*'b2) ell2›
  assumes eq: ‹butterfly ψ ψ' ⊗⇩o a23 = assoc_ell2 o⇩C⇩L (b12 ⊗⇩o butterfly φ φ') o⇩C⇩L assoc_ell2*›
  assumes ‹ψ ≠ 0› ‹ψ' ≠ 0› ‹φ ≠ 0› ‹φ' ≠ 0›
  shows ‹∃c. butterfly ψ ψ' ⊗⇩o a23 = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
proof -
  let ?id1 = ‹id_cblinfun :: unit ell2 ⇒⇩C⇩L unit ell2›
  note id_cblinfun_eq_1[simp del]
  define d where ‹d = butterfly ψ ψ' ⊗⇩o a23›

  define ψ⇩n ψ⇩n' a23⇩n where ‹ψ⇩n = ψ /⇩C norm ψ› and ‹ψ⇩n' = ψ' /⇩C norm ψ'› and ‹a23⇩n = norm ψ *⇩C norm ψ' *⇩C a23›
  have [simp]: ‹norm ψ⇩n = 1› ‹norm ψ⇩n' = 1›
    using ‹ψ ≠ 0› ‹ψ' ≠ 0› by (auto simp: ψ⇩n_def ψ⇩n'_def norm_inverse)
  have n1: ‹butterfly ψ⇩n ψ⇩n' ⊗⇩o a23⇩n = butterfly ψ ψ' ⊗⇩o a23›
    by (auto simp: ψ⇩n_def ψ⇩n'_def a23⇩n_def tensor_op_scaleC_left tensor_op_scaleC_right field_simps)

  define φ⇩n φ⇩n' b12⇩n where ‹φ⇩n = φ /⇩C norm φ› and ‹φ⇩n' = φ' /⇩C norm φ'› and ‹b12⇩n = norm φ *⇩C norm φ' *⇩C b12›
  have [simp]: ‹norm φ⇩n = 1› ‹norm φ⇩n' = 1›
    using ‹φ ≠ 0› ‹φ' ≠ 0› by (auto simp: φ⇩n_def φ⇩n'_def norm_inverse)
  have n2: ‹b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n' = b12 ⊗⇩o butterfly φ φ'›
    by (auto simp: φ⇩n_def φ⇩n'_def b12⇩n_def tensor_op_scaleC_left tensor_op_scaleC_right field_simps)

  define c' :: ‹(unit*'a2*unit) ell2 ⇒⇩C⇩L (unit*'b2*unit) ell2› 
    where ‹c' = (vector_to_cblinfun ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n)* o⇩C⇩L d
            o⇩C⇩L (vector_to_cblinfun ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n')›

  define c'' :: ‹'a2 ell2 ⇒⇩C⇩L 'b2 ell2›
    where ‹c'' = inv (λc''. id_cblinfun ⊗⇩o c'' ⊗⇩o id_cblinfun) c'›

  have *: ‹bij (λc''::'a2 ell2 ⇒⇩C⇩L 'b2 ell2. ?id1 ⊗⇩o c'' ⊗⇩o ?id1)›
    by (subst asm_rl[of ‹_ = (λx. id_cblinfun ⊗⇩o x) o (λc''. c'' ⊗⇩o id_cblinfun)›])
       (auto intro!: bij_comp bij_tensor_op_one_dim_left bij_tensor_op_one_dim_right)

  have c'_c'': ‹c' = ?id1 ⊗⇩o c'' ⊗⇩o ?id1›
    unfolding c''_def 
    by (rule surj_f_inv_f[where y=c', symmetric]) (use * in ‹rule bij_is_surj›)

  define c :: ‹'a2 ell2 ⇒⇩C⇩L 'b2 ell2›
    where ‹c = c'' /⇩C norm ψ /⇩C norm ψ' /⇩C norm φ /⇩C norm φ'›

  have aux: ‹assoc_ell2* o⇩C⇩L (assoc_ell2 o⇩C⇩L x o⇩C⇩L assoc_ell2*) o⇩C⇩L assoc_ell2 = x› for x
    apply (simp add: cblinfun_assoc_left)
    by (simp add: cblinfun_assoc_right)?
  have aux2: ‹(assoc_ell2 o⇩C⇩L ((x ⊗⇩o y) ⊗⇩o z) o⇩C⇩L assoc_ell2*) = x ⊗⇩o (y ⊗⇩o z)› for x y z
    by (intro equal_ket) (auto simp flip: tensor_ell2_ket simp: assoc_ell2'_tensor assoc_ell2_tensor tensor_op_ell2)

  have ‹d = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L d o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
    by (auto simp: d_def n1[symmetric] comp_tensor_op cnorm_eq_1[THEN iffD1])
  also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L (b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n')
                  o⇩C⇩L assoc_ell2* o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
    by (auto simp: d_def eq n2 cblinfun_assoc_left)
  also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L 
               ((id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L (b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n') o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n'))
               o⇩C⇩L assoc_ell2* o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
    by (auto simp: comp_tensor_op cnorm_eq_1[THEN iffD1])
  also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L 
               ((id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L (assoc_ell2* o⇩C⇩L d o⇩C⇩L assoc_ell2) o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n'))
               o⇩C⇩L assoc_ell2* o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
    by (auto simp: d_def n2 eq aux)
  also have ‹… = ((butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L (assoc_ell2 o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L assoc_ell2*))
               o⇩C⇩L d o⇩C⇩L ((assoc_ell2 o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n') o⇩C⇩L assoc_ell2*) o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun))›
    by (auto simp: sandwich_def cblinfun_assoc_left)
  also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n)
               o⇩C⇩L d o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n')›
    apply (simp only: tensor_id[symmetric] comp_tensor_op aux2)
    by (simp add: cnorm_eq_1[THEN iffD1])
  also have ‹… = (vector_to_cblinfun ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n)
               o⇩C⇩L c' o⇩C⇩L (vector_to_cblinfun ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n')*›
    apply (simp add: c'_def butterfly_def_one_dim[where 'c="unit ell2"] cblinfun_assoc_left comp_tensor_op
                      tensor_op_adjoint cnorm_eq_1[THEN iffD1])
    by (simp add: cblinfun_assoc_right comp_tensor_op)
  also have ‹… = butterfly ψ⇩n ψ⇩n' ⊗⇩o c'' ⊗⇩o butterfly φ⇩n φ⇩n'›
    by (simp add: c'_c'' comp_tensor_op tensor_op_adjoint butterfly_def_one_dim[symmetric])
  also have ‹… = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
    by (simp add: ψ⇩n_def ψ⇩n'_def φ⇩n_def φ⇩n'_def c_def tensor_op_scaleC_left tensor_op_scaleC_right)
  finally have d_c: ‹d = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
    by -
  then show ?thesis
    by (auto simp: d_def)
qed


lemma tensor_op_pos: ‹a ⊗⇩o b ≥ 0› if [simp]: ‹a ≥ 0› ‹b ≥ 0›
  for a :: ‹'a ell2 ⇒⇩C⇩L 'a ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'b ell2›
    ― ‹\<^cite>‹"Lemma 18" in "references-v3"››
proof -
  have ‹(sqrt_op a ⊗⇩o sqrt_op b)* o⇩C⇩L (sqrt_op a ⊗⇩o sqrt_op b) = a ⊗⇩o b›
    by (simp add: tensor_op_adjoint comp_tensor_op positive_selfadjointI[unfolded selfadjoint_def])
  then show ‹a ⊗⇩o b ≥ 0›
    by (metis positive_cblinfun_squareI)
qed

lemma abs_op_tensor: ‹abs_op (a ⊗⇩o b) = abs_op a ⊗⇩o abs_op b›
  ― ‹\<^cite>‹"Lemma 18" in "references-v3"››
proof -
  have ‹(abs_op a ⊗⇩o abs_op b)* o⇩C⇩L (abs_op a ⊗⇩o abs_op b) = (a ⊗⇩o b)* o⇩C⇩L (a ⊗⇩o b)›
    by (simp add: tensor_op_adjoint comp_tensor_op abs_op_def positive_cblinfun_squareI positive_selfadjointI[unfolded selfadjoint_def])
  then show ?thesis
    by (metis abs_opI abs_op_pos tensor_op_pos)
qed

lemma trace_class_tensor: ‹trace_class (a ⊗⇩o b)› if ‹trace_class a› and ‹trace_class b›
    ― ‹\<^cite>‹"Lemma 32" in "references-v3"››
proof -
  from ‹trace_class a›
  have a: ‹(λx. ket x ∙⇩C (abs_op a *⇩V ket x)) abs_summable_on UNIV›
    by (auto simp add: trace_class_iff_summable[OF is_onb_ket] summable_on_reindex o_def)
  from ‹trace_class b›
  have b: ‹(λy. ket y ∙⇩C (abs_op b *⇩V ket y)) abs_summable_on UNIV›
    by (auto simp add: trace_class_iff_summable[OF is_onb_ket] summable_on_reindex o_def)
  from a b have ‹(λ(x,y). (ket x ∙⇩C (abs_op a *⇩V ket x)) * (ket y ∙⇩C (abs_op b *⇩V ket y))) abs_summable_on UNIV × UNIV›
    by (rule abs_summable_times)
  then have ‹(λ(x,y). (ket x ⊗⇩s ket y) ∙⇩C ((abs_op a ⊗⇩o abs_op b) *⇩V (ket x ⊗⇩s ket y))) abs_summable_on UNIV × UNIV›
    by (simp add: tensor_op_ell2 case_prod_unfold flip: tensor_ell2_ket)
  then have ‹(λxy. ket xy ∙⇩C ((abs_op a ⊗⇩o abs_op b) *⇩V ket xy)) abs_summable_on UNIV›
    by (simp add: case_prod_beta tensor_ell2_ket)
  then have ‹(λxy. ket xy ∙⇩C (abs_op (a ⊗⇩o b) *⇩V ket xy)) abs_summable_on UNIV›
    by (simp add: abs_op_tensor)
  then show ‹trace_class (a ⊗⇩o b)›
    by (auto simp add: trace_class_iff_summable[OF is_onb_ket] summable_on_reindex o_def)
qed

lemma swap_tensor_op[simp]: ‹swap_ell2 o⇩C⇩L (a ⊗⇩o b) o⇩C⇩L swap_ell2 = b ⊗⇩o a›
  by (auto intro!: equal_ket simp add: tensor_op_ell2 simp flip: tensor_ell2_ket)

lemma swap_tensor_op_sandwich[simp]: ‹sandwich swap_ell2 (a ⊗⇩o b) = b ⊗⇩o a›
  by (simp add: sandwich_apply)

lemma swap_ell2_commute_tensor_op: 
  ‹swap_ell2 o⇩C⇩L (a ⊗⇩o b) = (b ⊗⇩o a) o⇩C⇩L swap_ell2›
  by (auto intro!: tensor_ell2_extensionality simp: tensor_op_ell2)

lemma trace_class_tensor_op_swap: ‹trace_class (a ⊗⇩o b) ⟷ trace_class (b ⊗⇩o a)›
proof (rule iffI)
  assume ‹trace_class (a ⊗⇩o b)›
  then have ‹trace_class (swap_ell2 o⇩C⇩L (a ⊗⇩o b) o⇩C⇩L swap_ell2)›
    using trace_class_comp_left trace_class_comp_right by blast
  then show ‹trace_class (b ⊗⇩o a)›
    by simp
next
  assume ‹trace_class (b ⊗⇩o a)›
  then have ‹trace_class (swap_ell2 o⇩C⇩L (b ⊗⇩o a) o⇩C⇩L swap_ell2)›
    using trace_class_comp_left trace_class_comp_right by blast
  then show ‹trace_class (a ⊗⇩o b)›
    by simp
qed


lemma trace_class_tensor_iff: ‹trace_class (a ⊗⇩o b) ⟷ (trace_class a ∧ trace_class b) ∨ a = 0 ∨ b = 0›
proof (intro iffI)
  show ‹trace_class a ∧ trace_class b ∨ a = 0 ∨ b = 0 ⟹ trace_class (a ⊗⇩o b)›
    by (auto simp add: trace_class_tensor)
  show ‹trace_class a ∧ trace_class b ∨ a = 0 ∨ b = 0› if ‹trace_class (a ⊗⇩o b)›
  proof (cases ‹a = 0 ∨ b = 0›)
    case True
    then show ?thesis
      by simp
  next
    case False
    then have ‹a ≠ 0› and ‹b ≠ 0›
      by auto
    have *: ‹trace_class a› if ‹trace_class (a ⊗⇩o b)› and ‹b ≠ 0› for a :: ‹'e ell2 ⇒⇩C⇩L 'g ell2› and b :: ‹'f ell2 ⇒⇩C⇩L 'h ell2›
    proof -
      from ‹b ≠ 0› have ‹abs_op b ≠ 0›
        using abs_op_nondegenerate by blast
      then obtain ψ0 where ψ0: ‹ψ0 ∙⇩C (abs_op b *⇩V ψ0) ≠ 0›
        by (metis cblinfun.zero_left cblinfun_cinner_eqI cinner_zero_right)
      define ψ where ‹ψ = sgn ψ0›
      with ψ0 have ‹ψ ∙⇩C (abs_op b *⇩V ψ) ≠ 0› and ‹norm ψ = 1›
         by (auto simp add: ψ_def norm_sgn sgn_div_norm cblinfun.scaleR_right field_simps)
      then have ‹∃B. {ψ} ⊆ B ∧ is_onb B›
        by (intro orthonormal_basis_exists) auto
      then obtain B where [simp]: ‹is_onb B› and ‹ψ ∈ B›
        by auto
      define A :: ‹'e ell2 set› where ‹A = range ket›      
      then have [simp]: ‹is_onb A› by simp
      with ‹is_onb B› have ‹is_onb {α ⊗⇩s β |α β. α ∈ A ∧ β ∈ B}›
        by (simp add: tensor_ell2_is_onb)
      with ‹trace_class (a ⊗⇩o b)›
      have ‹(λγ. γ ∙⇩C (abs_op (a ⊗⇩o b) *⇩V γ)) abs_summable_on {α ⊗⇩s β |α β. α ∈ A ∧ β ∈ B}›
        using trace_class_iff_summable by auto
      then have ‹(λγ. γ ∙⇩C (abs_op (a ⊗⇩o b) *⇩V γ)) abs_summable_on (λα. α ⊗⇩s ψ) ` A›
        by (rule summable_on_subset_banach) (use ‹ψ ∈ B› in blast)
      then have ‹(λα. (α ⊗⇩s ψ) ∙⇩C (abs_op (a ⊗⇩o b) *⇩V (α ⊗⇩s ψ))) abs_summable_on A›
      proof (subst (asm) summable_on_reindex)
        show "inj_on (λα. α ⊗⇩s ψ) A"
         by (metis UNIV_I ‹norm ψ = 1› inj_on_subset inj_tensor_ell2_left norm_le_zero_iff not_one_le_zero subset_iff)
      qed (simp_all add: o_def)
      then have ‹(λα. norm (α ∙⇩C (abs_op a *⇩V α)) * norm (ψ ∙⇩C (abs_op b *⇩V ψ))) summable_on A›
        by (simp add: abs_op_tensor tensor_op_ell2 norm_mult)
      then have ‹(λα. α ∙⇩C (abs_op a *⇩V α)) abs_summable_on A›
        by (rule summable_on_cmult_left'[THEN iffD1, rotated])
           (use ‹ψ ∙⇩C (abs_op b *⇩V ψ) ≠ 0› norm_eq_zero in ‹blast›)
      then show ‹trace_class a›
        using ‹is_onb A› trace_classI by blast
    qed
    from *[of a b] ‹b ≠ 0› ‹trace_class (a ⊗⇩o b)› have ‹trace_class a›
      by simp
    have ‹trace_class (b ⊗⇩o a)›
      using that trace_class_tensor_op_swap by blast
    from *[of b a] ‹a ≠ 0› ‹trace_class (b ⊗⇩o a)› have ‹trace_class b›
      by simp
    from ‹trace_class a› ‹trace_class b› show ?thesis
      by simp
  qed
qed


lemma trace_tensor: ‹trace (a ⊗⇩o b) = trace a * trace b›
  ― ‹\<^cite>‹"Lemma 32" in "references-v3"››
proof -
  consider (tc) ‹trace_class a› ‹trace_class b› | (zero) ‹a = 0 ∨ b = 0› | (nota) ‹a ≠ 0› ‹b ≠ 0› ‹¬ trace_class a› | (notb) ‹a ≠ 0› ‹b ≠ 0› ‹¬ trace_class b›
    by blast
  then show ?thesis
  proof cases
    case tc
    then have *: ‹trace_class (a ⊗⇩o b)›
      by (simp add: trace_class_tensor)
    have sum: ‹(λ(x, y). ket (x, y) ∙⇩C ((a ⊗⇩o b) *⇩V ket (x, y))) summable_on UNIV›
      using trace_exists[OF is_onb_ket *]
      by (simp_all add: o_def case_prod_unfold summable_on_reindex)

    have ‹trace a * trace b = (∑⇩∞x. ∑⇩∞y. ket x ∙⇩C (a *⇩V ket x) * (ket y ∙⇩C (b *⇩V ket y)))›
      apply (simp add: trace_ket_sum tc flip: infsum_cmult_left')
      by (simp flip: infsum_cmult_right')
    also have ‹… = (∑⇩∞x. ∑⇩∞y. ket (x,y) ∙⇩C ((a ⊗⇩o b) *⇩V ket (x,y)))›
      by (simp add: tensor_op_ell2 flip: tensor_ell2_ket)
    also have ‹… = (∑⇩∞xy∈UNIV. ket xy ∙⇩C ((a ⊗⇩o b) *⇩V ket xy))›
      apply (simp add: sum infsum_Sigma'_banach)
      by (simp add: case_prod_unfold)
    also have ‹… = trace (a ⊗⇩o b)›
      by (simp add: "*" trace_ket_sum)
    finally show ?thesis 
      by simp
  next
    case zero
    then show ?thesis by auto
  next
    case nota
    then have [simp]: ‹trace a = 0›
      unfolding trace_def by simp
    from nota have ‹¬ trace_class (a ⊗⇩o b)›
      by (simp add: trace_class_tensor_iff)
    then have [simp]: ‹trace (a ⊗⇩o b) = 0›
      unfolding trace_def by simp
    show ?thesis 
      by simp
  next
    case notb
    then have [simp]: ‹trace b = 0›
      unfolding trace_def by simp
    from notb have ‹¬ trace_class (a ⊗⇩o b)›
      by (simp add: trace_class_tensor_iff)
    then have [simp]: ‹trace (a ⊗⇩o b) = 0›
      unfolding trace_def by simp
    show ?thesis 
      by simp
  qed
qed

lemma isometry_tensor_op: ‹isometry (U ⊗⇩o V)› if ‹isometry U› and ‹isometry V›
  unfolding isometry_def using that by (simp add: tensor_op_adjoint comp_tensor_op)

lemma is_Proj_tensor_op: ‹is_Proj a ⟹ is_Proj b ⟹ is_Proj (a ⊗⇩o b)›
  by (simp add: comp_tensor_op is_Proj_algebraic tensor_op_adjoint)

lemma isometry_tensor_id_right[simp]:
  fixes U :: ‹'a ell2 ⇒⇩C⇩L 'b ell2›
  shows ‹isometry (U ⊗⇩o (id_cblinfun :: 'c ell2 ⇒⇩C⇩L _)) ⟷ isometry U›
proof (rule iffI)
  assume ‹isometry U›
  then show ‹isometry (U ⊗⇩o id_cblinfun)›
    unfolding isometry_def
    by (auto simp add: tensor_op_adjoint comp_tensor_op)
next
  let ?id = ‹id_cblinfun :: 'c ell2 ⇒⇩C⇩L _›
  assume asm: ‹isometry (U ⊗⇩o ?id)›
  then have ‹(U* o⇩C⇩L U) ⊗⇩o ?id = id_cblinfun ⊗⇩o ?id›
    by (simp add: isometry_def tensor_op_adjoint comp_tensor_op)
  then have ‹U* o⇩C⇩L U = id_cblinfun›
    by (rule inj_tensor_left[of ?id, unfolded inj_def, rule_format, rotated]) simp
  then show ‹isometry U›
    by (simp add: isometry_def)
qed

lemma isometry_tensor_id_left[simp]: 
  fixes U :: ‹'a ell2 ⇒⇩C⇩L 'b ell2›
  shows ‹isometry ((id_cblinfun :: 'c ell2 ⇒⇩C⇩L _) ⊗⇩o U) ⟷ isometry U›
proof (rule iffI)
  assume ‹isometry U›
  then show ‹isometry (id_cblinfun ⊗⇩o U)›
    unfolding isometry_def
    by (auto simp add: tensor_op_adjoint comp_tensor_op)
next
  let ?id = ‹id_cblinfun :: 'c ell2 ⇒⇩C⇩L _›
  assume asm: ‹isometry (?id ⊗⇩o U)›
  then have ‹?id ⊗⇩o (U* o⇩C⇩L U) = ?id ⊗⇩o id_cblinfun›
    by (simp add: isometry_def tensor_op_adjoint comp_tensor_op)
  then have ‹U* o⇩C⇩L U = id_cblinfun›
    by (rule inj_tensor_right[of ?id, unfolded inj_def, rule_format, rotated]) simp
  then show ‹isometry U›
    by (simp add: isometry_def)
qed

lemma unitary_tensor_id_right[simp]: ‹unitary (U ⊗⇩o id_cblinfun) ⟷ unitary U›
  unfolding unitary_twosided_isometry
  by (simp add: tensor_op_adjoint)

lemma unitary_tensor_id_left[simp]: ‹unitary (id_cblinfun ⊗⇩o U) ⟷ unitary U›
  unfolding unitary_twosided_isometry
  by (simp add: tensor_op_adjoint)


lemma sandwich_tensor_op: ‹sandwich (a ⊗⇩o b) (c ⊗⇩o d) = sandwich a c ⊗⇩o sandwich b d›
  by (simp add: sandwich_apply tensor_op_adjoint flip: cblinfun_compose_assoc comp_tensor_op)

lemma sandwich_assoc_ell2_tensor_op[simp]: ‹sandwich assoc_ell2 ((a ⊗⇩o b) ⊗⇩o c) = a ⊗⇩o (b ⊗⇩o c)›
  by (auto intro!: tensor_ell2_extensionality3 
      simp: sandwich_apply assoc_ell2'_tensor assoc_ell2_tensor tensor_op_ell2)

lemma unitary_tensor_op: ‹unitary (a ⊗⇩o b)› if [simp]: ‹unitary a› ‹unitary b›
  by (auto intro!: unitaryI simp add: tensor_op_adjoint comp_tensor_op)

lemma tensor_ell2_right_butterfly: ‹tensor_ell2_right ψ o⇩C⇩L tensor_ell2_right φ* = id_cblinfun ⊗⇩o butterfly ψ φ›
  by (auto intro!: equal_ket cinner_ket_eqI simp: tensor_op_ell2 simp flip: tensor_ell2_ket)
lemma tensor_ell2_left_butterfly: ‹tensor_ell2_left ψ o⇩C⇩L tensor_ell2_left φ* = butterfly ψ φ ⊗⇩o id_cblinfun›
  by (auto intro!: equal_ket cinner_ket_eqI simp: tensor_op_ell2 simp flip: tensor_ell2_ket)

lift_definition tc_tensor :: ‹('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class ⇒ 
      (('a × 'c) ell2, ('b × 'd) ell2) trace_class› is
  tensor_op
  by (auto intro!: trace_class_tensor)

lemma trace_norm_tensor: ‹trace_norm (a ⊗⇩o b) = trace_norm a * trace_norm b›
  by (rule of_real_hom.injectivity[where 'a=complex])
     (simp add: abs_op_tensor trace_tensor flip: trace_abs_op)


lemma bounded_cbilinear_tc_tensor: ‹bounded_cbilinear tc_tensor›
  unfolding bounded_cbilinear_def
  by transfer
     (auto intro!: exI[of _ 1]
           simp: trace_norm_tensor tensor_op_left_add tensor_op_right_add tensor_op_scaleC_left tensor_op_scaleC_right)
lemmas bounded_clinear_tc_tensor_left[bounded_clinear] = bounded_cbilinear.bounded_clinear_left[OF bounded_cbilinear_tc_tensor]
lemmas bounded_clinear_tc_tensor_right[bounded_clinear] = bounded_cbilinear.bounded_clinear_right[OF bounded_cbilinear_tc_tensor]


lemma tc_tensor_scaleC_left: ‹tc_tensor (c *⇩C a) b = c *⇩C tc_tensor a b›
  by transfer' (simp add: tensor_op_scaleC_left)
lemma tc_tensor_scaleC_right: ‹tc_tensor a (c *⇩C b) = c *⇩C tc_tensor a b›
  by transfer' (simp add: tensor_op_scaleC_right)
  
lemma comp_tc_tensor: ‹tc_compose (tc_tensor a b) (tc_tensor c d) = tc_tensor (tc_compose a c) (tc_compose b d)›
  by transfer' (rule comp_tensor_op)

lemma norm_tc_tensor: ‹norm (tc_tensor a b) = norm a * norm b›
  by (transfer', rule of_real_hom.injectivity[where 'a=complex])
     (simp add: abs_op_tensor trace_tensor flip: trace_abs_op)

lemma tc_tensor_pos: ‹tc_tensor a b ≥ 0› if ‹a ≥ 0› and ‹b ≥ 0›
  for a :: ‹('a ell2,'a ell2) trace_class› and b :: ‹('b ell2,'b ell2) trace_class›
  using that by transfer' (rule tensor_op_pos)

interpretation tensor_op_cbilinear: bounded_cbilinear tensor_op
  by simp

lemma tensor_op_mono_left:
  fixes a :: ‹'a ell2 ⇒⇩C⇩L 'a ell2› and c :: ‹'b ell2 ⇒⇩C⇩L 'b ell2›
  assumes ‹a ≤ b› and ‹c ≥ 0›
  shows ‹a ⊗⇩o c ≤ b ⊗⇩o c›
proof -
  have ‹b - a ≥ 0›
    by (simp add: assms(1))
  with ‹c ≥ 0› have ‹(b - a) ⊗⇩o c ≥ 0›
    by (intro tensor_op_pos)
  then have ‹b ⊗⇩o c - a ⊗⇩o c ≥ 0›
    by (simp add: tensor_op_cbilinear.diff_left)
  then show ?thesis
    by simp
qed

lemma tensor_op_mono_right:
  fixes a :: ‹'a ell2 ⇒⇩C⇩L 'a ell2› and b :: ‹'b ell2 ⇒⇩C⇩L 'b ell2›
  assumes ‹b ≤ c› and ‹a ≥ 0›
  shows ‹a ⊗⇩o b ≤ a ⊗⇩o c›
proof -
  have ‹c - b ≥ 0›
    by (simp add: assms(1))
  with ‹a ≥ 0› have ‹a ⊗⇩o (c - b) ≥ 0›
    by (intro tensor_op_pos)
  then have ‹a ⊗⇩o c - a ⊗⇩o b ≥ 0›
    by (simp add: tensor_op_cbilinear.diff_right)
  then show ?thesis
    by simp
qed


lemma tensor_op_mono:
  fixes a :: ‹'a ell2 ⇒⇩C⇩L 'a ell2› and c :: ‹'b ell2 ⇒⇩C⇩L 'b ell2›
  assumes ‹a ≤ b› and ‹c ≤ d› and ‹b ≥ 0› and ‹c ≥ 0›
  shows ‹a ⊗⇩o c ≤ b ⊗⇩o d›
proof -
  have ‹a ⊗⇩o c ≤ b ⊗⇩o c›
    using ‹a ≤ b› and ‹c ≥ 0›
    by (rule tensor_op_mono_left)
  also have ‹… ≤ b ⊗⇩o d›
    using ‹c ≤ d› and ‹b ≥ 0›
    by (rule tensor_op_mono_right)
  finally show ?thesis
    by -
qed



lemma sandwich_tc_tensor: ‹sandwich_tc (E ⊗⇩o F) (tc_tensor t u) = tc_tensor (sandwich_tc E t) (sandwich_tc F u)›
  by (transfer fixing: E F) (simp add: sandwich_tensor_op)


lemma tensor_tc_butterfly: "tc_tensor (tc_butterfly ψ ψ') (tc_butterfly φ φ') = tc_butterfly (tensor_ell2 ψ φ) (tensor_ell2 ψ' φ')"
  by (transfer fixing: φ φ' ψ ψ') (simp add: tensor_butterfly)


lemma separating_set_bounded_clinear_tc_tensor:
  shows ‹separating_set bounded_clinear ((λ(ρ,σ). tc_tensor ρ σ) ` (UNIV × UNIV))›
proof -
  have ‹⊤ = ccspan ((λ(x, y). tc_butterfly x y) ` (range ket × range ket))›
    by (simp add: onb_butterflies_span_trace_class)
  also have ‹… = ccspan ((λ(x, y, z, w). tc_butterfly (x ⊗⇩s y) (z ⊗⇩s w)) ` (range ket × range ket × range ket × range ket))›
    by (auto intro!: arg_cong[where f=ccspan] image_eqI simp: tensor_ell2_ket)
  also have ‹… = ccspan ((λ(x, y, z, w). tc_tensor (tc_butterfly x z) (tc_butterfly y w)) ` (range ket × range ket × range ket × range ket))›
    by (simp add: tensor_tc_butterfly)
  also have ‹… ≤ ccspan ((λ(ρ, σ). tc_tensor ρ σ) ` (UNIV × UNIV))›
    by (auto intro!: ccspan_mono)
  finally show ?thesis
    by (intro separating_set_bounded_clinear_dense) (use top_le in blast)
qed


lemma separating_set_bounded_clinear_tc_tensor_nested:
  assumes ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector) ⇒ _) A›
  assumes ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector) ⇒ _) B›
  shows ‹separating_set (bounded_clinear :: (_ => 'e::complex_normed_vector) ⇒ _) ((λ(ρ,σ). tc_tensor ρ σ) ` (A × B))›
  using separating_set_bounded_clinear_tc_tensor bounded_cbilinear_tc_tensor assms
  by (rule separating_set_bounded_cbilinear_nested)

lemma tc_tensor_0_left[simp]: ‹tc_tensor 0 x = 0›
  by transfer' simp
lemma tc_tensor_0_right[simp]: ‹tc_tensor x 0 = 0›
  by transfer' simp

lemma sandwich_tensor_ell2_right': ‹sandwich (tensor_ell2_right ψ) *⇩V a = a ⊗⇩o selfbutter ψ›
  apply (rule cblinfun_cinner_tensor_eqI)
  by (simp add: sandwich_apply tensor_op_ell2 cblinfun.scaleC_right)

lemma sandwich_tensor_ell2_left': ‹sandwich (tensor_ell2_left ψ) *⇩V a = selfbutter ψ ⊗⇩o a›
  apply (rule cblinfun_cinner_tensor_eqI)
  by (simp add: sandwich_apply tensor_op_ell2 cblinfun.scaleC_right)


subsection ‹Tensor product of subspaces›

definition tensor_ccsubspace (infixr "⊗⇩S" 70) where
  ‹tensor_ccsubspace A B = ccspan {ψ ⊗⇩s φ | ψ φ. ψ ∈ space_as_set A ∧ φ ∈ space_as_set B}›

lemma tensor_ccsubspace_via_Proj: ‹A ⊗⇩S B = (Proj A ⊗⇩o Proj B) *⇩S ⊤›
proof (rule antisym)
  have ‹ψ ⊗⇩s φ ∈ space_as_set ((Proj A ⊗⇩o Proj B) *⇩S ⊤)› if ‹ψ ∈ space_as_set A› and ‹φ ∈ space_as_set B› for ψ φ
    by (metis Proj_fixes_image cblinfun_apply_in_image tensor_op_ell2 that(1) that(2))
  then show ‹A ⊗⇩S B ≤ (Proj A ⊗⇩o Proj B) *⇩S ⊤›
    by (auto intro!: ccspan_leqI simp: tensor_ccsubspace_def)
  have *: ‹ccspan {ψ ⊗⇩s φ | (ψ::'a ell2) (φ::'b ell2). True} = ⊤›
    using tensor_ell2_dense'[where A=‹UNIV :: 'a ell2 set› and B=‹UNIV :: 'b ell2 set›]
    by auto
  have ‹(Proj A ⊗⇩o Proj B) *⇩V ψ ⊗⇩s φ ∈ space_as_set (A ⊗⇩S B)› for ψ φ
    unfolding tensor_op_ell2 tensor_ccsubspace_def
    by (smt (verit) Proj_range cblinfun_apply_in_image ccspan_superset mem_Collect_eq subsetD)
  then show ‹(Proj A ⊗⇩o Proj B) *⇩S ⊤ ≤ A ⊗⇩S B›
    by (auto intro!: ccspan_leqI simp: cblinfun_image_ccspan simp flip: *)
qed

lemma tensor_ccsubspace_top[simp]: ‹⊤ ⊗⇩S ⊤ = ⊤›
  by (simp add: tensor_ccsubspace_via_Proj)

lemma tensor_ccsubspace_0_left[simp]: ‹0 ⊗⇩S X = 0›
  by (simp add: tensor_ccsubspace_via_Proj)

lemma tensor_ccsubspace_0_right[simp]: ‹X ⊗⇩S 0 = 0›
  by (simp add: tensor_ccsubspace_via_Proj)


lemma tensor_ccsubspace_image: ‹(A *⇩S T) ⊗⇩S (B *⇩S U) = (A ⊗⇩o B) *⇩S (T ⊗⇩S U)›
proof -
  have ‹(A *⇩S T) ⊗⇩S (B *⇩S U) = ccspan ((λ(ψ, φ). ψ ⊗⇩s φ) ` (space_as_set (A *⇩S T) × space_as_set (B *⇩S U)))›
    by (simp add: tensor_ccsubspace_def set_compr_2_image_collect ccspan.rep_eq)
  also have ‹… = ccspan ((λ(ψ, φ). ψ ⊗⇩s φ) ` closure ((A ` space_as_set T) × (B ` space_as_set U)))›
    by (simp add: cblinfun_image.rep_eq closure_Times)
  also have ‹… = ccspan (closure ((λ(ψ, φ). ψ ⊗⇩s φ) ` ((A ` space_as_set T) × (B ` space_as_set U))))›
    by (subst closure_image_closure[symmetric])
       (use continuous_on_subset continuous_tensor_ell2 in auto)
  also have ‹… = ccspan ((λ(ψ, φ). ψ ⊗⇩s φ) ` ((A ` space_as_set T) × (B ` space_as_set U)))›
    by simp
  also have ‹… = (A ⊗⇩o B) *⇩S ccspan ((λ(ψ, φ). ψ ⊗⇩s φ) ` (space_as_set T × space_as_set U))›
    by (simp add: cblinfun_image_ccspan image_image tensor_op_ell2 case_prod_beta
        flip: map_prod_image)
  also have ‹… = (A ⊗⇩o B) *⇩S (T ⊗⇩S U)›
    by (simp add: tensor_ccsubspace_def set_compr_2_image_collect)
  finally show ?thesis
    by -
qed

lemma tensor_ccsubspace_bot_left[simp]: ‹⊥ ⊗⇩S S = ⊥›
  by (simp add: tensor_ccsubspace_via_Proj)
lemma tensor_ccsubspace_bot_right[simp]: ‹S ⊗⇩S ⊥ = ⊥›
  by (simp add: tensor_ccsubspace_via_Proj)

lemma swap_ell2_tensor_ccsubspace: ‹swap_ell2 *⇩S (S ⊗⇩S T) = T ⊗⇩S S›
  by (force intro!: arg_cong[where f=ccspan] 
            simp add: tensor_ccsubspace_def cblinfun_image_ccspan image_image set_compr_2_image_collect)

lemma tensor_ccsubspace_right1dim_member:
  assumes ‹ψ ∈ space_as_set (S ⊗⇩S ccspan{φ})›
  shows ‹∃ψ'. ψ = ψ' ⊗⇩s φ›
proof (cases ‹φ = 0›)
  case True
  with assms show ?thesis 
    by simp
next
  case False
  have ‹{ψ ⊗⇩s φ' |ψ φ'. ψ ∈ space_as_set S ∧ φ' ∈ space_as_set (ccspan {φ})}
    = {ψ ⊗⇩s φ | ψ. ψ ∈ space_as_set S}›
  proof -
    have ‹ψ ∈ space_as_set S ⟹ ∃ψ'. ψ ⊗⇩s c *⇩C φ = ψ' ⊗⇩s φ ∧ ψ' ∈ space_as_set S› for c ψ
      by (rule exI[where x=‹c *⇩C ψ›])
         (auto simp: tensor_ell2_scaleC2 tensor_ell2_scaleC1
            complex_vector.subspace_scale)
    moreover have ‹ψ ∈ space_as_set S ⟹
         ∃ψ' φ'. ψ ⊗⇩s φ = ψ' ⊗⇩s φ' ∧ ψ' ∈ space_as_set S ∧ φ' ∈ range (λk. k *⇩C φ)› for ψ
      by (rule exI[where x=ψ], rule exI[where x=φ])
         (auto intro!: range_eqI[where x=‹1::complex›])
    ultimately show ?thesis
      by (auto simp: ccspan_finite complex_vector.span_singleton)
  qed
  moreover have ‹csubspace {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
  proof (rule complex_vector.subspaceI)
    show ‹0 ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
      by (auto intro!: exI[where x=0])
    show ‹x + y ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
      if x: ‹x ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
      and y: ‹y ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}› for x y
      using that complex_vector.subspace_add tensor_ell2_add1
      unfolding mem_Collect_eq by (metis csubspace_space_as_set)
    show ‹c *⇩C x ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
      if x: ‹x ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}› for c x
      using that complex_vector.subspace_scale tensor_ell2_scaleC2 tensor_ell2_scaleC1
      unfolding mem_Collect_eq by (metis csubspace_space_as_set)
  qed
  moreover have ‹closed {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
  proof (rule closed_sequential_limits[THEN iffD2, rule_format])
    fix x l
    assume asm: ‹(∀n. x n ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}) ∧ x ⇢ l›
    then obtain ψ' where x_def: ‹x n = ψ' n ⊗⇩s φ› and ψ'_S: ‹ψ' n ∈ space_as_set S› for n
      unfolding mem_Collect_eq by metis
    from asm have ‹x ⇢ l›
      by simp
    have ‹Cauchy ψ'›
    proof (rule CauchyI)
      fix e :: real assume ‹e > 0›
      define d where ‹d = e * norm φ›
      with False ‹e > 0› have ‹d > 0›
        by auto
      from ‹x ⇢ l›
      have ‹Cauchy x›
        using LIMSEQ_imp_Cauchy by blast
      then obtain M where ‹∀m≥M. ∀n≥M. norm (x m - x n) < d›
        using Cauchy_iff ‹0 < d› by blast
      then show ‹∃M. ∀m≥M. ∀n≥M. norm (ψ' m - ψ' n) < e›
        by (intro exI[of _ M])
           (use False in ‹auto simp add: x_def norm_tensor_ell2 d_def simp flip: tensor_ell2_diff1›)
    qed
    then obtain l' where ‹ψ' ⇢ l'›
      using convergent_eq_Cauchy by blast
    with ψ'_S have l'_S: ‹l' ∈ space_as_set S›
      by (metis ‹Cauchy ψ'› completeE complete_space_as_set limI)
    from ‹ψ' ⇢ l'› have ‹x ⇢ l' ⊗⇩s φ›
      by (auto intro: tendsto_eq_intros simp: x_def[abs_def])
    with ‹x ⇢ l› have ‹l = l' ⊗⇩s φ›
      using LIMSEQ_unique by blast
    then show ‹l ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
      using l'_S by auto
  qed
  ultimately have ‹space_as_set (ccspan {ψ ⊗⇩s φ' |ψ φ'. ψ ∈ space_as_set S ∧ φ' ∈ space_as_set (ccspan {φ})})
      = {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}› 
    by (simp add: ccspan.rep_eq complex_vector.span_eq_iff[THEN iffD2])
  with assms have ‹ψ ∈ {ψ ⊗⇩s φ |ψ. ψ ∈ space_as_set S}›
    by (simp add: tensor_ccsubspace_def)
  then show ‹∃ψ'. ψ = ψ' ⊗⇩s φ›
    by auto
qed

lemma tensor_ccsubspace_left1dim_member:
  assumes ‹ψ ∈ space_as_set (ccspan{φ} ⊗⇩S S)›
  shows ‹∃ψ'. ψ = φ ⊗⇩s ψ'›
proof -
  from assms 
  have ‹swap_ell2 *⇩V ψ ∈ space_as_set (swap_ell2 *⇩S (ccspan {φ} ⊗⇩S S))›
  by (metis rev_image_eqI space_as_set_image_commute swap_ell2_selfinv)
  then have ‹swap_ell2 ψ ∈ space_as_set (S ⊗⇩S ccspan{φ})›
    by (simp add: swap_ell2_tensor_ccsubspace)
  then obtain ψ' where ψ': ‹swap_ell2 ψ = ψ' ⊗⇩s φ›
    using tensor_ccsubspace_right1dim_member by blast
  have ‹ψ = swap_ell2 *⇩V swap_ell2 *⇩V ψ›
    by (simp flip: cblinfun_apply_cblinfun_compose)
  also have ‹… = swap_ell2 *⇩V (ψ' ⊗⇩s φ)›
    by (simp add: ψ')
  also have ‹… = φ ⊗⇩s ψ'›
    by simp
  finally show ?thesis
    by auto
qed

lemma tensor_ell2_mem_tensor_ccsubspace_left:
  assumes ‹a ⊗⇩s b ∈ space_as_set (S ⊗⇩S T)› and ‹b ≠ 0›
  shows ‹a ∈ space_as_set S›
proof (cases ‹a = 0›)
  case True
  then show ?thesis 
    by simp
next
  case False
  have ‹norm (Proj S a) * norm (Proj T b) = norm ((Proj S a) ⊗⇩s (Proj T b))›
    by (simp add: norm_tensor_ell2)
  also have ‹… = norm (Proj (S ⊗⇩S T) (a ⊗⇩s b))›
    by (simp add: tensor_ccsubspace_via_Proj Proj_on_own_range is_Proj_tensor_op
        tensor_op_ell2)
  also from assms have ‹… = norm (a ⊗⇩s b)›
    by (simp add: Proj_fixes_image)
  also have ‹… = norm a * norm b›
    by (simp add: norm_tensor_ell2)
  finally have prod_eq: ‹norm (Proj S *⇩V a) * norm (Proj T *⇩V b) = norm a * norm b›
    by -
  with False ‹b ≠ 0› have Tb_non0: ‹norm (Proj T *⇩V b) ≠ 0›
    by fastforce
  have ‹norm (Proj S a) = norm a›
  proof (rule ccontr)
    assume asm: ‹norm (Proj S *⇩V a) ≠ norm a›
    have Sa_leq: ‹norm (Proj S *⇩V a) ≤ norm a›
      by (simp add: is_Proj_reduces_norm)
    have Tb_leq: ‹norm (Proj T *⇩V b) ≤ norm b›
      by (simp add: is_Proj_reduces_norm)
    from asm Sa_leq have ‹norm (Proj S *⇩V a) < norm a›
      by simp
    then have ‹norm (Proj S *⇩V a) * norm (Proj T *⇩V b) < norm a * norm (Proj T *⇩V b)›
      using Tb_non0 by auto
    also from Tb_leq have ‹… ≤ norm a * norm b›
      using False by force
    also note prod_eq
    finally show False
      by simp
  qed
  then show ‹a ∈ space_as_set S›
    using norm_Proj_apply by blast
qed

lemma tensor_ell2_mem_tensor_ccsubspace_right:
  assumes ‹a ⊗⇩s b ∈ space_as_set (S ⊗⇩S T)› and ‹a ≠ 0›
  shows ‹b ∈ space_as_set T›
proof -
  have ‹swap_ell2 *⇩V (a ⊗⇩s b) ∈ space_as_set (swap_ell2 *⇩S (S ⊗⇩S T))›
    using assms(1) cblinfun_apply_in_image' by blast
  then have ‹b ⊗⇩s a ∈ space_as_set (T ⊗⇩S S)›
    by (simp add: swap_ell2_tensor_ccsubspace)
  then show ‹b ∈ space_as_set T›
    using ‹a ≠ 0› by (rule tensor_ell2_mem_tensor_ccsubspace_left)
qed

lemma tensor_ell2_in_tensor_ccsubspace: ‹a ⊗⇩s b ∈ space_as_set (A ⊗⇩S B)› if ‹a ∈ space_as_set A› and ‹b ∈ space_as_set B›
  ― ‹Converse is @{thm [source] tensor_ell2_mem_tensor_ccsubspace_left} and ‹…_right›.›
  using that by (auto intro!: ccspan_superset[THEN subsetD] simp add: tensor_ccsubspace_def)

lemma tensor_ccsubspace_INF_left_top:
  fixes S :: ‹'a ⇒ 'b ell2 ccsubspace›
  shows ‹(INF x∈X. S x) ⊗⇩S (⊤::'c ell2 ccsubspace) = (INF x∈X. S x ⊗⇩S ⊤)›
proof (rule antisym[rotated])
  let ?top = ‹⊤ :: 'c ell2 ccsubspace›
  have *: ‹ψ ⊗⇩s φ ∈ space_as_set (⨅x∈X. S x ⊗⇩S ?top)›
    if ‹ψ ∈ space_as_set (⨅x∈X. S x)› for ψ φ
  proof -
    from that(1) have ‹ψ ∈ space_as_set (S x)› if ‹x ∈ X› for x
      using that by (simp add: Inf_ccsubspace.rep_eq)
    then have ‹ψ ⊗⇩s φ ∈ space_as_set (S x ⊗⇩S ⊤)› if ‹x ∈ X› for x
      using ccspan_superset that by (force simp: tensor_ccsubspace_def)
    then show ?thesis
      by (simp add: Inf_ccsubspace.rep_eq)
  qed
  show ‹(INF x∈X. S x) ⊗⇩S ?top ≤ (INF x∈X. S x ⊗⇩S ?top)›
    by (subst tensor_ccsubspace_def, rule ccspan_leqI) (use * in auto)

  show ‹(⨅x∈X. S x ⊗⇩S ?top) ≤ (⨅x∈X. S x) ⊗⇩S ?top›
  proof (rule ccsubspace_leI_unit)
    fix ψ
    assume asm: ‹ψ ∈ space_as_set (⨅x∈X. S x ⊗⇩S ?top)›
    obtain ψ' where ψ'b_b: ‹ψ' b ⊗⇩s ket b = (id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) *⇩V ψ› for b
    proof (atomize_elim, rule choice, intro allI)
      fix b :: 'c
      have ‹(id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) *⇩V ψ ∈ space_as_set (⊤ ⊗⇩S ccspan {ket b})›
        by (simp add: butterfly_eq_proj tensor_ccsubspace_via_Proj)
      then show ‹∃ψ'. ψ' ⊗⇩s ket b = (id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) *⇩V ψ›
       by (metis tensor_ccsubspace_right1dim_member)
    qed
  
    have ‹ψ' b ∈ space_as_set (S x)› if ‹x ∈ X› for x b
    proof -
      from asm have ψ_ST: ‹ψ ∈ space_as_set (S x ⊗⇩S ?top)›
        by (meson INF_lower Set.basic_monos(7) less_eq_ccsubspace.rep_eq that)
      have ‹ψ' b ⊗⇩s ket b = (id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) *⇩V ψ›
        by (simp add: ψ'b_b)
      also from ψ_ST
      have ‹… ∈ space_as_set (((id_cblinfun ⊗⇩o butterfly (ket b) (ket b))) *⇩S (S x ⊗⇩S ?top))›
        by (meson cblinfun_apply_in_image')
      also have ‹… = space_as_set (((id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) o⇩C⇩L (Proj (S x) ⊗⇩o id_cblinfun)) *⇩S ⊤)›
        by (simp add: cblinfun_compose_image tensor_ccsubspace_via_Proj)
      also have ‹… = space_as_set ((Proj (S x) ⊗⇩o (butterfly (ket b) (ket b) o⇩C⇩L id_cblinfun)) *⇩S ⊤)›
        by (simp add: comp_tensor_op)
      also have ‹… = space_as_set ((Proj (S x) ⊗⇩o (id_cblinfun o⇩C⇩L butterfly (ket b) (ket b))) *⇩S ⊤)›
        by simp
      also have ‹… = space_as_set (((Proj (S x) ⊗⇩o id_cblinfun) o⇩C⇩L (id_cblinfun ⊗⇩o butterfly (ket b) (ket b))) *⇩S ⊤)›
        by (simp add: comp_tensor_op)
      also have ‹… ⊆ space_as_set ((Proj (S x) ⊗⇩o id_cblinfun) *⇩S ⊤)›
        by (metis cblinfun_compose_image cblinfun_image_mono less_eq_ccsubspace.rep_eq top_greatest)
      also have ‹… = space_as_set (S x ⊗⇩S ?top)›
        by (simp add: tensor_ccsubspace_via_Proj)
      finally have ‹ψ' b ⊗⇩s ket b ∈ space_as_set (S x ⊗⇩S ?top)›
        by -
      then show ‹ψ' b ∈ space_as_set (S x)›
        using tensor_ell2_mem_tensor_ccsubspace_left
        by (metis ket_nonzero)
    qed

    then have ‹ψ' b ∈ space_as_set (⨅x∈X. S x)› if ‹x ∈ X› for x b
      using that by (simp add: Inf_ccsubspace.rep_eq)

    then have *: ‹ψ' b ⊗⇩s ket b ∈ space_as_set ((⨅x∈X. S x) ⊗⇩S ?top)› for b
      by (auto intro!: ccspan_superset[THEN set_mp] 
          simp add: tensor_ccsubspace_def Inf_ccsubspace.rep_eq)
    
    have ‹ψ ∈ space_as_set (ccspan (range (λb. ψ' b ⊗⇩s ket b)))› (is ‹ψ ∈ ?rhs›)
    proof -
      define γ where ‹γ F = (∑b∈F. (id_cblinfun ⊗⇩o butterfly (ket b) (ket b)) *⇩V ψ)› for F
      have γ_rhs: ‹γ F ∈ ?rhs› for F
        using ccspan_superset  by (force intro!: complex_vector.subspace_sum simp add: γ_def ψ'b_b)
      have γ_trunc: ‹γ F = trunc_ell2 (UNIV × F) ψ› if ‹finite F› for F
      proof (rule cinner_ket_eqI)
        fix x :: ‹'b × 'c› obtain x1 x2 where x_def: ‹x = (x1,x2)›
          by force
        have *: ‹ket x ∙⇩C ((id_cblinfun ⊗⇩o butterfly (ket j) (ket j)) *⇩V ψ) = of_bool (j=x2) * Rep_ell2 ψ x› for j
          apply (simp add: x_def tensor_op_ell2 tensor_op_adjoint cinner_ket 
              flip: tensor_ell2_ket cinner_adj_left)
          by (simp add: tensor_ell2_ket cinner_ket_left)
        have ‹ket x ∙⇩C γ F = of_bool (x2∈F) *⇩C Rep_ell2 ψ x›
          using that
          apply (simp add: x_def γ_def complex_vector.linear_sum[of ‹cinner _›] bounded_clinear_cinner_right 
              bounded_clinear.clinear sum_single[where i=x2] tensor_op_adjoint tensor_op_ell2 cinner_ket
              flip: tensor_ell2_ket cinner_adj_left)
          by (simp add: tensor_ell2_ket cinner_ket_left)
        moreover have ‹ket x ∙⇩C trunc_ell2 (UNIV × F) ψ = of_bool (x2∈F) *⇩C Rep_ell2 ψ x›
          by (simp add: trunc_ell2.rep_eq cinner_ket_left x_def)
        ultimately show ‹ket x ∙⇩C γ F = ket x ∙⇩C trunc_ell2 (UNIV × F) ψ›
          by simp
      qed
      have ‹(γ ⤏ ψ) (finite_subsets_at_top UNIV)›
      proof (rule tendsto_iff[THEN iffD2, rule_format])
        fix e :: real assume ‹e > 0›
        from trunc_ell2_lim_at_UNIV[of ψ]
        have ‹∀⇩F F in finite_subsets_at_top UNIV. dist (trunc_ell2 F ψ) ψ < e›
          by (simp add: ‹0 < e› tendstoD)
        then obtain M where ‹finite M› and less_e: ‹finite F ⟹ F ⊇ M ⟹ dist (trunc_ell2 F ψ) ψ < e› for F
          by (metis (mono_tags, lifting) eventually_finite_subsets_at_top subset_UNIV)
        define M' where ‹M' = snd ` M›
        have ‹finite M'›
          using M'_def ‹finite M› by blast
        have ‹dist (γ F') ψ < e› if ‹finite F'› and ‹F' ⊇ M'› for F'
        proof -
          have ‹dist (γ F') ψ = norm (trunc_ell2 (- (UNIV × F')) ψ)›
            using that by (simp only: γ_trunc dist_norm trunc_ell2_uminus norm_minus_commute)
          also have ‹… ≤ norm (trunc_ell2 (- ((fst ` M) × F')) ψ)›
            by (meson Compl_anti_mono Set.basic_monos(1) Sigma_mono subset_UNIV trunc_ell2_norm_mono)
          also have ‹… = dist (trunc_ell2 ((fst ` M) × F') ψ) ψ›
            apply (simp add: trunc_ell2_uminus dist_norm)
            using norm_minus_commute by blast
          also have ‹… < e›
            apply (rule less_e)
            subgoal
              using ‹finite F'› ‹finite M› by force
            subgoal
              using ‹F' ⊇ M'› M'_def by force
            done
          finally show ?thesis
            by -
        qed
        then show ‹∀⇩F F' in finite_subsets_at_top UNIV. dist (γ F') ψ < e›
          using ‹finite M'› by (auto simp add: eventually_finite_subsets_at_top)
      qed
      then show ‹ψ ∈ ?rhs›
        by (rule Lim_in_closed_set[rotated -1]) (use γ_rhs in auto)
    qed
    also from * have ‹… ⊆ space_as_set ((⨅x∈X. S x) ⊗⇩S ?top)›
      by (meson ccspan_leqI image_subset_iff less_eq_ccsubspace.rep_eq)
    
    finally show ‹ψ ∈ space_as_set ((⨅x∈X. S x) ⊗⇩S ?top)›
      by -
  qed
qed

lemma tensor_ccsubspace_INF_right_top:
  fixes S :: ‹'a ⇒ 'b ell2 ccsubspace›
  shows ‹(⊤::'c ell2 ccsubspace) ⊗⇩S (INF x∈X. S x) = (INF x∈X. ⊤ ⊗⇩S S x)›
proof -
  have ‹(INF x∈X. S x) ⊗⇩S (⊤::'c ell2 ccsubspace) = (INF x∈X. S x ⊗⇩S ⊤)›
    by (rule tensor_ccsubspace_INF_left_top)
  then have ‹swap_ell2 *⇩S ((INF x∈X. S x) ⊗⇩S (⊤::'c ell2 ccsubspace)) = swap_ell2 *⇩S (INF x∈X. S x ⊗⇩S ⊤)›
    by simp
  then show ?thesis
    by (cases ‹X = {}›)
       (simp_all add: swap_ell2_tensor_ccsubspace)
qed

lemma tensor_ccsubspace_INF_left: ‹(INF x∈X. S x) ⊗⇩S T = (INF x∈X. S x ⊗⇩S T)› if ‹X ≠ {}›
proof (cases ‹T=0›)
  case True
  then show ?thesis 
    using that by simp
next
  case False
  from ccsubspace_as_whole_type[OF False]
  have ‹let 't::type = some_onb_of T in
        (INF x∈X. S x) ⊗⇩S T = (INF x∈X. S x ⊗⇩S T)›
  proof with_type_mp
    with_type_case
    from with_type_mp.premise
    obtain U :: ‹'t ell2 ⇒⇩C⇩L 'c ell2› where [simp]: ‹isometry U› and imU: ‹U *⇩S ⊤ = T›
      by auto
    have ‹(id_cblinfun ⊗⇩o U) *⇩S ((⨅x∈X. S x) ⊗⇩S ⊤) = (id_cblinfun ⊗⇩o U) *⇩S (⨅x∈X. S x ⊗⇩S ⊤)›
      by (rule arg_cong[where f=‹λx. _ *⇩S x›], rule tensor_ccsubspace_INF_left_top)
    then show ‹(⨅x∈X. S x) ⊗⇩S T = (⨅x∈X. S x ⊗⇩S T)›
      using that by (simp add: imU flip: tensor_ccsubspace_image)
  qed
  from this[cancel_with_type]
  show ?thesis
    by -
qed

lemma tensor_ccsubspace_INF_right: ‹(INF x∈X. T ⊗⇩S S x) = (INF x∈X. T ⊗⇩S S x)› if ‹X ≠ {}›
proof -
  from that have ‹(INF x∈X. S x) ⊗⇩S T = (INF x∈X. S x ⊗⇩S T)›
    by (rule tensor_ccsubspace_INF_left)
  then have ‹swap_ell2 *⇩S ((INF x∈X. S x) ⊗⇩S T) = swap_ell2 *⇩S (INF x∈X. S x ⊗⇩S T)›
    by simp
  then show ?thesis
    by (cases ‹X = {}›)
       (simp_all add: swap_ell2_tensor_ccsubspace)
qed

lemma tensor_ccsubspace_ccspan: ‹ccspan X ⊗⇩S ccspan Y = ccspan {x ⊗⇩s y | x y. x ∈ X ∧ y ∈ Y}›
proof (rule antisym)
  show ‹ccspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y} ≤ ccspan X ⊗⇩S ccspan Y›
    using ccspan_superset[of X] ccspan_superset[of Y]
    by (auto intro!: ccspan_mono Collect_mono ex_mono simp add: tensor_ccsubspace_def)
next
  have ‹{ψ ⊗⇩s φ |ψ φ. ψ ∈ space_as_set (ccspan X) ∧ φ ∈ space_as_set (ccspan Y)}
       ⊆ closure {x ⊗⇩s y |x y. x ∈ cspan X ∧ y ∈ cspan Y}›
  proof (rule subsetI)
    fix γ
    assume ‹γ ∈ {ψ ⊗⇩s φ |ψ φ. ψ ∈ space_as_set (ccspan X) ∧ φ ∈ space_as_set (ccspan Y)}›
    then obtain ψ φ where ψ: ‹ψ ∈ space_as_set (ccspan X)› and φ: ‹φ ∈ space_as_set (ccspan Y)› and γ_def: ‹γ = ψ ⊗⇩s φ›
      by blast
    from ψ
    obtain ψ' where lim1: ‹ψ' ⇢ ψ› and ψ'X: ‹ψ' n ∈ cspan X› for n
      using closure_sequential unfolding ccspan.rep_eq by blast
    from φ
    obtain φ' where lim2: ‹φ' ⇢ φ› and φ'Y: ‹φ' n ∈ cspan Y› for n
      using closure_sequential unfolding ccspan.rep_eq by blast
    interpret tensor: bounded_cbilinear tensor_ell2
      by (rule bounded_cbilinear_tensor_ell2)
    from lim1 lim2 have ‹(λn. ψ' n ⊗⇩s φ' n) ⇢ ψ ⊗⇩s φ›
      by (rule tensor.tendsto)
    moreover have ‹ψ' n ⊗⇩s φ' n ∈ {x ⊗⇩s y |x y. x ∈ cspan X ∧ y ∈ cspan Y}› for n
      using ψ'X φ'Y by auto
    ultimately show ‹γ ∈ closure {x ⊗⇩s y |x y. x ∈ cspan X ∧ y ∈ cspan Y}›
      unfolding γ_def
      by (meson closure_sequential)
  qed
  also have ‹closure {x ⊗⇩s y |x y. x ∈ cspan X ∧ y ∈ cspan Y}
          ⊆ closure (cspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y})›
  proof (intro closure_mono subsetI)
    fix γ
    assume ‹γ ∈ {x ⊗⇩s y |x y. x ∈ cspan X ∧ y ∈ cspan Y}›
    then obtain x y where γ_def: ‹γ = x ⊗⇩s y› and ‹x ∈ cspan X› and ‹y ∈ cspan Y›
      by blast
    from ‹x ∈ cspan X›
    obtain X' x' where ‹finite X'› and ‹X' ⊆ X› and x_def: ‹x = (∑i∈X'. x' i *⇩C i)›
      using complex_vector.span_explicit[of X] by auto
    from ‹y ∈ cspan Y›
    obtain Y' y' where ‹finite Y'› and ‹Y' ⊆ Y› and y_def: ‹y = (∑j∈Y'. y' j *⇩C j)›
      using complex_vector.span_explicit[of Y] by auto
    from x_def y_def γ_def
    have ‹γ = (∑i∈X'. x' i *⇩C i) ⊗⇩s (∑j∈Y'. y' j *⇩C j)›
      by simp
    also have ‹… = (∑i∈X'. ∑j∈Y'. (x' i *⇩C i) ⊗⇩s (y' j *⇩C j))›
      by (smt (verit) sum.cong tensor_ell2_sum_left tensor_ell2_sum_right)
    also have ‹… = (∑i∈X'. ∑j∈Y'. (x' i * y' j) *⇩C (i ⊗⇩s j))›
      by (metis (no_types, lifting) scaleC_scaleC sum.cong tensor_ell2_scaleC1 tensor_ell2_scaleC2)
    also have ‹… ∈ cspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y}›
      using ‹X' ⊆ X› ‹Y' ⊆ Y›
      by (auto intro!: complex_vector.span_sum complex_vector.span_scale
          complex_vector.span_base[of ‹_ ⊗⇩s _›])
    finally show ‹γ ∈ cspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y}›
      by -
  qed
  also have ‹… = space_as_set (ccspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y})›
    using ccspan.rep_eq by blast
  finally show ‹ccspan X ⊗⇩S ccspan Y ≤ ccspan {x ⊗⇩s y |x y. x ∈ X ∧ y ∈ Y}›
    by (auto intro!: ccspan_leqI simp add: tensor_ccsubspace_def)
qed

lemma tensor_ccsubspace_mono: ‹A ⊗⇩S B ≤ C ⊗⇩S D› if ‹A ≤ C› and ‹B ≤ D›
  apply (auto intro!: ccspan_mono simp add: tensor_ccsubspace_def)
  using that
  by (auto simp add: less_eq_ccsubspace_def)

lemma tensor_ccsubspace_element_as_infsum:
  fixes A :: ‹'a ell2 ccsubspace› and B :: ‹'b ell2 ccsubspace›
  assumes ‹ψ ∈ space_as_set (A ⊗⇩S B)›
  shows ‹∃φ δ. (∀n::nat. φ n ∈ space_as_set A) ∧ (∀n. δ n ∈ space_as_set B)
       ∧ ((λn. φ n ⊗⇩s δ n) has_sum ψ) UNIV›
proof -
  obtain A' where spanA': ‹ccspan A' = A› and orthoA': ‹is_ortho_set A'› and normA': ‹a ∈ A' ⟹ norm a = 1› for a
    using some_onb_of_ccspan some_onb_of_is_ortho_set some_onb_of_norm1
    by blast
  obtain B' where spanB': ‹ccspan B' = B› and orthoB': ‹is_ortho_set B'› and normB': ‹b ∈ B' ⟹ norm b = 1› for b
    using some_onb_of_ccspan some_onb_of_is_ortho_set some_onb_of_norm1
    by blast
  define AB' where ‹AB' = {a ⊗⇩s b | a b. a ∈ A' ∧ b ∈ B'}›
  define ABnon0 where ‹ABnon0 = {ab ∈ AB'. (ab ∙⇩C ψ) *⇩C ab ≠ 0}›
  have ABnon0_def': ‹ABnon0 = {ab ∈ AB'. (norm (ab ∙⇩C ψ))⇧2 ≠ 0}›
    by (auto simp: ABnon0_def)
  have ‹is_ortho_set AB'›
    by (simp add: AB'_def orthoA' orthoB' tensor_ell2_is_ortho_set)
  have normAB': ‹ab ∈ AB' ⟹ norm ab = 1› for ab
    by (auto simp add: AB'_def norm_tensor_ell2 normA' normB')
  have spanAB': ‹ccspan AB' = A ⊗⇩S B›
    by (simp add: tensor_ccsubspace_ccspan AB'_def flip: spanA' spanB')
  have sum1: ‹((λab. (ab ∙⇩C ψ) *⇩C ab) has_sum ψ) AB'›
    apply (rule basis_projections_reconstruct_has_sum)
    by (simp_all add: spanAB' ‹is_ortho_set AB'› normAB' assms)
  have ‹(λab. (norm (ab ∙⇩C ψ))⇧2) summable_on AB'›
    by (rule parseval_identity_summable)
       (simp_all add: spanAB' ‹is_ortho_set AB'› normAB' assms)
  then have ‹countable ABnon0›
    using ABnon0_def' summable_countable_real by blast
  obtain f and N :: ‹nat set› where bij_f: ‹bij_betw f N ABnon0›
    using ‹countable ABnon0› countableE_bij by blast
  then obtain φ0 δ0 where f_def: ‹f n = φ0 n ⊗⇩s δ0 n› and φ0A': ‹φ0 n ∈ A'› and δ0B': ‹δ0 n ∈ B'› if ‹n ∈ N› for n
    apply atomize_elim 
    apply (subst all_conj_distrib[symmetric] choice_iff[symmetric])+
    apply (simp add: bij_betw_def ABnon0_def)
    using AB'_def ‹bij_betw f N ABnon0› bij_betwE mem_Collect_eq by blast
  define c where ‹c n = (φ0 n ⊗⇩s δ0 n) ∙⇩C ψ› for n
  from sum1 have ‹((λab. (ab ∙⇩C ψ) *⇩C ab) has_sum ψ) ABnon0›
    by (rule has_sum_cong_neutral[THEN iffD1, rotated -1]) (auto simp: ABnon0_def)
  then have ‹((λn. (f n ∙⇩C ψ) *⇩C f n) has_sum ψ) N›
    by (rule has_sum_reindex_bij_betw[OF bij_f, THEN iffD2])
  then have sum2: ‹((λn. c n *⇩C (φ0 n ⊗⇩s δ0 n)) has_sum ψ) N›
    by (rule has_sum_cong[THEN iffD1, rotated]) (simp add: f_def c_def)
  define φ δ where ‹φ n = (if n∈N then c n *⇩C φ0 n else 0)› and ‹δ n = (if n∈N then δ0 n else 0)› for n
  then have 1: ‹φ n ∈ space_as_set A› and 2: ‹δ n ∈ space_as_set B› for n
    using φ0A' δ0B' spanA' spanB' ccspan_superset 
    by (auto intro!: complex_vector.subspace_scale simp: φ_def δ_def)
  from sum2 have sum3: ‹((λn. φ n ⊗⇩s δ n) has_sum ψ) UNIV›
    by (rule has_sum_cong_neutral[THEN iffD2, rotated -1])
       (auto simp: φ_def δ_def tensor_ell2_scaleC1)
  from 1 2 sum3 show ?thesis
    by auto
qed

lemma ortho_tensor_ccsubspace_right: ‹- (⊤ ⊗⇩S A) = ⊤ ⊗⇩S (- A)›
proof -
  have [simp]: ‹is_Proj (id_cblinfun ⊗⇩o Proj X)› for X
    by (metis Proj_is_Proj Proj_top is_Proj_tensor_op)
  
  have ‹Proj (- (⊤ ⊗⇩S A)) = id_cblinfun - Proj (⊤ ⊗⇩S A)›
    by (simp add: Proj_ortho_compl)
  also have ‹… = id_cblinfun - (id_cblinfun ⊗⇩o Proj A)›
    by (simp add: tensor_ccsubspace_via_Proj Proj_on_own_range)
  also have ‹… = id_cblinfun ⊗⇩o (id_cblinfun - Proj A)›
    by (metis cblinfun.diff_right left_amplification.rep_eq tensor_id)
  also have ‹… = Proj ⊤ ⊗⇩o Proj (- A)›
    by (simp add: Proj_ortho_compl)
  also have ‹… = Proj (⊤ ⊗⇩S (- A))›
    by (simp add: tensor_ccsubspace_via_Proj Proj_on_own_range)
  finally show ?thesis
    using Proj_inj by blast
qed

lemma ortho_tensor_ccsubspace_left: ‹- (A ⊗⇩S ⊤) = (- A) ⊗⇩S ⊤›
proof -
  have ‹- (A ⊗⇩S ⊤) = swap_ell2 *⇩S (- (⊤ ⊗⇩S A))›
    by (simp add: unitary_image_ortho_compl swap_ell2_tensor_ccsubspace)
  also have ‹… = swap_ell2 *⇩S (⊤ ⊗⇩S (- A))›
    by (simp add: ortho_tensor_ccsubspace_right)
  also have ‹… = (- A) ⊗⇩S ⊤›
    by (simp add: swap_ell2_tensor_ccsubspace)
  finally show ?thesis
    by -
qed

lemma kernel_tensor_id_left: ‹kernel (id_cblinfun ⊗⇩o A) = ⊤ ⊗⇩S kernel A›
proof -
  have ‹kernel (id_cblinfun ⊗⇩o A) = - ((id_cblinfun ⊗⇩o A)* *⇩S ⊤)›
    by (rule kernel_compl_adj_range)
  also have ‹… = - (id_cblinfun *⇩S ⊤ ⊗⇩S A* *⇩S ⊤)›
    by (metis cblinfun_image_id id_cblinfun_adjoint tensor_ccsubspace_image tensor_ccsubspace_top tensor_op_adjoint)
  also have ‹… = ⊤ ⊗⇩S (- (A* *⇩S ⊤))›
    by (simp add: ortho_tensor_ccsubspace_right)
  also have ‹… = ⊤ ⊗⇩S kernel A›
    by (simp add: kernel_compl_adj_range)
  finally show ?thesis
    by -
qed

lemma kernel_tensor_id_right: ‹kernel (A ⊗⇩o id_cblinfun) = kernel A ⊗⇩S ⊤›
proof -
  have ker_swap: ‹kernel swap_ell2 = 0›
    by (simp add: kernel_isometry)
  have ‹kernel (id_cblinfun ⊗⇩o A) = ⊤ ⊗⇩S kernel A›
    by (rule kernel_tensor_id_left)
  from this[THEN arg_cong, of ‹cblinfun_image swap_ell2›]
  show ?thesis
    by (simp add: swap_ell2_tensor_ccsubspace cblinfun_image_kernel_unitary
        flip: swap_ell2_commute_tensor_op kernel_cblinfun_compose[OF ker_swap])
qed


lemma eigenspace_tensor_id_left: ‹eigenspace c (id_cblinfun ⊗⇩o A) = ⊤ ⊗⇩S eigenspace c A›
proof -
  have ‹eigenspace c (id_cblinfun ⊗⇩o A) = kernel (id_cblinfun ⊗⇩o (A - c *⇩C id_cblinfun))›
    unfolding eigenspace_def
    by (metis (no_types, lifting) complex_vector.scale_minus_left tensor_id tensor_op_right_add tensor_op_scaleC_right uminus_add_conv_diff)
  also have ‹kernel (id_cblinfun ⊗⇩o (A - c *⇩C id_cblinfun)) = ⊤ ⊗⇩S kernel (A - c *⇩C id_cblinfun)›
    by (simp add: kernel_tensor_id_left)
  also have ‹… = ⊤ ⊗⇩S eigenspace c A›
    by (simp add: eigenspace_def)
  finally show ?thesis
    by -
qed

lemma eigenspace_tensor_id_right: ‹eigenspace c (A ⊗⇩o id_cblinfun) = eigenspace c A ⊗⇩S ⊤›
proof -
  have ‹eigenspace c (id_cblinfun ⊗⇩o A) = ⊤ ⊗⇩S eigenspace c A›
    by (rule eigenspace_tensor_id_left)
  from this[THEN arg_cong, of ‹cblinfun_image swap_ell2›]
  show ?thesis
    by (simp add: swap_ell2_commute_tensor_op cblinfun_image_eigenspace_unitary swap_ell2_tensor_ccsubspace)
qed

unbundle no cblinfun_syntax

end