rintro ⟨f, hf⟩
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
⊢ G ⊑ H → ∃ H', Nonempty (G ≃g H'.coe)
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G →g H
hf : Injective ⇑f
⊢ ∃ H', Nonempty (G ≃g H'.coe)