V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (InduceHom Hom.id (_ : Kᶜ ⊆ Mᶜ)) (ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Kᶜ)) C)
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ hom (_ : M ⊆ L) C = hom h' (hom h C)
change C.map _ = (C.map _).map _
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map
      (InduceHom (Hom.comp Hom.id Hom.id) (_ : Set.MapsTo (↑Hom.id ∘ fun x => ↑Hom.id x) (Lᶜ) (Mᶜ))) C
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (InduceHom Hom.id (_ : Kᶜ ⊆ Mᶜ)) (ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Kᶜ)) C)
erw [ConnectedComponent.map_comp, induceHom_comp]
no goals
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (InduceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map
      (InduceHom (Hom.comp Hom.id Hom.id) (_ : Set.MapsTo (↑Hom.id ∘ fun x => ↑Hom.id x) (Lᶜ) (Mᶜ))) C
rfl