V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ (∀ (L : Finset V) (h : K.unop ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom (_ : K.unop ≤ i.unop) y = C
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ Set.Infinite (ComponentCompl.supp C) ↔ C ∈ Functor.eventualRange (componentComplFunctor G) K
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
  Set.mem_range, componentComplFunctor_map]
no goals
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ (∀ (L : Finset V) (h : K.unop ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom (_ : K.unop ≤ i.unop) y = C
exact
  ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
    h (Opposite.op L) (opHomOfLE KL)⟩