V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
⊢ ∀ (v w : V),
    supp (connectedComponentMk G v) = supp (connectedComponentMk G w) →
      connectedComponentMk G v = connectedComponentMk G w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
⊢ Injective supp
refine' ConnectedComponent.ind₂ _
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ supp (connectedComponentMk G v) = supp (connectedComponentMk G w) →
    connectedComponentMk G v = connectedComponentMk G w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
⊢ ∀ (v w : V),
    supp (connectedComponentMk G v) = supp (connectedComponentMk G w) →
      connectedComponentMk G v = connectedComponentMk G w
intro v w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (∀ (x : V), Reachable G x v ↔ Reachable G x w) → Reachable G v w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ supp (connectedComponentMk G v) = supp (connectedComponentMk G w) →
    connectedComponentMk G v = connectedComponentMk G w
simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : ∀ (x : V), Reachable G x v ↔ Reachable G x w
⊢ Reachable G v w
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (∀ (x : V), Reachable G x v ↔ Reachable G x w) → Reachable G v w
intro h
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : ∀ (x : V), Reachable G x v ↔ Reachable G x w
⊢ Reachable G v w
rw [reachable_comm, h]