∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : SpectralMap β γ} {f₁ f₂ : SpectralMap α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂) = (f₁ = f₂)