case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
⊢ Nonempty (G →g F)
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
⊢ Nonempty (G →g F)
cases nonempty_fintype W
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
⊢ Nonempty (G →g F)
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Nonempty ((finsubgraphHomFunctor G F).obj G') := fun G' =>
  ⟨h G'.unop G'.unop.property⟩
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
haveI : ∀ G' : G.Finsubgraphᵒᵖ, Fintype ((finsubgraphHomFunctor G F).obj G') := by
  intro G'
  haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
  haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
  exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
case intro.intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
⊢ Nonempty (G →g F)
case intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
⊢ Nonempty (G →g F)
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_inverse_system (finsubgraphHomFunctor G F)
case intro.intro.refine'_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ W

case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
⊢ ∀ {a b : V}, Adj G a b → Adj F ((fun v => ?m.26519 v) a) ((fun v => ?m.26519 v) b)
case intro.intro
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
⊢ Nonempty (G →g F)
refine' ⟨⟨fun v => _, _⟩⟩
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
⊢ (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
intro G'
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
haveI : Fintype (G'.unop.val.verts : Type u) := G'.unop.property.fintype
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this✝ : Fintype ↑(↑G'.unop).verts
this : Fintype (↑(↑G'.unop).verts → W)
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
haveI : Fintype (↥G'.unop.val.verts → W) := by classical exact Pi.fintype
no goals
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝¹ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this✝ : Fintype ↑(↑G'.unop).verts
this : Fintype (↑(↑G'.unop).verts → W)
⊢ Fintype ((finsubgraphHomFunctor G F).obj G')
exact Fintype.ofInjective (fun f => f.toFun) RelHom.coe_fn_injective
no goals
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
classical exact Pi.fintype
no goals
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
G' : (Finsubgraph G)ᵒᵖ
this : Fintype ↑(↑G'.unop).verts
⊢ Fintype (↑(↑G'.unop).verts → W)
exact Pi.fintype
no goals
case intro.intro.refine'_1
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ W
exact
  (u (Opposite.op (singletonFinsubgraph v))).toFun
    ⟨v, by
      unfold singletonFinsubgraph
      simp⟩
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑{ val := SimpleGraph.singletonSubgraph G v, property := (_ : Set.Finite {v}) }.op.unop).verts
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑(singletonFinsubgraph v).op.unop).verts
unfold singletonFinsubgraph
no goals
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v : V
⊢ v ∈ (↑{ val := SimpleGraph.singletonSubgraph G v, property := (_ : Set.Finite {v}) }.op.unop).verts
simp
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    ((fun v =>
        RelHom.toFun (u (singletonFinsubgraph v).op)
          { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
      v)
    ((fun v =>
        RelHom.toFun (u (singletonFinsubgraph v).op)
          { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
      v')
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
⊢ ∀ {a b : V},
    Adj G a b →
      Adj F
        ((fun v =>
            RelHom.toFun (u (singletonFinsubgraph v).op)
              { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
          a)
        ((fun v =>
            RelHom.toFun (u (singletonFinsubgraph v).op)
              { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
          b)
intro v v' e
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    ((fun v =>
        RelHom.toFun (u (singletonFinsubgraph v).op)
          { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
      v)
    ((fun v =>
        RelHom.toFun (u (singletonFinsubgraph v).op)
          { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
      v')
simp only
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
  Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj F
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv (u (finsubgraphOfAdj e).op))
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv' (u (finsubgraphOfAdj e).op))
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj F
    (RelHom.toFun (u (singletonFinsubgraph v).op)
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun (u (singletonFinsubgraph v').op)
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
rw [← hu hv, ← hu hv']
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj (Subgraph.coe ↑(finsubgraphOfAdj e).op.unop)
    { val := v, property := (_ : v ∈ (↑(finsubgraphOfAdj e).op.unop).verts) }
    { val := v', property := (_ : v' ∈ (↑(finsubgraphOfAdj e).op.unop).verts) }
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj F
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv (u (finsubgraphOfAdj e).op))
      { val := v, property := (_ : v ∈ (↑(singletonFinsubgraph v).op.unop).verts) })
    (RelHom.toFun ((finsubgraphHomFunctor G F).map hv' (u (finsubgraphOfAdj e).op))
      { val := v', property := (_ : v' ∈ (↑(singletonFinsubgraph v').op.unop).verts) })
refine' Hom.map_adj (u (Opposite.op (finsubgraphOfAdj e))) _
no goals
case intro.intro.refine'_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : Subgraph G) → Set.Finite G'.verts → Subgraph.coe G' →g F
val✝ : Fintype W
this✝ : ∀ (G' : (Finsubgraph G)ᵒᵖ), Nonempty ((finsubgraphHomFunctor G F).obj G')
this : (G' : (Finsubgraph G)ᵒᵖ) → Fintype ((finsubgraphHomFunctor G F).obj G')
u : (j : (Finsubgraph G)ᵒᵖ) → (finsubgraphHomFunctor G F).obj j
hu : u ∈ CategoryTheory.Functor.sections (finsubgraphHomFunctor G F)
v v' : V
e : Adj G v v'
hv : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v).op
hv' : (finsubgraphOfAdj e).op ⟶ (singletonFinsubgraph v').op
⊢ Adj (Subgraph.coe ↑(finsubgraphOfAdj e).op.unop)
    { val := v, property := (_ : v ∈ (↑(finsubgraphOfAdj e).op.unop).verts) }
    { val := v', property := (_ : v' ∈ (↑(finsubgraphOfAdj e).op.unop).verts) }
simp [finsubgraphOfAdj]