awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A : Type u_2
inst : CStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
b : f.GNS (A := A)
h :
  IsClosed.{u_2} (X := Completion (f.PreGNS (A := A)))
    {a : Completion (f.PreGNS (A := A)) |
      Eq (α := f.GNS (A := A))
        (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))
        ((1 : (a : f.GNS) → f.GNS) a : f.GNS (A := A))}
h₁ :
  ∀ (b : f.PreGNS (A := A)),
    Eq (α := f.GNS (A := A))
      (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) (↑b : Completion f.PreGNS) :
        f.GNS (A := A))
      ((1 : (a : f.GNS) → f.GNS) (↑b : Completion f.PreGNS) : f.GNS (A := A))
⊢ Eq (α := f.GNS (A := A))
    (((f.gnsNonUnitalStarAlgHom : (a : A) → f.GNS →L[ℂ] f.GNS) 1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))
    ((1 : (a : f.GNS) → f.GNS) b : f.GNS (A := A))

Tactic:
induction b using induction_on with
  | hp => apply isClosed_eq <;> fun_prop
  | ih b => simp [gnsNonUnitalStarAlgHom]

Premises used: PositiveLinearMap.gnsNonUnitalStarAlgHom, isClosed_eq
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A_1 : Type u_1
inst : NonUnitalCStarAlgebra A_1
inst_1 : PartialOrder A_1
f_1 : A_1 →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A_1
A : Type u_2
inst_3 : CStarAlgebra A
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
⊢ Eq.{u_2 + 1} (α := f.GNS (A := A) →L[ℂ] f.GNS (A := A))
    (MulActionHom.toFun
      (DistribMulActionHom.toMulActionHom
        (NonUnitalAlgHom.toDistribMulActionHom (NonUnitalStarAlgHom.toNonUnitalAlgHom f.gnsNonUnitalStarAlgHom)))
      1)
    1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
Goal:
A_1 : Type u_1
inst : NonUnitalCStarAlgebra A_1
inst_1 : PartialOrder A_1
f_1 : A_1 →ₚ[ℂ] ℂ
inst_2 : StarOrderedRing A_1
A : Type u_2
inst_3 : CStarAlgebra A
inst_4 : PartialOrder A
inst_5 : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
r : ℂ
⊢ Eq (α := f.GNS (A := A) →L[ℂ] f.GNS (A := A))
    (MulActionHom.toFun
        (DistribMulActionHom.toMulActionHom
          (NonUnitalAlgHom.toDistribMulActionHom (NonUnitalStarAlgHom.toNonUnitalAlgHom f.gnsNonUnitalStarAlgHom)))
        ((algebraMap ℂ A : (a : ℂ) → A) r) :
      f.GNS (A := A) →L[ℂ] f.GNS (A := A))
    ((algebraMap ℂ (f.GNS (A := A) →L[ℂ] f.GNS (A := A)) : (a : ℂ) → f.GNS →L[ℂ] f.GNS) r :
      f.GNS (A := A) →L[ℂ] f.GNS (A := A))

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
a :
  ∀ (x : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ)) x →
      0 ≤ x
a₁ :
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
    (HPow.hPow (β := ℕ) ‖U i j‖ 2)
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2

Tactic:
apply Multiset.single_le_sum

Premises used: Multiset.single_le_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
h_x :
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
    x
⊢ ∃ (a : n), Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x

Tactic:
rw [Multiset.mem_map] at h_x

Premises used: Multiset.mem_map
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
h_x : ∃ (a : n), Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
a :
  ∀ (a : n) (h_a : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x),
    0 ≤ x
⊢ 0 ≤ x

Tactic:
obtain ⟨a, h_a⟩ := h_x
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
a : n
h_a : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
a₁ : 0 ≤ HPow.hPow (β := ℕ) ‖U i a‖ 2
⊢ 0 ≤ x

Tactic:
rw [← h_a.2]

Premises used: And.right
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
x : ℝ
a : n
h_a : Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧ HPow.hPow (β := ℕ) ‖U i a‖ 2 = x
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖U i a‖ 2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
a :
  ∃ (a : n),
    Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧
      HPow.hPow (β := ℕ) ‖U i a‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2
⊢ Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (x : n) ↦ HPow.hPow (β := ℕ) ‖U i x‖ 2) (Finset.val Finset.univ))
    (HPow.hPow (β := ℕ) ‖U i j‖ 2)

