-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem map_subgraphOfAdj (f : G →g G') {v w : V} (hvw : G.Adj v w) :
    Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj (f.map_adj hvw)

Proof state:
case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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✝¹

Tactic:
constructor

Result:
case Adj.h.h.a.mp
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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✝

Proof state:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = v ∨ v = w) ∧ f v = f v

Tactic:
simp

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x✝¹ x✝ ↔ (G'.subgraphOfAdj ⋯).Adj x✝¹ x✝

Tactic:
simp only [Relation.Map, Subgraph.map_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff]

Result:
case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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✝¹

Proof state:
case verts.h.mpr.inr
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ x, (x = v ∨ x = w) ∧ f x = f w

Tactic:
use w

Result:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (w = v ∨ w = w) ∧ f w = f w

Proof state:
case Adj.h.h.a.mpr.inl.intro
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ f a = f v ∧ f b = f w

Tactic:
use v, w

Result:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ f v = f v ∧ f w = f w

Proof state:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = w ∧ w = v ∨ v = v ∧ w = w) ∧ f w = f w ∧ f v = f v

Tactic:
simp

Result:
no goals

Proof state:
case Adj.h.h.a.mpr
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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✝

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Result:
case Adj.h.h.a.mpr.inl.intro
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ f a = f w ∧ f b = f v

Proof state:
case Adj.h.h.a.mp
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj 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✝¹

Tactic:
rintro ⟨a, b, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl, rfl⟩ <;> simp

Result:
no goals

Proof state:
case verts.h.mp
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ f x = x✝) → x✝ = f v ∨ x✝ = f w

Tactic:
rintro ⟨u, rfl | rfl, rfl⟩ <;> simp

Result:
no goals

Proof state:
case verts.h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x✝ ∈ (G'.subgraphOfAdj ⋯).verts

Tactic:
simp only [Subgraph.map_verts, subgraphOfAdj_verts, Set.mem_image, Set.mem_insert_iff,
  Set.mem_singleton_iff]

Result:
case verts.h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ f x = x✝) ↔ x✝ = f v ∨ x✝ = f w

Proof state:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (w = v ∨ w = w) ∧ f w = f w

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = v ∧ w = w ∨ v = w ∧ w = v) ∧ f v = f v ∧ f w = f w

Tactic:
simp

Result:
no goals

Proof state:
case Adj.h.h.a.mpr.inr.intro
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ a b, (v = a ∧ w = b ∨ v = b ∧ w = a) ∧ f a = f w ∧ f b = f v

Tactic:
use w, v

Result:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = w ∧ w = v ∨ v = v ∧ w = w) ∧ f w = f w ∧ f v = f v

Proof state:
case verts.h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ f x = x✝) ↔ x✝ = f v ∨ x✝ = f w

Tactic:
constructor

Result:
case verts.h.mp
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ (∃ x, (x = v ∨ x = w) ∧ f x = x✝) → x✝ = f v ∨ x✝ = f w

case verts.h.mpr
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ = f v ∨ x✝ = f w → ∃ x, (x = v ∨ x = w) ∧ f x = x✝

Proof state:
case verts.h.mpr
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ = f v ∨ x✝ = f w → ∃ x, (x = v ∨ x = w) ∧ f x = x✝

Tactic:
rintro (rfl | rfl)

Result:
case verts.h.mpr.inl
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ x, (x = v ∨ x = w) ∧ f x = f v

case verts.h.mpr.inr
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ x, (x = v ∨ x = w) ∧ f x = f w

Proof state:
case verts.h.mpr.inl
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ ∃ x, (x = v ∨ x = w) ∧ f x = f v

Tactic:
use v

Result:
case h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ (v = v ∨ v = w) ∧ f v = f v

Proof state:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
⊢ Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj ⋯

Tactic:
ext

Result:
case verts.h
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.subgraphOfAdj hvw)).verts ↔ x✝ ∈ (G'.subgraphOfAdj ⋯).verts

case Adj.h.h.a
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
hvw : G.Adj v w
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.subgraphOfAdj hvw)).Adj x✝¹ x✝ ↔ (G'.subgraphOfAdj ⋯).Adj x✝¹ x✝