case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
h : K ⊆ L
c : V
cL : ¬c ∈ L
⊢ c ∈ ↑(hom h (componentComplMk G cL))
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ↑C ⊆ ↑(hom h C)
rintro c ⟨cL, rfl⟩
no goals
case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
h : K ⊆ L
c : V
cL : ¬c ∈ L
⊢ c ∈ ↑(hom h (componentComplMk G cL))
exact ⟨fun h' => cL (h h'), rfl⟩