ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
⊢ (v ≠ w ∧ ∃ e, e ∈ edgeSet G ∧ v ∈ e ∧ w ∈ e) → Adj G v w
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
⊢ Adj G v w ↔ v ≠ w ∧ ∃ e, e ∈ edgeSet G ∧ v ∈ e ∧ w ∈ e
refine' ⟨fun _ => ⟨G.ne_of_adj ‹_›, ⟦(v, w)⟧, by simpa⟩, _⟩
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ edgeSet G
hv : v ∈ e ∧ w ∈ e
⊢ Adj G v w
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
⊢ (v ≠ w ∧ ∃ e, e ∈ edgeSet G ∧ v ∈ e ∧ w ∈ e) → Adj G v w
rintro ⟨hne, e, he, hv⟩
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ edgeSet G
hv : e = Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ Adj G v w
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ edgeSet G
hv : v ∈ e ∧ w ∈ e
⊢ Adj G v w
rw [Sym2.mem_and_mem_iff hne] at hv
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ Adj G v w
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
e : Sym2 V
he : e ∈ edgeSet G
hv : e = Quotient.mk (Sym2.Rel.setoid V) (v, w)
⊢ Adj G v w
subst e
no goals
case intro.intro.intro
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
hne : v ≠ w
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ Adj G v w
rwa [mem_edgeSet] at he
no goals
ι : Sort ?u.71588
𝕜 : Type ?u.71591
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
G₁ G₂ : SimpleGraph V
v w : V
x✝ : Adj G v w
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G ∧
    v ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∧ w ∈ Quotient.mk (Sym2.Rel.setoid V) (v, w)
simpa