V : Type u_1
V₁ : Type ?u.320008
V₂ : Type ?u.320011
V₃ : Type ?u.320014
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖
V : Type u_1
V₁ : Type ?u.320008
V₂ : Type ?u.320011
V₃ : Type ?u.320014
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
h : ∃ x, ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖
let ⟨x, hx⟩ := h
V : Type u_1
V₁ : Type ?u.320008
V₂ : Type ?u.320011
V₃ : Type ?u.320014
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
this : ‖↑(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
V : Type u_1
V₁ : Type ?u.320008
V₂ : Type ?u.320011
V₃ : Type ?u.320014
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖
have := (id V).ratio_le_opNorm x
no goals
V : Type u_1
V₁ : Type ?u.320008
V₂ : Type ?u.320011
V₃ : Type ?u.320014
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
this : ‖↑(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
rwa [id_apply, div_self hx] at this