[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]


[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
let f : G → R := fun g => toFun hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
let U : Set G := (R * S).image fun g => g * (f g : G)⁻¹
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
change (closure U : Set G) * R = ⊤
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
⊢ ↑(closure U) * R = ⊤
[PROOFSTEP]
refine' top_le_iff.mp fun g _ => _
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ ↑(closure U) * R
[PROOFSTEP]
apply closure_induction_right (eq_top_iff.mp hS (mem_top g))
[GOAL]
case H1
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ 1 ∈ ↑(closure U) * R
[PROOFSTEP]
exact ⟨1, 1, (closure U).one_mem, hR1, one_mul 1⟩
[GOAL]
case Hmul
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ ∀ (x y : G), y ∈ S → x ∈ ↑(closure U) * R → x * y ∈ ↑(closure U) * R
[PROOFSTEP]
rintro - s hs ⟨u, r, hu, hr, rfl⟩
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun x x_1 => x * x_1) u r * s ∈ ↑(closure U) * R
[PROOFSTEP]
rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * r * s = u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s))
[PROOFSTEP]
group
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s)) ∈ ↑(closure U) * R
[PROOFSTEP]
refine' Set.mul_mem_mul ((closure U).mul_mem hu _) (f (r * s)).coe_prop
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ r * s * (↑(f (r * s)))⁻¹ ∈ closure U
[PROOFSTEP]
exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩
[GOAL]
case Hinv
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ ∀ (x y : G), y ∈ S → x ∈ ↑(closure U) * R → x * y⁻¹ ∈ ↑(closure U) * R
[PROOFSTEP]
rintro - s hs ⟨u, r, hu, hr, rfl⟩
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun x x_1 => x * x_1) u r * s⁻¹ ∈ ↑(closure U) * R
[PROOFSTEP]
rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * r * s⁻¹ = u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹))
[PROOFSTEP]
group
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹)) ∈ ↑(closure U) * R
[PROOFSTEP]
refine' Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem _)) (f (r * s⁻¹)).2
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * r⁻¹ ∈ closure U
[PROOFSTEP]
refine' subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, _⟩
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun g => g * (↑(f g))⁻¹) (↑(f (r * s⁻¹)) * s) = ↑(f (r * s⁻¹)) * s * r⁻¹
[PROOFSTEP]
rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ f (↑(toFun hR (↑{ val := r, property := hr } * s⁻¹)) * s) = { val := r, property := hr }
[PROOFSTEP]
apply
  (mem_rightTransversals_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
    (mul_inv_toFun_mem hR (f (r * s⁻¹) * s))
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * (↑{ val := r, property := hr })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * (↑{ val := r, property := hr } * s⁻¹)⁻¹ ∈ ↑H
[PROOFSTEP]
exact toFun_mul_inv_mem hR (r * s⁻¹)
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
[PROOFSTEP]
have hU : closure ((R * S).image fun g => g * (toFun hR g : G)⁻¹) ≤ H :=
  by
  rw [closure_le]
  rintro - ⟨g, -, rfl⟩
  exact mul_inv_toFun_mem hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
[PROOFSTEP]
rw [closure_le]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(toFun hR g))⁻¹) '' (R * S) ⊆ ↑H
[PROOFSTEP]
rintro - ⟨g, -, rfl⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(toFun hR g))⁻¹) g ∈ ↑H
[PROOFSTEP]
exact mul_inv_toFun_mem hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
[PROOFSTEP]
refine' le_antisymm hU fun h hh => _
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
obtain ⟨g, r, hg, hr, rfl⟩ := show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
this : { val := r, property := hr } = { val := 1, property := hR1 }
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ { val := r, property := hr } = { val := 1, property := hR1 }
[PROOFSTEP]
apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.mp hR r).unique
[GOAL]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := r, property := hr })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [Subtype.coe_mk, mul_inv_self]
[GOAL]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ 1 ∈ ↑H
[PROOFSTEP]
exact H.one_mem
[GOAL]
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := 1, property := hR1 })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [Subtype.coe_mk, inv_one, mul_one]
[GOAL]
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r ∈ ↑H
[PROOFSTEP]
exact (H.mul_mem_cancel_left (hU hg)).mp hh
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (R * S)) = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map (Subgroup.subtype H) ⊤ ≤
    closure
      ((fun x => ↑(Subgroup.subtype H) { val := x * (↑(toFun hR x))⁻¹, property := (_ : x * (↑(toFun hR x))⁻¹ ∈ H) }) ''
        (R * S))
