no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.36632
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f✝ g : C(α, β)
f : C(β, γ)
g₁ g₂ : C(α, β)
hf : Injective ↑f
h : comp f g₁ = comp f g₂
a : α
⊢ ↑f (↑g₁ a) = ↑f (↑g₂ a)
rw [← comp_apply, h, comp_apply]