case verts.h
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (subgraphOfAdj G hvw)).verts ↔ x✝ ∈ (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))).verts

case Adj.h.h.a
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ Subgraph.Adj (Subgraph.map f (subgraphOfAdj G hvw)) x✝¹ x✝ ↔
    Subgraph.Adj (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))) x✝¹ x✝
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ Subgraph.map f (subgraphOfAdj G hvw) = subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))
ext
case verts.h
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) ↔ x✝ = ↑f v ∨ x✝ = ↑f w
case verts.h
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (subgraphOfAdj G hvw)).verts ↔ x✝ ∈ (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))).verts
simp only [Subgraph.map_verts, subgraphOfAdj_verts, Set.mem_image, Set.mem_insert_iff,
  Set.mem_singleton_iff]
case verts.h.mp
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) → x✝ = ↑f v ∨ x✝ = ↑f w

case verts.h.mpr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ = ↑f v ∨ x✝ = ↑f w → ∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝
case verts.h
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) ↔ x✝ = ↑f v ∨ x✝ = ↑f w
constructor
no goals
case verts.h.mp
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝) → x✝ = ↑f v ∨ x✝ = ↑f w
rintro ⟨u, rfl | rfl, rfl⟩ <;> simp
case verts.h.mpr.inl
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f v

case verts.h.mpr.inr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f w
case verts.h.mpr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝ : W
⊢ x✝ = ↑f v ∨ x✝ = ↑f w → ∃ x, (x = v ∨ x = w) ∧ ↑f x = x✝
rintro (rfl | rfl)
case verts.h.mpr.inl
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∨ v = w) ∧ ↑f v = ↑f v
case verts.h.mpr.inl
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f v
use v
no goals
case verts.h.mpr.inl
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∨ v = w) ∧ ↑f v = ↑f v
simp
case verts.h.mpr.inr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (w = v ∨ w = w) ∧ ↑f w = ↑f w
case verts.h.mpr.inr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ x, (x = v ∨ x = w) ∧ ↑f x = ↑f w
use w
no goals
case verts.h.mpr.inr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (w = v ∨ w = w) ∧ ↑f w = ↑f w
simp
case Adj.h.h.a
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹
case Adj.h.h.a
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ Subgraph.Adj (Subgraph.map f (subgraphOfAdj G hvw)) x✝¹ x✝ ↔
    Subgraph.Adj (subgraphOfAdj G' (_ : Adj G' (↑f v) (↑f w))) x✝¹ x✝
simp only [Relation.Map, Subgraph.map_Adj, subgraphOfAdj_Adj, Quotient.eq, Sym2.rel_iff]
case Adj.h.h.a.mp
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) → ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹

case Adj.h.h.a.mpr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹ → ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
case Adj.h.h.a
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) ↔ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹
constructor
no goals
case Adj.h.h.a.mp
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ (∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝) → ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹
rintro ⟨a, b, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl, rfl⟩ <;> simp
case Adj.h.h.a.mpr.inl.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f v ∧ ↑f b = ↑f w

case Adj.h.h.a.mpr.inr.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f w ∧ ↑f b = ↑f v
case Adj.h.h.a.mpr
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
x✝¹ x✝ : W
⊢ ↑f v = x✝¹ ∧ ↑f w = x✝ ∨ ↑f v = x✝ ∧ ↑f w = x✝¹ → ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = x✝¹ ∧ ↑f b = x✝
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
case Adj.h.h.a.mpr.inl.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ ↑f v = ↑f v ∧ ↑f w = ↑f w
case Adj.h.h.a.mpr.inl.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f v ∧ ↑f b = ↑f w
use v, w
no goals
case Adj.h.h.a.mpr.inl.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ ↑f v = ↑f v ∧ ↑f w = ↑f w
simp
case Adj.h.h.a.mpr.inr.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = w ∧ w = v ∨ v = v ∧ w = w) ∧ ↑f w = ↑f w ∧ ↑f v = ↑f v
case Adj.h.h.a.mpr.inr.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ ↑f a = ↑f w ∧ ↑f b = ↑f v
use w, v
no goals
case Adj.h.h.a.mpr.inr.intro
ι : Sort ?u.219034
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : Adj G v w
⊢ (v = w ∧ w = v ∨ v = v ∧ w = w) ∧ ↑f w = ↑f w ∧ ↑f v = ↑f v
simp