case a
ι : Sort ?u.277119
𝕜 : Type ?u.277122
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e✝ : Sym2 V
inst✝² : Fintype ↑(neighborSet G v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
e : Sym2 V
⊢ e ∈ incidenceFinset G v ↔ e ∈ filter (Membership.mem v) (edgeFinset G)
ι : Sort ?u.277119
𝕜 : Type ?u.277122
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝² : Fintype ↑(neighborSet G v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
⊢ incidenceFinset G v = filter (Membership.mem v) (edgeFinset G)
ext e
case a
ι : Sort ?u.277119
𝕜 : Type ?u.277122
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e✝ : Sym2 V
inst✝² : Fintype ↑(neighborSet G v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
e : Sym2 V
x y : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ incidenceFinset G v ↔
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ filter (Membership.mem v) (edgeFinset G)
case a
ι : Sort ?u.277119
𝕜 : Type ?u.277122
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e✝ : Sym2 V
inst✝² : Fintype ↑(neighborSet G v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
e : Sym2 V
⊢ e ∈ incidenceFinset G v ↔ e ∈ filter (Membership.mem v) (edgeFinset G)
refine' Sym2.ind (fun x y => _) e
no goals
case a
ι : Sort ?u.277119
𝕜 : Type ?u.277122
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e✝ : Sym2 V
inst✝² : Fintype ↑(neighborSet G v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
e : Sym2 V
x y : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ incidenceFinset G v ↔
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ filter (Membership.mem v) (edgeFinset G)
simp [mk'_mem_incidenceSet_iff]