case h
ι : Sort ?u.217461
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ e ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔ e ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
ι : Sort ?u.217461
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
⊢ Subgraph.edgeSet (subgraphOfAdj G hvw) = {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
ext e
case h
ι : Sort ?u.217461
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
case h
ι : Sort ?u.217461
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ e ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔ e ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
refine' e.ind _
no goals
case h
ι : Sort ?u.217461
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v w : V
hvw : Adj G v w
e : Sym2 V
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ Subgraph.edgeSet (subgraphOfAdj G hvw) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ {Quotient.mk (Sym2.Rel.setoid V) (v, w)}
simp only [eq_comm, Set.mem_singleton_iff, Subgraph.mem_edgeSet, subgraphOfAdj_Adj, iff_self_iff,
  forall₂_true_iff]