[PROOFSTEP]
exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure
      ↑(Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) =
    ⊤
[PROOFSTEP]
rw [Finset.coe_image, Finset.coe_mul]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (↑R * ↑S)) = ⊤
[PROOFSTEP]
exact closure_mul_image_eq_top hR hR1 hS
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
haveI : DecidableEq G := Classical.decEq G
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
obtain ⟨R₀, hR : R₀ ∈ rightTransversals (H : Set G), hR1⟩ := exists_right_transversal (1 : G)
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
haveI : Fintype R₀ := Fintype.ofEquiv _ (toEquiv hR)
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
let R : Finset G := Set.toFinset R₀
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
replace hR : (R : Set G) ∈ rightTransversals (H : Set G) := by rwa [Set.coe_toFinset]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ↑R ∈ rightTransversals ↑H
[PROOFSTEP]
rwa [Set.coe_toFinset]
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ 1 ∈ R
[PROOFSTEP]
rwa [Set.mem_toFinset]
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
refine' ⟨_, _, closure_mul_image_eq_top' hR hR1 hS⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card
      (Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) ≤
    index H * Finset.card S
[PROOFSTEP]
calc
  _ ≤ (R * S).card := Finset.card_image_le
  _ ≤ (R ×ˢ S).card := Finset.card_image_le
  _ = R.card * S.card := (R.card_product S)
  _ = H.index * S.card := congr_arg (· * S.card) ?_
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card R = index H
[PROOFSTEP]
calc
  R.card = Fintype.card R := (Fintype.card_coe R).symm
  _ = _ := (Fintype.card_congr (toEquiv hR)).symm
  _ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H)
  _ = H.index := H.index_eq_card.symm
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
obtain ⟨S, hS⟩ := hG.1
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
T : Finset { x // x ∈ H }
hT : closure ↑T = ⊤
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
exact ⟨⟨T, hT⟩⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
haveI := H.fg_of_index_ne_zero
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
T : Finset { x // x ∈ H }
hT₀ : Finset.card T ≤ index H * Finset.card S
hT : closure ↑T = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
calc
  Group.rank H ≤ T.card := Group.rank_le H hT
  _ ≤ H.index * S.card := hT₀
  _ = H.index * Group.rank G := congr_arg ((· * ·) H.index) hS₀
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
by_cases hG : (center G).index = 0
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
haveI : FiniteIndex (center G) :=
  ⟨hG⟩
    -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ']
  -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
[PROOFSTEP]
have h1 :=
  relindex_dvd_index_of_normal (center G)
    (_root_.commutator G)
      -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
[PROOFSTEP]
refine' mul_dvd_mul _ h1
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
haveI : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
  ⟨ne_zero_of_dvd_ne_zero hG h1⟩
    -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h2 :=
  rank_le_index_mul_rank
    ((center G).subgroupOf (_root_.commutator G))
      -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h3 :=
  Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1)
    (rank_commutator_le_card G)
      -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
refine'
  dvd_trans _
    (pow_dvd_pow (center G).index (h2.trans h3))
      -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
[PROOFSTEP]
apply card_dvd_exponent_pow_rank'
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }), g ^ index (center G) = 1
[PROOFSTEP]
intro g
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
⊢ g ^ index (center G) = 1
[PROOFSTEP]
have :=
  Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G)
    g.1.2
      -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝¹ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this✝ : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
this : ↑↑g ∈ MonoidHom.ker (MonoidHom.transferCenterPow G)
⊢ g ^ index (center G) = 1
[PROOFSTEP]
simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h1 := index_center_le_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [card_commutator_closureCommutatorRepresentatives] at h2
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
replace h1 := h1.trans (Nat.pow_le_pow_of_le_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [← pow_succ'] at h2
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
refine' (Nat.le_of_dvd _ h2).trans (Nat.pow_le_pow_of_le_left h1 _)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
[PROOFSTEP]
exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.finiteIndex) _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Finite { x // x ∈ _root_.commutator G }
[PROOFSTEP]
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Finite { x // x ∈ _root_.commutator G }
[PROOFSTEP]
refine' Nat.finite_of_card_ne_zero fun h => _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
h : Nat.card { x // x ∈ _root_.commutator G } = 0
⊢ False
[PROOFSTEP]
rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1) =
    0
h : Nat.card { x // x ∈ _root_.commutator G } = 0
⊢ False
[PROOFSTEP]
exact FiniteIndex.finiteIndex (pow_eq_zero h2)