case H
V : Type u_1
W : Type u_2
V₁ : Type ?u.501676
V₂ : Type ?u.501679
V₃ : Type ?u.501682
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.501714
W₂ : Type ?u.501717
W₃ : Type ?u.501720
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
x : { x // x ∈ equalizer f g }
⊢ ↑(NormedAddGroupHom.comp f (ι f g)) x = ↑(NormedAddGroupHom.comp g (ι f g)) x
V : Type u_1
W : Type u_2
V₁ : Type ?u.501676
V₂ : Type ?u.501679
V₃ : Type ?u.501682
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.501714
W₂ : Type ?u.501717
W₃ : Type ?u.501720
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
⊢ NormedAddGroupHom.comp f (ι f g) = NormedAddGroupHom.comp g (ι f g)
ext x
case H
V : Type u_1
W : Type u_2
V₁ : Type ?u.501676
V₂ : Type ?u.501679
V₃ : Type ?u.501682
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.501714
W₂ : Type ?u.501717
W₃ : Type ?u.501720
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
x : { x // x ∈ equalizer f g }
⊢ ↑(f - g) (↑(ι f g) x) = 0
case H
V : Type u_1
W : Type u_2
V₁ : Type ?u.501676
V₂ : Type ?u.501679
V₃ : Type ?u.501682
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.501714
W₂ : Type ?u.501717
W₃ : Type ?u.501720
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
x : { x // x ∈ equalizer f g }
⊢ ↑(NormedAddGroupHom.comp f (ι f g)) x = ↑(NormedAddGroupHom.comp g (ι f g)) x
rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]
no goals
case H
V : Type u_1
W : Type u_2
V₁ : Type ?u.501676
V₂ : Type ?u.501679
V₃ : Type ?u.501682
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.501714
W₂ : Type ?u.501717
W₃ : Type ?u.501720
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
x : { x // x ∈ equalizer f g }
⊢ ↑(f - g) (↑(ι f g) x) = 0
exact x.2