simp [Relation.map_apply_apply, f.injective]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
f : G ↪g H
a b : α
⊢ H.Adj (f.toHom a) (f.toHom b) → (Subgraph.map f.toHom ⊤).Adj (f.toHom a) (f.toHom b)
no goals