sorry
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Injective fun H' => ⟨(↑H').hom.comp ⋯.some.toHom, ⋯⟩
no goals