case preconnected
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v : V
⊢ Preconnected (Subgraph.coe (SimpleGraph.singletonSubgraph G v))
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v : V
⊢ Subgraph.Connected (SimpleGraph.singletonSubgraph G v)
constructor
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v a : V
ha : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb : b ∈ (SimpleGraph.singletonSubgraph G v).verts
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha } { val := b, property := hb }
case preconnected
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v : V
⊢ Preconnected (Subgraph.coe (SimpleGraph.singletonSubgraph G v))
rintro ⟨a, ha⟩ ⟨b, hb⟩
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v a : V
ha✝ : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb✝ : b ∈ (SimpleGraph.singletonSubgraph G v).verts
ha : a = v
hb : b = v
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha✝ }
    { val := b, property := hb✝ }
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v a : V
ha : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb : b ∈ (SimpleGraph.singletonSubgraph G v).verts
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha } { val := b, property := hb }
simp only [singletonSubgraph_verts, Set.mem_singleton_iff] at ha hb
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
b : V
ha hb : b = b
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G b)) { val := b, property := (_ : b = b) }
    { val := b, property := (_ : b = b) }
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v a : V
ha✝ : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb✝ : b ∈ (SimpleGraph.singletonSubgraph G v).verts
ha : a = v
hb : b = v
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha✝ }
    { val := b, property := hb✝ }
subst_vars
no goals
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
b : V
ha hb : b = b
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G b)) { val := b, property := (_ : b = b) }
    { val := b, property := (_ : b = b) }
rfl