case h
ι : Sort ?u.109989
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sSup s) ↔ e ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
ι : Sort ?u.109989
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ edgeSet (sSup s) = ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
ext e
case h.h
ι : Sort ?u.109989
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sSup s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
case h
ι : Sort ?u.109989
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sSup s) ↔ e ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
induction e using Sym2.ind
no goals
case h.h
ι : Sort ?u.109989
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sSup s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G'
simp