is another, possibly more convenient, way to put it.

We were considering it before making the PR, but decided to stick with the more verbose notation.

I prefer the original notation: I feel it's a bit more transparent; e.g. when C := G.connected_component_mk v, membership is clear rfl while with the other notation you have (well, at least I do) to think to convince yourself that it unfolds to a rfl.

In one of my branches I had written connected_component_mk ⁻¹' {c} directly, but since we're developing this API for the support of a connected component, I'm happy with { v | G.connected_component_mk v = C }.

I would turn this one around

You can look at order_iso.symm_apply_le for a better naming convention.

The following is valid syntax

You can pull a few more variables out

Is there a reason for G to be explicit here? If not, could you please make it be implicit?

Also, I think the proof would be nicer as connected_component.sound a.reachable.

Further, you could leverage dot notation on adj.

Make sure to use the coercion for φ rather than φ.to_hom. There are some extraneous parenthesis as well, and note that you can combine the last two lines of the proof (you can squeeze it if you want).

The last two lines of the proof can be merged as simp [iso.symm_apply_reachable]

In one of my branches I had written connected_component_mk ⁻¹' {c} directly, but since we're developing this API for the support of a connected component, I'm happy with { v | G.connected_component_mk v = C }.

Here's perhaps less of a technical proof? In any case, I think the last line would be nice.

Maybe G should be implicit?

Just to nitpick, you can do this:

I haven't tested this, but these should work, and it would be preferred:

I don't think this lemma is ready for the library. To do it right, we should have supporting theory for relating walks in G.induce s to walks whose support is contained in s.

I started writing

def induce_lift (s : set V) : Π {v w : V} (p : G.walk v w) (h : ∀ u, u ∈ p.support → u ∈ s),
  (G.induce s).walk ⟨v, h v p.start_mem_support⟩ ⟨w, h w p.end_mem_support⟩
| _ _ walk.nil _ := walk.nil
| _ _ (walk.cons' u v w ha p) h :=
  let p' := induce_lift p (λ x hx, h x (by simp [hx]))
  in walk.cons (by exact ha) p'

but fleshing everything out would take some time. Would you be ok with removing the lemma for now?

Thanks for the review! I agree having a more general theory for mapping walks back and forth would be better (this is how we handled it before), but at the same time the lemma works as-is and can be made to use this API when it gets there…
Since it's needed to make progress on Freudenthal-Hopf, I'd rather have it there, but I understand if you don't want to introduce "half-baked" results in simple_graph.*. Your call in any case :)

I get that it works as-is, but at least for now it seems somewhat out of place from the rest of the PR.

I'm dusting off some things I have in a branch to make use of what you have here. I've said it before, but I suspect a number of things are cleaner through subgraphs rather than induced graphs (or at least, if you want to work with induced graphs, they can follow from facts about subgraphs).

In the meantime, would you be ok keeping this lemma in your Freudenthal-Hopf project?

Yeah, works for me :) (I'm not doing any changes (yet?) since @0art0 might want to pitch in first and/or do the changes themselves).