[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace G
A : E →L[𝕜] F
x : E
y : F
⊢ inner (↑(↑adjointAux A) y) x = inner y (↑A x)
[PROOFSTEP]
rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', innerSL_apply_coe, Function.comp_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace G
A : E →L[𝕜] F
x : E
y : F
⊢ inner x (↑(↑adjointAux A) y) = inner (↑A x) y
[PROOFSTEP]
rw [← inner_conj_symm, adjointAux_inner_left, inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ↑adjointAux (↑adjointAux A) = A
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
⊢ ↑(↑adjointAux (↑adjointAux A)) v = ↑A v
[PROOFSTEP]
refine' ext_inner_left 𝕜 fun w => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
v : E
w : (fun x => F) v
⊢ inner w (↑(↑adjointAux (↑adjointAux A)) v) = inner w (↑A v)
[PROOFSTEP]
rw [adjointAux_inner_right, adjointAux_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖↑adjointAux A‖ = ‖A‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖↑adjointAux A‖ ≤ ‖A‖
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg _) fun x => _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ ‖↑(↑adjointAux A) x‖ ≤ ‖A‖ * ‖x‖
[PROOFSTEP]
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ ‖↑(↑toSesqForm A) x‖ ≤ ‖A‖ * ‖x‖
[PROOFSTEP]
exact toSesqForm_apply_norm_le
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖A‖ ≤ ‖↑adjointAux A‖
[PROOFSTEP]
nth_rw 1 [← adjointAux_adjointAux A]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖↑adjointAux (↑adjointAux A)‖ ≤ ‖↑adjointAux A‖
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_bound _ (norm_nonneg _) fun x => _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖↑(↑adjointAux (↑adjointAux A)) x‖ ≤ ‖↑adjointAux A‖ * ‖x‖
[PROOFSTEP]
rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖↑(↑toSesqForm (↑adjointAux A)) x‖ ≤ ‖↑adjointAux A‖ * ‖x‖
[PROOFSTEP]
exact toSesqForm_apply_norm_le
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
⊢ ↑adjoint (comp A B) = comp (↑adjoint B) (↑adjoint A)
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ ↑(↑adjoint (comp A B)) v = ↑(comp (↑adjoint B) (↑adjoint A)) v
[PROOFSTEP]
refine' ext_inner_left 𝕜 fun w => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : (fun x => E) v
⊢ inner w (↑(↑adjoint (comp A B)) v) = inner w (↑(comp (↑adjoint B) (↑adjoint A)) v)
[PROOFSTEP]
simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ ^ 2 = ↑re (inner (↑(↑adjoint A * A) x) x)
[PROOFSTEP]
have h : ⟪(A† * A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner (↑(↑adjoint A * A) x) x = inner (↑A x) (↑A x)
[PROOFSTEP]
rw [← adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner (↑(↑adjoint A * A) x) x = inner (↑(↑adjoint A) (↑A x)) x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
h : inner (↑(↑adjoint A * A) x) x = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner (↑(↑adjoint A * A) x) x)
[PROOFSTEP]
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ = Real.sqrt (↑re (inner (↑(↑adjoint A * A) x) x))
[PROOFSTEP]
rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ ^ 2 = ↑re (inner x (↑(↑adjoint A * A) x))
[PROOFSTEP]
have h : ⟪x, (A† * A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner x (↑(↑adjoint A * A) x) = inner (↑A x) (↑A x)
[PROOFSTEP]
rw [← adjoint_inner_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ inner x (↑(↑adjoint A * A) x) = inner x (↑(↑adjoint A) (↑A x))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
h : inner x (↑(↑adjoint A * A) x) = inner (↑A x) (↑A x)
⊢ ‖↑A x‖ ^ 2 = ↑re (inner x (↑(↑adjoint A * A) x))
[PROOFSTEP]
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ = Real.sqrt (↑re (inner x (↑(↑adjoint A * A) x)))
[PROOFSTEP]
rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
[PROOFSTEP]
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = ↑adjoint B
x : E
y : (fun x => F) x
⊢ inner (↑A x) y = inner x (↑B y)
[PROOFSTEP]
rw [h, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
⊢ A = ↑adjoint B
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
x : E
⊢ ↑A x = ↑(↑adjoint B) x
[PROOFSTEP]
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
x : E
y : (fun x => F) x
⊢ inner (↑A x) y = inner (↑(↑adjoint B) x) y
[PROOFSTEP]
simp only [adjoint_inner_left, h x y]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
⊢ ↑adjoint (id 𝕜 E) = id 𝕜 E
[PROOFSTEP]
refine' Eq.symm _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
⊢ id 𝕜 E = ↑adjoint (id 𝕜 E)
[PROOFSTEP]
rw [eq_adjoint_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
⊢ ∀ (x : E) (y : (fun x => E) x), inner (↑(id 𝕜 E) x) y = inner x (↑(id 𝕜 E) y)
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ↑adjoint (Submodule.subtypeL U) = orthogonalProjection U
[PROOFSTEP]
symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ orthogonalProjection U = ↑adjoint (Submodule.subtypeL U)
[PROOFSTEP]
rw [eq_adjoint_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ∀ (x : E) (y : (fun x => { x // x ∈ U }) x),
    inner (↑(orthogonalProjection U) x) y = inner x (↑(Submodule.subtypeL U) y)
[PROOFSTEP]
intro x u
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner (↑(orthogonalProjection U) x) u = inner x (↑(Submodule.subtypeL U) u)
[PROOFSTEP]
rw [U.coe_inner, inner_orthogonalProjection_left_eq_right, orthogonalProjection_mem_subspace_eq_self]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
x : E
u : { x // x ∈ U }
⊢ inner x ↑u = inner x (↑(Submodule.subtypeL U) u)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
inst✝³ : CompleteSpace E
inst✝² : CompleteSpace G
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ ↑adjoint (orthogonalProjection U) = Submodule.subtypeL U
[PROOFSTEP]
rw [← U.adjoint_subtypeL, adjoint_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
⊢ ∀ {x : E →L[𝕜] E}, ‖star x * x‖ = ‖x‖ * ‖x‖
[PROOFSTEP]
intro A
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖star A * A‖ = ‖A‖ * ‖A‖
[PROOFSTEP]
rw [star_eq_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖↑adjoint A * A‖ = ‖A‖ * ‖A‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖↑adjoint A * A‖ ≤ ‖A‖ * ‖A‖
[PROOFSTEP]
calc
  ‖A† * A‖ ≤ ‖A†‖ * ‖A‖ := op_norm_comp_le _ _
  _ = ‖A‖ * ‖A‖ := by rw [LinearIsometryEquiv.norm_map]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖↑adjoint A‖ * ‖A‖ = ‖A‖ * ‖A‖
[PROOFSTEP]
rw [LinearIsometryEquiv.norm_map]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖A‖ * ‖A‖ ≤ ‖↑adjoint A * A‖
[PROOFSTEP]
rw [← sq, ← Real.sqrt_le_sqrt_iff (norm_nonneg _), Real.sqrt_sq (norm_nonneg _)]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
⊢ ‖A‖ ≤ Real.sqrt ‖↑adjoint A * A‖
[PROOFSTEP]
refine' op_norm_le_bound _ (Real.sqrt_nonneg _) fun x => _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
⊢ ‖↑A x‖ ≤ Real.sqrt ‖↑adjoint A * A‖ * ‖x‖
[PROOFSTEP]
have :=
  calc
    re ⟪(A† * A) x, x⟫ ≤ ‖(A† * A) x‖ * ‖x‖ := re_inner_le_norm _ _
    _ ≤ ‖A† * A‖ * ‖x‖ * ‖x‖ := mul_le_mul_of_nonneg_right (le_op_norm _ _) (norm_nonneg _)
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
this : ↑re (inner (↑(↑adjoint A * A) x) x) ≤ ‖↑adjoint A * A‖ * ‖x‖ * ‖x‖
⊢ ‖↑A x‖ ≤ Real.sqrt ‖↑adjoint A * A‖ * ‖x‖
[PROOFSTEP]
calc
  ‖A x‖ = Real.sqrt (re ⟪(A† * A) x, x⟫) := by rw [apply_norm_eq_sqrt_inner_adjoint_left]
  _ ≤ Real.sqrt (‖A† * A‖ * ‖x‖ * ‖x‖) := (Real.sqrt_le_sqrt this)
  _ = Real.sqrt ‖A† * A‖ * ‖x‖ := by
    simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖), Real.sqrt_mul_self (norm_nonneg x)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
this : ↑re (inner (↑(↑adjoint A * A) x) x) ≤ ‖↑adjoint A * A‖ * ‖x‖ * ‖x‖
⊢ ‖↑A x‖ = Real.sqrt (↑re (inner (↑(↑adjoint A * A) x) x))
[PROOFSTEP]
rw [apply_norm_eq_sqrt_inner_adjoint_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : E →L[𝕜] E
x : E
this : ↑re (inner (↑(↑adjoint A * A) x) x) ≤ ‖↑adjoint A * A‖ * ‖x‖ * ‖x‖
⊢ Real.sqrt (‖↑adjoint A * A‖ * ‖x‖ * ‖x‖) = Real.sqrt ‖↑adjoint A * A‖ * ‖x‖
[PROOFSTEP]
simp_rw [mul_assoc, Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖), Real.sqrt_mul_self (norm_nonneg x)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : InnerProductSpace 𝕜 E
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : InnerProductSpace 𝕜 G
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace G
inst✝⁶ : CompleteSpace F
E' : Type u_5
F' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : CompleteSpace E'
inst✝ : CompleteSpace F'
A : E' →L[ℝ] F'
⊢ LinearMap.IsAdjointPair sesqFormOfInner sesqFormOfInner ↑A ↑(↑adjoint A)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : InnerProductSpace 𝕜 E
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : InnerProductSpace 𝕜 G
inst✝⁸ : CompleteSpace E
inst✝⁷ : CompleteSpace G
inst✝⁶ : CompleteSpace F
E' : Type u_5
F' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : CompleteSpace E'
inst✝ : CompleteSpace F'
A : E' →L[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑↑A x)) y = ↑(↑sesqFormOfInner x) (↑↑(↑adjoint A) y)
[PROOFSTEP]
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left, coe_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] E
hA : IsSelfAdjoint A
⊢ LinearMap.IsSymmetric ↑A
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] E
hA : IsSelfAdjoint A
x y : E
⊢ inner (↑↑A x) y = inner x (↑↑A y)
[PROOFSTEP]
rw_mod_cast [← A.adjoint_inner_right, hA.adjoint_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : E →L[𝕜] F
⊢ IsSelfAdjoint (comp S (comp T (↑adjoint S)))
[PROOFSTEP]
rw [isSelfAdjoint_iff'] at hT ⊢
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ ↑adjoint (comp S (comp T (↑adjoint S))) = comp S (comp T (↑adjoint S))
[PROOFSTEP]
simp only [hT, adjoint_comp, adjoint_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : E →L[𝕜] F
⊢ comp (comp S T) (↑adjoint S) = comp S (comp T (↑adjoint S))
[PROOFSTEP]
exact ContinuousLinearMap.comp_assoc _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : F →L[𝕜] E
⊢ IsSelfAdjoint (comp (↑adjoint S) (comp T S))
[PROOFSTEP]
rw [isSelfAdjoint_iff'] at hT ⊢
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : F →L[𝕜] E
⊢ ↑adjoint (comp (↑adjoint S) (comp T S)) = comp (↑adjoint S) (comp T S)
[PROOFSTEP]
simp only [hT, adjoint_comp, adjoint_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : ↑adjoint T = T
S : F →L[𝕜] E
⊢ comp (comp (↑adjoint S) T) S = comp (↑adjoint S) (comp T S)
[PROOFSTEP]
exact ContinuousLinearMap.comp_assoc _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] E
hA : LinearMap.IsSymmetric ↑A
⊢ IsSelfAdjoint A
[PROOFSTEP]
rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA 
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsSelfAdjoint
    (comp (Submodule.subtypeL U)
      (comp (orthogonalProjection U) (comp T (comp (Submodule.subtypeL U) (orthogonalProjection U)))))
[PROOFSTEP]
rw [← ContinuousLinearMap.comp_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsSelfAdjoint
    (comp (comp (Submodule.subtypeL U) (orthogonalProjection U))
      (comp T (comp (Submodule.subtypeL U) (orthogonalProjection U))))
[PROOFSTEP]
nth_rw 1 [← (orthogonalProjection_isSelfAdjoint U).adjoint_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsSelfAdjoint
    (comp (↑adjoint (comp (Submodule.subtypeL U) (orthogonalProjection U)))
      (comp T (comp (Submodule.subtypeL U) (orthogonalProjection U))))
[PROOFSTEP]
refine' hT.adjoint_conj _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner (↑(↑adjoint A) y) x = inner y (↑A x)
[PROOFSTEP]
rw [← coe_toContinuousLinearMap A, adjoint_eq_toClm_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) x =
    inner y (↑↑(↑toContinuousLinearMap A) x)
[PROOFSTEP]
exact ContinuousLinearMap.adjoint_inner_left _ x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner x (↑(↑adjoint A) y) = inner (↑A x) y
[PROOFSTEP]
rw [← coe_toContinuousLinearMap A, adjoint_eq_toClm_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
x : E
y : F
⊢ inner x (↑↑(↑ContinuousLinearMap.adjoint (↑toContinuousLinearMap ↑(↑toContinuousLinearMap A))) y) =
    inner (↑↑(↑toContinuousLinearMap A) x) y
[PROOFSTEP]
exact ContinuousLinearMap.adjoint_inner_right _ x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
⊢ ↑adjoint (↑adjoint A) = A
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
v : E
⊢ ↑(↑adjoint (↑adjoint A)) v = ↑A v
[PROOFSTEP]
refine' ext_inner_left 𝕜 fun w => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
v : E
w : (fun x => F) v
⊢ inner w (↑(↑adjoint (↑adjoint A)) v) = inner w (↑A v)
[PROOFSTEP]
rw [adjoint_inner_right, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
⊢ ↑adjoint (comp A B) = comp (↑adjoint B) (↑adjoint A)
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
⊢ ↑(↑adjoint (comp A B)) v = ↑(comp (↑adjoint B) (↑adjoint A)) v
[PROOFSTEP]
refine' ext_inner_left 𝕜 fun w => _
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : F →ₗ[𝕜] G
B : E →ₗ[𝕜] F
v : G
w : (fun x => E) v
⊢ inner w (↑(↑adjoint (comp A B)) v) = inner w (↑(comp (↑adjoint B) (↑adjoint A)) v)
[PROOFSTEP]
simp only [adjoint_inner_right, LinearMap.coe_comp, Function.comp_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
[PROOFSTEP]
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = ↑adjoint B
x : E
y : (fun x => F) x
⊢ inner (↑A x) y = inner x (↑B y)
[PROOFSTEP]
rw [h, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
⊢ A = ↑adjoint B
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
x : E
⊢ ↑A x = ↑(↑adjoint B) x
[PROOFSTEP]
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : (fun x => F) x), inner (↑A x) y = inner x (↑B y)
x : E
y : (fun x => F) x
⊢ inner (↑A x) y = inner (↑(↑adjoint B) x) y
[PROOFSTEP]
simp only [adjoint_inner_left, h x y]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), inner (↑A (↑b₁ i₁)) (↑b₂ i₂) = inner (↑b₁ i₁) (↑B (↑b₂ i₂))
[PROOFSTEP]
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = ↑adjoint B
x : ι₁
y : ι₂
⊢ inner (↑A (↑b₁ x)) (↑b₂ y) = inner (↑b₁ x) (↑B (↑b₂ y))
[PROOFSTEP]
rw [h, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i₁ : ι₁) (i₂ : ι₂), inner (↑A (↑b₁ i₁)) (↑b₂ i₂) = inner (↑b₁ i₁) (↑B (↑b₂ i₂))
⊢ A = ↑adjoint B
[PROOFSTEP]
refine' Basis.ext b₁ fun i₁ => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i₁ : ι₁) (i₂ : ι₂), inner (↑A (↑b₁ i₁)) (↑b₂ i₂) = inner (↑b₁ i₁) (↑B (↑b₂ i₂))
i₁ : ι₁
⊢ ↑A (↑b₁ i₁) = ↑(↑adjoint B) (↑b₁ i₁)
[PROOFSTEP]
exact ext_inner_right_basis b₂ fun i₂ => by simp only [adjoint_inner_left, h i₁ i₂]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i₁ : ι₁) (i₂ : ι₂), inner (↑A (↑b₁ i₁)) (↑b₂ i₂) = inner (↑b₁ i₁) (↑B (↑b₂ i₂))
i₁ : ι₁
i₂ : ι₂
⊢ inner (↑A (↑b₁ i₁)) (↑b₂ i₂) = inner (↑(↑adjoint B) (↑b₁ i₁)) (↑b₂ i₂)
[PROOFSTEP]
simp only [adjoint_inner_left, h i₁ i₂]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
[PROOFSTEP]
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = ↑adjoint B
x : ι
y : (fun x => F) (↑b x)
⊢ inner (↑A (↑b x)) y = inner (↑b x) (↑B y)
[PROOFSTEP]
rw [h, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
i : ι
⊢ ↑A (↑b i) = ↑(↑adjoint B) (↑b i)
[PROOFSTEP]
exact ext_inner_right 𝕜 fun y => by simp only [h i, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : (fun x => F) (↑b i)), inner (↑A (↑b i)) y = inner (↑b i) (↑B y)
i : ι
y : (fun x => F) (↑b i)
⊢ inner (↑A (↑b i)) y = inner (↑(↑adjoint B) (↑b i)) y
[PROOFSTEP]
simp only [h i, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = ↑adjoint B ↔ ∀ (i : ι) (x : E), inner (↑A x) (↑b i) = inner x (↑B (↑b i))
[PROOFSTEP]
refine' ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = ↑adjoint B
x : ι
y : E
⊢ inner (↑A y) (↑b x) = inner y (↑B (↑b x))
[PROOFSTEP]
rw [h, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (x : E), inner (↑A x) (↑b i) = inner x (↑B (↑b i))
⊢ A = ↑adjoint B
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (x : E), inner (↑A x) (↑b i) = inner x (↑B (↑b i))
x : E
⊢ ↑A x = ↑(↑adjoint B) x
[PROOFSTEP]
refine' ext_inner_right_basis b fun i => by simp only [h i, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (x : E), inner (↑A x) (↑b i) = inner x (↑B (↑b i))
x : E
i : ι
⊢ inner (↑A x) (↑b i) = inner (↑(↑adjoint B) x) (↑b i)
[PROOFSTEP]
simp only [h i, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] E
⊢ IsSymmetric A ↔ IsSelfAdjoint A
[PROOFSTEP]
rw [isSelfAdjoint_iff', IsSymmetric, ← LinearMap.eq_adjoint_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
A : E →ₗ[𝕜] E
⊢ A = ↑adjoint A ↔ ↑adjoint A = A
[PROOFSTEP]
exact eq_comm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : InnerProductSpace 𝕜 E
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : InnerProductSpace 𝕜 G
inst✝⁸ : FiniteDimensional 𝕜 E
inst✝⁷ : FiniteDimensional 𝕜 F
inst✝⁶ : FiniteDimensional 𝕜 G
E' : Type u_5
F' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : FiniteDimensional ℝ E'
inst✝ : FiniteDimensional ℝ F'
A : E' →ₗ[ℝ] F'
⊢ IsAdjointPair sesqFormOfInner sesqFormOfInner A (↑adjoint A)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁵ : IsROrC 𝕜
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedAddCommGroup G
inst✝¹¹ : InnerProductSpace 𝕜 E
inst✝¹⁰ : InnerProductSpace 𝕜 F
inst✝⁹ : InnerProductSpace 𝕜 G
inst✝⁸ : FiniteDimensional 𝕜 E
inst✝⁷ : FiniteDimensional 𝕜 F
inst✝⁶ : FiniteDimensional 𝕜 G
E' : Type u_5
F' : Type u_6
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ E'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : FiniteDimensional ℝ E'
inst✝ : FiniteDimensional ℝ F'
A : E' →ₗ[ℝ] F'
x : E'
y : F'
⊢ ↑(↑sesqFormOfInner (↑A x)) y = ↑(↑sesqFormOfInner x) (↑(↑adjoint A) y)
[PROOFSTEP]
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
⊢ IsSymmetric (↑adjoint T * T)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x y : E
⊢ inner (↑(↑adjoint T * T) x) y = inner x (↑(↑adjoint T * T) y)
[PROOFSTEP]
simp only [mul_apply, adjoint_inner_left, adjoint_inner_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ↑re (inner x (↑(↑adjoint T * T) x))
[PROOFSTEP]
simp only [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ↑re (↑‖↑T x‖ ^ 2)
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ‖↑T x‖ ^ 2
[PROOFSTEP]
exact sq_nonneg _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x : E
⊢ ↑im (inner x (↑(↑adjoint T) (↑T x))) = 0
[PROOFSTEP]
simp only [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
T : E →ₗ[𝕜] E
x : E
⊢ ↑im (↑‖↑T x‖ ^ 2) = 0
[PROOFSTEP]
norm_cast
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_5
n : Type u_6
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ↑toEuclideanLin Aᴴ = ↑LinearMap.adjoint (↑toEuclideanLin A)
[PROOFSTEP]
rw [LinearMap.eq_adjoint_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_5
n : Type u_6
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ∀ (x : EuclideanSpace 𝕜 m) (y : (fun x => EuclideanSpace 𝕜 n) x),
    inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
[PROOFSTEP]
intro x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : InnerProductSpace 𝕜 G
m : Type u_5
n : Type u_6
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
x : EuclideanSpace 𝕜 m
y : EuclideanSpace 𝕜 n
⊢ inner (↑(↑toEuclideanLin Aᴴ) x) y = inner x (↑(↑toEuclideanLin A) y)
[PROOFSTEP]
simp_rw [EuclideanSpace.inner_eq_star_dotProduct, piLp_equiv_toEuclideanLin, toLin'_apply, star_mulVec,
  conjTranspose_conjTranspose, dotProduct_mulVec]
