case h
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ e' ∈ incidenceSet G v ∩ incidenceSet G (Sym2.Mem.other h) ↔ e' ∈ {e}
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
⊢ incidenceSet G v ∩ incidenceSet G (Sym2.Mem.other h) = {e}
ext e'
case h
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e' ↔ e' = e
case h
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ e' ∈ incidenceSet G v ∩ incidenceSet G (Sym2.Mem.other h) ↔ e' ∈ {e}
simp only [incidenceSet, Set.mem_sep_iff, Set.mem_inter_iff, Set.mem_singleton_iff]
case h.refine'_1
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e

case h.refine'_2
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
case h
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e' ↔ e' = e
refine' ⟨fun h' => _, _⟩
case h.refine'_1
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
⊢ e' = Quotient.mk (Sym2.Rel.setoid V) (v, Sym2.Mem.other h)
case h.refine'_1
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
⊢ e' = e
rw [← Sym2.other_spec h]
no goals
case h.refine'_1
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
h' : (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
⊢ e' = Quotient.mk (Sym2.Rel.setoid V) (v, Sym2.Mem.other h)
exact (Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩
case h.refine'_2
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e' : Sym2 V
he : e' ∈ edgeSet G
h : v ∈ e'
⊢ (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
case h.refine'_2
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e : Sym2 V
he : e ∈ edgeSet G
h : v ∈ e
e' : Sym2 V
⊢ e' = e → (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
rintro rfl
no goals
case h.refine'_2
ι : Sort ?u.138625
𝕜 : Type ?u.138628
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
v : V
e' : Sym2 V
he : e' ∈ edgeSet G
h : v ∈ e'
⊢ (e' ∈ edgeSet G ∧ v ∈ e') ∧ e' ∈ edgeSet G ∧ Sym2.Mem.other h ∈ e'
exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