Theorem: SimpleGraph.Subgraph.map_id (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 α
G' : G.Subgraph
⊢ Subgraph.map Hom.id G' = G'
Tactic:
ext <;> simp
State after:
no goals