-- Mathlib/Analysis/Matrix.lean
lemma linfty_opNNNorm_eq_opNNNorm (A : Matrix m n α) :
    ‖A‖₊ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖₊

Proof state:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖∑ i_1 : n, A i i_1 * x i_1‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
  nnnorm_one, mul_one] at hN

Result:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
⊢ ‖x‖₊ = 1

Tactic:
simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]

Result:
no goals

Proof state:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
hxn : ‖x‖₊ = 1
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
specialize hN x

Result:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Proof state:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
classical
let x : n → α := fun j => unitOf (A i j)
have hxn : ‖x‖₊ = 1 := by
  simp_rw [x, Pi.nnnorm_def, norm_unitOf, Finset.sup_const Finset.univ_nonempty]
specialize hN x
rw [hxn, mul_one, Pi.nnnorm_def, Finset.sup_le_iff] at hN
replace hN := hN i (Finset.mem_univ _)
dsimp [mulVec, dotProduct] at hN
simp_rw [x, mul_unitOf, ← map_sum, nnnorm_algebraMap, ← NNReal.coe_sum, NNReal.nnnorm_eq,
  nnnorm_one, mul_one] at hN
exact hN

Result:
no goals

Proof state:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j => Matrix.unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ∑ i_1 : n, ‖A i i_1‖₊ ≤ N
⊢ ∑ j : n, ‖A i j‖₊ ≤ N

Tactic:
exact hN

Result:
no goals