V : Type ?u.494024
W : Type ?u.494027
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.494036
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ AddMonoidHom.range (toAddMonoidHom f) = range f
V : Type ?u.494024
W : Type ?u.494027
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.494036
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ range (NormedAddGroupHom.comp f (incl ⊤)) = range f
simp [comp_range, incl_range, ← AddMonoidHom.range_eq_map]
no goals
V : Type ?u.494024
W : Type ?u.494027
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.494036
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ AddMonoidHom.range (toAddMonoidHom f) = range f
rfl