case h
V : Type ?u.485691
W : Type ?u.485694
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.485703
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ x✝ ∈ ker 0 ↔ x✝ ∈ ⊤
V : Type ?u.485691
W : Type ?u.485694
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.485703
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ ker 0 = ⊤
ext
no goals
case h
V : Type ?u.485691
W : Type ?u.485694
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.485703
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ x✝ ∈ ker 0 ↔ x✝ ∈ ⊤
simp [mem_ker]