Theorem: SimpleGraph.aux (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 ≠ ⊥
H' : H.Subgraph
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty
Tactic:
obtain ⟨e, he⟩ := edgeSet_nonempty.2 hG
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.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty

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.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → H'.edgeSet.Nonempty
Tactic:
rw [← Subgraph.image_coe_edgeSet_coe]
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.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → (Sym2.map Subtype.val '' H'.coe.edgeSet).Nonempty

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.Subgraph
e : Sym2 α
he : e ∈ G.edgeSet
⊢ Nonempty (G ≃g H'.coe) → (Sym2.map Subtype.val '' H'.coe.edgeSet).Nonempty
Tactic:
exact fun ⟨f⟩ ↦ Set.Nonempty.image _ ⟨_, f.map_mem_edgeSet_iff.2 he⟩
State after:
no goals