rw [Sym2.map_map, Set.mem_singleton_iff, ← he₁]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map Subtype.val e' ∈ {⋯.some}
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
hH' : (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hH'.some
e' : Sym2 ↑H'.verts := Sym2.map (⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' H'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ H.edgeSet ∧
    ∀ (x : H.Subgraph) (x_1 : Nonempty (G ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ Sym2.map (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) e = Sym2.map Subtype.val e