Tactic:
rw [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
h :
  Membership.mem (γ := Multiset n) (Finset.val Finset.univ) j ∧
    HPow.hPow (β := ℕ) ‖U i j‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2
⊢ ∃ (a : n),
    Membership.mem (γ := Multiset n) (Finset.val Finset.univ) a ∧
      HPow.hPow (β := ℕ) ‖U i a‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2

Tactic:
use j
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ Membership.mem (γ := Multiset n) (Finset.val Finset.univ) j ∧
    HPow.hPow (β := ℕ) ‖U i j‖ 2 = HPow.hPow (β := ℕ) ‖U i j‖ 2

Tactic:
simp only [Finset.mem_univ_val, and_self_iff]

Premises used: Finset.mem_univ_val, and_self_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2

Tactic:
have norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2 := by
    apply Multiset.single_le_sum
    · intro x h_x
      rw [Multiset.mem_map] at h_x
      obtain ⟨a, h_a⟩ := h_x
      rw [← h_a.2]
      apply sq_nonneg
    · rw [Multiset.mem_map]
      use j
      simp only [Finset.mem_univ_val, and_self_iff]
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
simp :
  Eq.{u_1 + 1} (α := 𝕜) (∑ x : n, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖U i x‖ : 𝕜) 2)
    (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
⊢ (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)

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

Premises used: RCLike.mul_conj, Matrix.mul_apply, starRingEnd_apply, Matrix.conjTranspose_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∑ i_1 : n, HPow.hPow (β := ℕ) ‖U i i_1‖ 2) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x : n, HPow.hPow (α := 𝕜) (β := ℕ) (↑‖U i x‖ : 𝕜) 2)
    (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
⊢ (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)

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]
    norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)

Tactic:
rw [RCLike.ext_iff] at diag_eq_norm_sum

Premises used: RCLike.ext_iff
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
rw :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
    (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)

Tactic:
rw [diag_eq_norm_sum.1]

Premises used: And.left
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ) ∧
    Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ)
      ((RCLike.im : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜) : ℝ)
    (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)

Tactic:
have re_diag_eq_norm_sum : RCLike.re ((U * Uᴴ) i i) = ∑ x : n, ‖U i x‖ ^ 2 := by
    rw [RCLike.ext_iff] at diag_eq_norm_sum
    rw [diag_eq_norm_sum.1]
    norm_cast
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
⊢ U * Uᴴ = 1

Tactic:
have mul_eq_one : U * Uᴴ = 1 := Unitary.mul_star_self_of_mem hU
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)

Tactic:
simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]

Premises used: RCLike.one_re, Matrix.one_apply_eq
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)

Tactic:
have diag_eq_one : RCLike.re ((U * Uᴴ) i i) = 1 := by
    simp only [mul_eq_one, Matrix.one_apply_eq, RCLike.one_re]
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
diag_eq_one : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)
rw : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
⊢ ‖U i j‖ ≤ 1

Tactic:
rw [← sq_le_one_iff₀ (norm_nonneg (U i j)), ← diag_eq_one, re_diag_eq_norm_sum]

Premises used: sq_le_one_iff₀, norm_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
diag_eq_one : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2

Tactic:
norm_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i j : n
norm_sum : HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2
diag_eq_norm_sum : (U * Uᴴ) i i = (↑(∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2) : 𝕜)
re_diag_eq_norm_sum :
  Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2 : ℝ)
mul_eq_one : U * Uᴴ = 1
diag_eq_one : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((U * Uᴴ) i i) : ℝ) (1 : ℝ)
⊢ HPow.hPow (β := ℕ) ‖U i j‖ 2 ≤ ∑ x : n, HPow.hPow (β := ℕ) ‖U i x‖ 2

Tactic:
exact norm_sum
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
simp_rw : ∀ (i i_1 : n), ‖U i i_1‖ ≤ 1
⊢ ‖U‖ ≤ 1

Tactic:
simp_rw [pi_norm_le_iff_of_nonneg zero_le_one]

Premises used: pi_norm_le_iff_of_nonneg, zero_le_one
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i i_1 : n
⊢ ‖U i i_1‖ ≤ 1

Tactic:
entry_norm_bound_of_unitary hU _ _

Premises used: entry_norm_bound_of_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
U : Matrix n n 𝕜
hU : Membership.mem (γ := Submonoid (Matrix n n 𝕜)) (Matrix.unitaryGroup n 𝕜) U
i i_1 : n
⊢ ‖U i i_1‖ ≤ 1

Tactic:
exact entry_norm_bound_of_unitary hU _ _

