ext <;> simp [Subgraph.map]
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G✝ H✝ : SimpleGraph V
G : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
G' : G.Subgraph
f : G →g H
g : H →g I
⊢ Subgraph.map (g.comp f) G' = Subgraph.map g (Subgraph.map f G')
no goals