ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he : e ∈ edgeSet G'
⊢ v ∈ e → v ∈ G'.verts
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he : e ∈ edgeSet G'
hv : v ∈ e
⊢ v ∈ G'.verts
revert hv
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
⊢ v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w) → v✝ ∈ G'.verts
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he : e ∈ edgeSet G'
⊢ v ∈ e → v ∈ G'.verts
refine' Sym2.ind (fun v w he ↦ _) e he
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v✝ ∈ G'.verts
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
⊢ v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w) → v✝ ∈ G'.verts
intro hv
case inl
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he✝ : e ∈ edgeSet G'
w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v ∈ G'.verts

case inr
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝)
⊢ v✝ ∈ G'.verts
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v✝ ∈ G'.verts
rcases Sym2.mem_iff.mp hv with (rfl | rfl)
no goals
case inl
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v : V
he✝ : e ∈ edgeSet G'
w : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G'
hv : v ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ v ∈ G'.verts
exact G'.edge_vert he
no goals
case inr
ι : Sort ?u.10234
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : Subgraph G
e : Sym2 V
v✝ : V
he✝ : e ∈ edgeSet G'
v : V
he : Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ edgeSet G'
hv : v✝ ∈ Quotient.mk (Sym2.Rel.setoid V) (v, v✝)
⊢ v✝ ∈ G'.verts
exact G'.edge_vert (G'.symm he)