case h
ι : Sort ?u.163733
𝕜 : Type ?u.163736
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
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s
ι : Sort ?u.163733
𝕜 : Type ?u.163736
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
s : Set (Sym2 V)
⊢ edgeSet (deleteEdges G s) = edgeSet G \ s
ext e
case h
ι : Sort ?u.163733
𝕜 : Type ?u.163736
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
s : Set (Sym2 V)
e : Sym2 V
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet (deleteEdges G s) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet G \ s
case h
ι : Sort ?u.163733
𝕜 : Type ?u.163736
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
s : Set (Sym2 V)
e : Sym2 V
⊢ e ∈ edgeSet (deleteEdges G s) ↔ e ∈ edgeSet G \ s
refine' Sym2.ind _ e
no goals
case h
ι : Sort ?u.163733
𝕜 : Type ?u.163736
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
s : Set (Sym2 V)
e : Sym2 V
⊢ ∀ (x y : V),
    Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet (deleteEdges G s) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet G \ s
simp