-- Mathlib/Analysis/CStarAlgebra/Matrix.lean
theorem entry_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜)
    (i j : n) : ‖U i j‖ ≤ 1

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)

Tactic:
simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj,
  RCLike.normSq_eq_def', RCLike.ofReal_pow]

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ ∑ x : n, ↑‖U i x‖ ^ 2 = ↑(∑ x : n, ‖U i x‖ ^ 2)

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2

Tactic:
apply Multiset.single_le_sum

Result:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∀ x ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val, 0 ≤ x

case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
⊢ ‖U i j‖ ≤ 1

Tactic:
have diag_eq_norm_sum : (U * Uᴴ) i i = (∑ x : n, ‖U i x‖ ^ 2 : ℝ) := by
  simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, ← starRingEnd_apply, RCLike.mul_conj,
    RCLike.normSq_eq_def', RCLike.ofReal_pow]; norm_cast

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ ‖U i j‖ ≤ 1

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
⊢ ‖U i j‖ ≤ 1

Tactic:
have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
  simp only [mul_eq_one, eq_self_iff_true, Matrix.one_apply_eq, RCLike.one_re]

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ≤ 1

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2
mul_eq_one : U * Uᴴ = 1
diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1
⊢ ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2

Tactic:
exact norm_sum

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ‖U i j‖ ^ 2 ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val

Tactic:
rw [Multiset.mem_map]

Result:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = ‖U i j‖ ^ 2

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2

Tactic:
rw [RCLike.ext_iff] at diag_eq_norm_sum

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2

Tactic:
rw [diag_eq_norm_sum.1]

Result:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) = ∑ x : n, ‖U i x‖ ^ 2

Proof state:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : x ∈ Multiset.map (fun x => ‖U i x‖ ^ 2) Finset.univ.val
⊢ 0 ≤ x

Tactic:
rw [Multiset.mem_map] at h_x

Result:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x

Proof state:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x : n, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) ∧
    RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x : n, ‖U i x‖ ^ 2)
⊢ RCLike.re ↑(∑ x : n, ‖U i x‖ ^ 2) = ∑ x : n, ‖U i x‖ ^ 2

Tactic:
norm_cast

Result:
no goals

Proof state:
case a.intro
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x

Tactic:
rw [← h_a.2]

Result:
case a.intro
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ ‖U i a‖ ^ 2

Proof state:
case h
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ j ∈ Finset.univ.val ∧ ‖U i j‖ ^ 2 = ‖U i j‖ ^ 2

Tactic:
simp only [eq_self_iff_true, Finset.mem_univ_val, and_self_iff, sq_eq_sq₀]

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
h_x : ∃ a ∈ Finset.univ.val, ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x

Tactic:
obtain ⟨a, h_a⟩ := h_x

Result:
case a.intro
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
x : ℝ
a : n
h_a : a ∈ Finset.univ.val ∧ ‖U i a‖ ^ 2 = x
⊢ 0 ≤ x