-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
private lemma antilipschitzWith_toMatrixAux :
    AntilipschitzWith (Fintype.card m * Fintype.card n)
      (ofMatrixₗ.symm (R := ℂ) : CStarMatrix m n A → Matrix m n A)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∑ i : m, ∑ j : n, ‖M i j‖ ≤ ∑ x : m, ∑ x : n, ‖ofMatrixₗ.symm M‖

Tactic:
gcongr with i _ j _

Result:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j‖ ≤ ‖ofMatrixₗ.symm M‖

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

Tactic:
positivity

Result:
no goals

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

Tactic:
refine (toCLM M).opNorm_le_bound (by positivity) fun v => ?_

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(toCLM M) v‖ ≤ (∑ i : m, ∑ j : n, ‖M i j‖) * ‖v‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖M‖ ≤ ↑(↑(Fintype.card m) * ↑(Fintype.card n)) * ‖ofMatrixₗ.symm M‖

Tactic:
calc
  ‖M‖ ≤ ∑ i, ∑ j, ‖M i j‖ := by
    rw [norm_def]
    refine (toCLM M).opNorm_le_bound (by positivity) fun v => ?_
    simp only [toCLM_apply_eq_sum, equiv_symm_pi_apply, Finset.sum_mul]
    apply pi_norm_le_sum_norm _ |>.trans
    gcongr with i _
    apply norm_sum_le _ _ |>.trans
    gcongr with j _
    apply norm_mul_le _ _ |>.trans
    gcongr
    exact norm_apply_le_norm v j
  _ ≤ ∑ _ : m, ∑ _ : n, ‖ofMatrixₗ.symm (R := ℂ) M‖ := by
    gcongr with i _ j _
    exact ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm
  _ = _ := by simp [mul_assoc]

Result:
no goals

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

Tactic:
rw [norm_def]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ‖toCLM M‖ ≤ ∑ i : m, ∑ j : n, ‖M i j‖

Proof state:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j‖ * ‖v j‖ ≤ ‖M i j‖ * ‖v‖

Tactic:
gcongr

Result:
case h.h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖v j‖ ≤ ‖v‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∑ x : m, ∑ x : n, ‖ofMatrixₗ.symm M‖ = ↑(↑(Fintype.card m) * ↑(Fintype.card n)) * ‖ofMatrixₗ.symm M‖

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(equiv (m → A)).symm fun i => ∑ j : n, M i j * v j‖ ≤ ∑ x : m, ∑ i : n, ‖M x i‖ * ‖v‖

Tactic:
apply pi_norm_le_sum_norm _ |>.trans

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ i : m, ‖(equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i‖ ≤ ∑ x : m, ∑ i : n, ‖M x i‖ * ‖v‖

Proof state:
case h.h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖v j‖ ≤ ‖v‖

Tactic:
exact norm_apply_le_norm v j

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(toCLM M) v‖ ≤ (∑ i : m, ∑ j : n, ‖M i j‖) * ‖v‖

Tactic:
simp only [toCLM_apply_eq_sum, equiv_symm_pi_apply, Finset.sum_mul]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(equiv (m → A)).symm fun i => ∑ j : n, M i j * v j‖ ≤ ∑ x : m, ∑ i : n, ‖M x i‖ * ‖v‖

Proof state:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j‖ ≤ ‖ofMatrixₗ.symm M‖

Tactic:
exact ofMatrixₗ.symm (R := ℂ) M |>.norm_entry_le_entrywise_sup_norm

Result:
no goals

Proof state:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝ : i ∈ Finset.univ
⊢ ‖(equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i‖ ≤ ∑ i_1 : n, ‖M i i_1‖ * ‖v‖

Tactic:
apply norm_sum_le _ _ |>.trans

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝ : i ∈ Finset.univ
⊢ ∑ i_1 : n, ‖M i i_1 * v i_1‖ ≤ ∑ i_1 : n, ‖M i i_1‖ * ‖v‖

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ i : m, ‖(equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i‖ ≤ ∑ x : m, ∑ i : n, ‖M x i‖ * ‖v‖

Tactic:
gcongr with i _

Result:
case h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝ : i ∈ Finset.univ
⊢ ‖(equiv (m → A)).symm (fun i => ∑ j : n, M i j * v j) i‖ ≤ ∑ i_1 : n, ‖M i i_1‖ * ‖v‖

Proof state:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j * v j‖ ≤ ‖M i j‖ * ‖v‖

Tactic:
apply norm_mul_le _ _ |>.trans

Result:
case h.h
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (n → A)
i : m
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖M i j‖ * ‖v j‖ ≤ ‖M i j‖ * ‖v‖