-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma norm_le_of_forall_inner_le {M : CStarMatrix m n A} {C : ℝ≥0}
    (h : ∀ v w, ‖⟪w, toCLM M v⟫_A‖ ≤ C * ‖v‖ * ‖w‖) : ‖M‖ ≤ C

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ 0 ≤ ↑C * ‖v‖

Tactic:
positivity

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
⊢ 0 ≤ ↑C

Tactic:
simp

Result:
no goals

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 < ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ * ‖(toCLM M) v‖ ≤ ↑C * ‖v‖ * ‖(toCLM M) v‖

Tactic:
simpa [← sq, norm_sq_eq] using 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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

Tactic:
obtain (h₀ | h₀) := (norm_nonneg (toCLM M v)).eq_or_lt

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 < ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 < ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

Tactic:
refine le_of_mul_le_mul_right ?_ h₀

Result:
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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 < ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ * ‖(toCLM M) v‖ ≤ ↑C * ‖v‖ * ‖(toCLM M) v‖

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
⊢ ‖M‖ ≤ ↑C

Tactic:
refine (toCLM M).opNorm_le_bound (by simp) fun v ↦ ?_

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

Tactic:
rw [← h₀]

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
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ (n → A)) (w : C⋆ᵐᵒᵈ (m → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ (n → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ 0 ≤ ↑C * ‖v‖