Theorem: SimpleGraph.Subgraph.edgeSet_coe (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
ext e
State after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

State before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
e : Sym2 ↑G'.verts
⊢ e ∈ G'.coe.edgeSet ↔ e ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
induction' e using Sym2.ind with a b
State after:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : ↑G'.verts
⊢ s(a, b) ∈ G'.coe.edgeSet ↔ s(a, b) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet

State before:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
V : Type u_4
G H : SimpleGraph V
G' : G.Subgraph
a b : ↑G'.verts
⊢ s(a, b) ∈ G'.coe.edgeSet ↔ s(a, b) ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
Tactic:
simp
State after:
no goals