V : Type ?u.110454
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.110463
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
x : V₁
⊢ ↑f x = ↑f x
V : Type ?u.110454
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.110463
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ f = g → ∀ (x : V₁), ↑f x = ↑g x
rintro rfl x
no goals
V : Type ?u.110454
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.110463
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
x : V₁
⊢ ↑f x = ↑f x
rfl