Premises used: entry_norm_bound_of_unitary
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
⊢ Eq (α := EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
    (↑((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A) :
      EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n)
    ((toEuclideanLin : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n) A)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
x : n → 𝕜
⊢ Eq (α := EuclideanSpace 𝕜 n)
    ((((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n)
        (toLp 2 x) :
      EuclideanSpace 𝕜 n)
    (toLp 2 (A *ᵥ x) : WithLp 2 (n → 𝕜))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
𝕜 : Type u_1
n : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
x : EuclideanSpace 𝕜 n
⊢ ofLp (p := 2)
      ((((toEuclideanCLM : (a : Matrix n n 𝕜) → EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) A :
            EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :
          (a : EuclideanSpace 𝕜 n) → EuclideanSpace 𝕜 n)
        x) =
    A *ᵥ x.ofLp

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
simp :
  Eq (α := ℝ)
    (∑ x_1 : n,
      (∑ x : n,
          HMul.hMul (α := ℝ) (β := ℝ) (∑ x_2 : n, y.ofLp x_2 * A x x_2 : ℝ)
            (Pi.single (M := fun (x : n) ↦ ℝ) x 1 x_1 : ℝ)) *
        x.ofLp x_1)
    (∑ x_1 : n, x.ofLp x_1 * ∑ x : n, y.ofLp x * A x_1 x)
⊢ ⟪x,
      (((toEuclideanCLM : (a : Matrix n n ℝ) → EuclideanSpace ℝ n →L[ℝ] EuclideanSpace ℝ n) A :
            EuclideanSpace ℝ n →L[ℝ] EuclideanSpace ℝ n) :
          (a : EuclideanSpace ℝ n) → EuclideanSpace ℝ n)
        y⟫ =
    x.ofLp ⬝ᵥ A *ᵥ y.ofLp

Tactic:
simp only [toEuclideanCLM, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe,
    LinearEquiv.invFun_eq_symm, LinearMap.coe_toContinuousLinearMap_symm, StarAlgEquiv.trans_apply,
    LinearMap.toMatrixOrthonormal_symm_apply, LinearMap.toMatrix_symm, StarAlgEquiv.coe_mk,
    StarRingEquiv.coe_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, LinearMap.coe_toContinuousLinearMap',
    toLin_apply, mulVec_eq_sum, OrthonormalBasis.coe_toBasis_repr_apply,
    EuclideanSpace.basisFun_repr, op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply,
    smul_eq_mul, OrthonormalBasis.coe_toBasis, EuclideanSpace.basisFun_apply, PiLp.inner_apply,
    ofLp_sum, ofLp_smul, PiLp.ofLp_single, RCLike.inner_apply, conj_trivial, dotProduct]

Premises used: WithLp.ofLp_smul, EuclideanSpace.basisFun_apply, LinearMap.coe_toContinuousLinearMap', Matrix.toEuclideanCLM, PiLp.ofLp_single, dotProduct, LinearMap.toMatrix_symm, Finset.sum_apply, LinearEquiv.invFun_eq_symm, AddHom.toFun_eq_coe, conj_trivial, RingEquiv.coe_mk, LinearMap.toMatrixOrthonormal_symm_apply, OrthonormalBasis.coe_toBasis, RCLike.inner_apply, EuclideanSpace.basisFun_repr, Matrix.toLin_apply, Matrix.mulVec_eq_sum, LinearMap.coe_toAddHom, Equiv.coe_fn_mk, OrthonormalBasis.coe_toBasis_repr_apply, smul_eq_mul, PiLp.inner_apply, LinearMap.coe_toContinuousLinearMap_symm, WithLp.ofLp_sum, StarAlgEquiv.coe_mk, Matrix.transpose_apply, StarRingEquiv.coe_mk, StarAlgEquiv.trans_apply, IsCentralScalar.op_smul_eq_smul, LinearEquiv.coe_coe, Pi.smul_apply
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
e_f :
  ∀ (i : n),
    (∑ x : n,
          HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
            (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
        x.ofLp i =
      x.ofLp i * ∑ x : n, y.ofLp x * A i x
⊢ Eq (α := ℝ)
    (∑ x_1 : n,
      (∑ x : n,
          HMul.hMul (α := ℝ) (β := ℝ) (∑ x_2 : n, y.ofLp x_2 * A x x_2 : ℝ)
            (Pi.single (M := fun (x : n) ↦ ℝ) x 1 x_1 : ℝ)) *
        x.ofLp x_1)
    (∑ x_1 : n, x.ofLp x_1 * ∑ x : n, y.ofLp x * A x_1 x)

Tactic:
congr with i
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
e_f :
  (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
      x.ofLp i =
    (∑ x : n, y.ofLp x * A i x) * x.ofLp i
⊢ (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
      x.ofLp i =
    x.ofLp i * ∑ x : n, y.ofLp x * A i x

Tactic:
rw [mul_comm (x.ofLp i)]

Premises used: mul_comm, WithLp.ofLp
-- Module: Mathlib.Analysis.CStarAlgebra.Matrix
Goal:
n : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
A : Matrix n n ℝ
x y : EuclideanSpace ℝ n
i : n
⊢ (∑ x : n,
        HMul.hMul (α := ℝ) (β := ℝ) (∑ x_1 : n, y.ofLp x_1 * A x x_1 : ℝ)
          (Pi.single (M := fun (x : n) ↦ ℝ) x 1 i : ℝ)) *
      x.ofLp i =
    (∑ x : n, y.ofLp x * A i x) * x.ofLp i

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply