V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Lᶜ)) C = C
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ hom (_ : L ⊆ L) C = C
change C.map _ = C
no goals
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Lᶜ)) C = C
erw [induceHom_id G (Lᶜ), ConnectedComponent.map_id]