Theorem: SimpleGraph.not_isContained_kill (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬G ⊑ G.kill H
Tactic:
rw [kill_of_ne_bot hG, deleteEdges, isContained_iff_exists_subgraph]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬∃ H', Nonempty (G ≃g H'.coe)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
⊢ ¬∃ H', Nonempty (G ≃g H'.coe)
Tactic:
rintro ⟨H', hGH'⟩
State after:
case 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)
⊢ False

State before:
case 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)
⊢ False
Tactic:
have hH' : (H'.map $ Hom.ofLE (sdiff_le : H \ _ ≤ H)).edgeSet.Nonempty := by
  rw [Subgraph.edgeSet_map]
  exact (aux hG hGH').image _
State after:
case 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
⊢ False

State before:
case 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
⊢ False
Tactic:
set e := hH'.some with he
State after:
case 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 β := hH'.some
he : e = hH'.some
⊢ False

State before:
case 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 β := hH'.some
he : e = hH'.some
⊢ False
Tactic:
have : e ∈ _ := hH'.some_mem
State after:
case 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 β := hH'.some
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False

State before:
case 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 β := hH'.some
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Tactic:
clear_value e
State after:
case 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 β
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False

State before:
case 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 β
he : e = hH'.some
this : e ∈ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet
⊢ False
Tactic:
rw [← Subgraph.image_coe_edgeSet_coe] at this
State after:
case 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 β
he : e = hH'.some
this : e ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False

State before:
case 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 β
he : e = hH'.some
this : e ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Tactic:
subst he
State after:
case 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
this : hH'.some ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False

State before:
case 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
this : hH'.some ∈ Sym2.map Subtype.val '' (Subgraph.map (Hom.ofLE ⋯) H').coe.edgeSet
⊢ False
Tactic:
obtain ⟨e, he₀, he₁⟩ := this
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
let e' : Sym2 H'.verts := Sym2.map (Subgraph.isoMap (Hom.ofLE _) injective_id _).symm e
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have he' : e' ∈ H'.coe.edgeSet := (Iso.map_mem_edgeSet_iff _).2 he₀
State after:
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' ∈ H'.coe.edgeSet
⊢ False

State before:
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' ∈ H'.coe.edgeSet
⊢ False
Tactic:
rw [Subgraph.edgeSet_coe] at he'
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have := Subgraph.edgeSet_subset _ he'
State after:
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).edgeSet
⊢ False

State before:
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 \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).edgeSet
⊢ False
Tactic:
simp only [edgeSet_sdiff,  edgeSet_fromEdgeSet,  edgeSet_sdiff_sdiff_isDiag, Set.mem_diff,
  Set.mem_iUnion, not_exists] at this
State after:
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}
⊢ False

State before:
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}
⊢ False
Tactic:
refine' this.2 (H'.map $ Hom.ofLE sdiff_le)
  ⟨(Subgraph.isoMap (Hom.ofLE _) injective_id _).comp hGH'.some⟩ _
State after:
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}

State before:
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}
Tactic:
rw [Sym2.map_map, Set.mem_singleton_iff, ← he₁]
State after:
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

State before:
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
Tactic:
congr 1 with x
State after:
case intro.intro.intro.e_f.h
α : 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}
x : ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
⊢ (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) x = ↑x

State before:
case intro.intro.intro.e_f.h
α : 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}
x : ↑(Subgraph.map (Hom.ofLE ⋯) H').verts
⊢ (Subtype.val ∘ ⇑(Subgraph.isoMap (Hom.ofLE ⋯) ⋯ H').symm) x = ↑x
Tactic:
refine' congr_arg (↑) (Equiv.Set.image_symm_apply _ _ injective_id _ _)
State after:
no goals

State before:
α : 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)
⊢ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
Tactic:
rw [Subgraph.edgeSet_map]
State after:
α : 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)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' H'.edgeSet).Nonempty

State before:
α : 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)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' H'.edgeSet).Nonempty
Tactic:
exact (aux hG hGH').image _
State after:
no goals