V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ (componentComplFunctor G).map h (componentComplMk G vnL) = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ s K = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
rw [← sec h, hs]
no goals
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ (componentComplFunctor G).map h (componentComplMk G vnL) = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)