case h
ι : Sort ?u.80342
𝕜 : Type ?u.80345
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 (fromEdgeSet s) ↔ e ∈ s \ {e | Sym2.IsDiag e}
ι : Sort ?u.80342
𝕜 : Type ?u.80345
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 (fromEdgeSet s) = s \ {e | Sym2.IsDiag e}
ext e
no goals
case h
ι : Sort ?u.80342
𝕜 : Type ?u.80345
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 (fromEdgeSet s) ↔ e ∈ s \ {e | Sym2.IsDiag e}
exact Sym2.ind (by simp) e
no goals
ι : Sort ?u.80342
𝕜 : Type ?u.80345
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 (fromEdgeSet s) ↔
      Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ s \ {e | Sym2.IsDiag e}
simp