Theorem: MatrixCookbook.eq_533 (MatrixCookbook/10FunctionsAndOperators.lean)

State before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖A‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
simp_rw [linfty_opNorm_eq_opNorm]
State after:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)

State before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ ‖{ toLinearMap := A.mulVecLin, cont := ⋯ }‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
rw [←ContinuousLinearMap.sSup_unit_ball_eq_norm]
State after:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ sSup ((fun x => ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖) '' Metric.ball 0 1) =
    sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)

State before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
⊢ sSup ((fun x => ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖) '' Metric.ball 0 1) =
    sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
Tactic:
sorry
State after:
no goals

State before:
ι : Type ?u.96365
R : Type ?u.96368
l : Type ?u.96371
m : Type u_1
n : Type u_2
p : Type ?u.96380
q : Type ?u.96383
r : Type ?u.96386
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n ℝ
this : ‖A‖ = sSup ((fun x => ‖A *ᵥ x‖) '' Metric.sphere 0 1)
⊢ ‖A‖ = sSup {x | ∃ x_1, ∃ (_ : ‖x_1‖ = 1), ‖A *ᵥ x_1‖ = x}
Tactic:
simpa [Set.image, mem_sphere_zero_iff_norm] using this
State after:
no goals