-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma norm_entry_le_norm {M : CStarMatrix m n A} {i : m} {j : n} :
    ‖M i j‖ ≤ ‖M‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv (n → A)).symm (Pi.single j (star (M i j))))‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
apply (toCLM M).le_opNorm _ |>.trans

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖toCLM M‖ * ‖(equiv (n → A)).symm (Pi.single j (star (M i j)))‖ ≤ ‖M‖ * ‖M i j‖

Proof state:
case inr
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
exact le_of_mul_le_mul_right this h

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖toCLM M‖ * ‖(equiv (n → A)).symm (Pi.single j (star (M i j)))‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
simp [norm_def]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
rw [← CStarRing.norm_self_mul_star, ← toCLM_apply_single_apply]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv (n → A)).symm (Pi.single j (star (M i j)))) i‖ ≤ ‖M‖ * ‖M i j‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv (n → A)).symm (Pi.single j (star (M i j)))) i‖ ≤ ‖M‖ * ‖M i j‖

Tactic:
apply norm_apply_le_norm _ _ |>.trans

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
⊢ ‖(toCLM M) ((equiv (n → A)).symm (Pi.single j (star (M i j))))‖ ≤ ‖M‖ * ‖M i j‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
obtain (h | h) := eq_zero_or_norm_pos (M i j)

Result:
case inl
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : M i j = 0
⊢ ‖M i j‖ ≤ ‖M‖

case inr
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : 0 < ‖M i j‖
⊢ ‖M i j‖ ≤ ‖M‖

Proof state:
case inl
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : M i j = 0
⊢ ‖M i j‖ ≤ ‖M‖

Tactic:
simp [h, norm_def]

Result:
case inl
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
i : m
j : n
this : ‖M i j‖ * ‖M i j‖ ≤ ‖M‖ * ‖M i j‖
h : M i j = 0
⊢ 0 ≤ ‖toCLM M‖