Theorem: SimpleGraph.Subgraph.map_comp (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean)

State before:
α : 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')
Tactic:
ext <;> simp [Subgraph.map]
State after:
no goals