case refine'_1
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : NormNoninc f
⊢ ‖f‖ ≤ 1

case refine'_2
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ ‖↑f v‖ ≤ ‖v‖
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
⊢ NormNoninc f ↔ ‖f‖ ≤ 1
refine' ⟨fun h => _, fun h => fun v => _⟩
case refine'_1
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : NormNoninc f
v : V
⊢ ‖↑f v‖ ≤ 1 * ‖v‖
case refine'_1
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : NormNoninc f
⊢ ‖f‖ ≤ 1
refine' opNorm_le_bound _ zero_le_one fun v => _
no goals
case refine'_1
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : NormNoninc f
v : V
⊢ ‖↑f v‖ ≤ 1 * ‖v‖
simpa [one_mul] using h v
no goals
case refine'_2
V : Type u_1
W : Type u_2
V₁ : Type ?u.495566
V₂ : Type ?u.495569
V₃ : Type ?u.495572
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ ‖↑f v‖ ≤ ‖v‖
simpa using le_of_opNorm_le f h v