mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x✝ ∈ (G'.singletonSubgraph (f v)).verts

pp: case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.singletonSubgraph v)).Adj x✝¹ x✝ ↔ (G'.singletonSubgraph (f v)).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝ : W
⊢ x✝ ∈ (Subgraph.map f (G.singletonSubgraph v)).verts ↔ x✝ ∈ (G'.singletonSubgraph (f v)).verts

case Adj
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v : V
x✝¹ x✝ : W
⊢ (Subgraph.map f (G.singletonSubgraph v)).Adj x✝¹ x✝ ↔ (G'.singletonSubgraph (f v)).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj ⋯).verts ↔ x✝ ∈ (G.subgraphOfAdj hvw).verts

pp: case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj ⋯).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝ : V
⊢ x✝ ∈ (G.subgraphOfAdj ⋯).verts ↔ x✝ ∈ (G.subgraphOfAdj hvw).verts

case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj ⋯).Adj x✝¹ x✝ ↔ (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
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

pp: case Adj
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:
<;>

Goal state after:
case verts
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
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✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅

pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ {v}

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = {w} ∪ ∅

case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ {v}

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
w : V
hvw : G.Adj w w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬v = w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅

pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬w = v
⊢ (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}

pp: case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
w : V
hvw : G.Adj w w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {w} ∪ {w}

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬v = w
⊢ (G.subgraphOfAdj hvw).neighborSet v = {w} ∪ ∅

case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w : V
hvw : G.Adj v w
h✝ : ¬w = v
⊢ (G.subgraphOfAdj hvw).neighborSet w = ∅ ∪ {v}

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
h✝¹ : ¬u = v
h✝ : ¬u = w
⊢ (G.subgraphOfAdj hvw).neighborSet u = ∅ ∪ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x✝ ∈ (G'.deleteEdges (s ∪ s')).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((G'.deleteEdges s).deleteEdges s').Adj x✝¹ x✝ ↔ (G'.deleteEdges (s ∪ s')).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x✝ ∈ (G'.deleteEdges (s ∪ s')).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((G'.deleteEdges s).deleteEdges s').Adj x✝¹ x✝ ↔ (G'.deleteEdges (s ∪ s')).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges ∅).verts ↔ x✝ ∈ G'.verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.deleteEdges ∅).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges ∅).verts ↔ x✝ ∈ G'.verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.deleteEdges ∅).Adj x✝¹ x✝ ↔ G'.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp.refl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ s(⟨v, hv'⟩, ⟨w, hw'⟩) ∉ s

pp: case mp.swap
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ s(⟨w, hv'⟩, ⟨v, hw'⟩) ∉ s

Tactic:
<;>

Goal state after:
case mp.refl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ s(⟨v, hv'⟩, ⟨w, hw'⟩) ∉ s

case mp.swap
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ s(⟨w, hv'⟩, ⟨v, hw'⟩) ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).verts ⊆ G'.verts

pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s).Adj v w → G'.Adj v w

Tactic:
<;>

Goal state after:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).verts ⊆ G'.verts

case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s).Adj v w → G'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts

pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w

Tactic:
<;>

Goal state after:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ (G'.deleteEdges s').verts ⊆ (G'.deleteEdges s).verts

case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, (G'.deleteEdges s').Adj v w → (G'.deleteEdges s).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x✝ ∈ (G'.deleteEdges s).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges (G'.edgeSet ∩ s)).verts ↔ x✝ ∈ (G'.deleteEdges s).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.deleteEdges (G'.edgeSet ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges (s ∩ G'.edgeSet)).verts ↔ x✝ ∈ (G'.deleteEdges s).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.deleteEdges (s ∩ G'.edgeSet)).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ (G'.deleteEdges (s ∩ G'.edgeSet)).verts ↔ x✝ ∈ (G'.deleteEdges s).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ (G'.deleteEdges (s ∩ G'.edgeSet)).Adj x✝¹ x✝ ↔ (G'.deleteEdges s).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce ∅).verts ↔ x✝ ∈ ⊥.verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce ∅).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (G'.induce ∅).verts ↔ x✝ ∈ ⊥.verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce ∅).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ → G'.Adj x✝¹ x✝

pp: case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → (G'.induce G'.verts).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case Adj.mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ (G'.induce G'.verts).Adj x✝¹ x✝ → G'.Adj x✝¹ x✝

case Adj.mpr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝¹ x✝ : V
⊢ G'.Adj x✝¹ x✝ → (G'.induce G'.verts).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case right.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s ∧ w ∈ s ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

pp: case right.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
<;>

Goal state after:
case right.inl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s ∧ w ∈ s ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

case right.inr
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
v w : V
h : v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w
⊢ (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
v x✝ : V
⊢ x✝ ∈ (G.singletonSubgraph v).verts ↔ x✝ ∈ (⊤.induce {v}).verts

pp: case Adj
V : Type u
G : SimpleGraph V
v x✝¹ x✝ : V
⊢ (G.singletonSubgraph v).Adj x✝¹ x✝ ↔ (⊤.induce {v}).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
v x✝ : V
⊢ x✝ ∈ (G.singletonSubgraph v).verts ↔ x✝ ∈ (⊤.induce {v}).verts

case Adj
V : Type u
G : SimpleGraph V
v x✝¹ x✝ : V
⊢ (G.singletonSubgraph v).Adj x✝¹ x✝ ↔ (⊤.induce {v}).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.getVert 0 = u

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).getVert 0 = u

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.getVert 0 = u

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).getVert 0 = u
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
⊢ nil.getVert i ∈ nil.support

pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
i : ℕ
⊢ (cons h✝ p✝).getVert i ∈ (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
⊢ nil.getVert i ∈ nil.support

case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
i : ℕ
⊢ (cons h✝ p✝).getVert i ∈ (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.getVert 0 ∈ nil.support

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ nil.getVert (n✝ + 1) ∈ nil.support

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
⊢ (cons h✝ p✝).getVert 0 ∈ (cons h✝ p✝).support

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
n✝ : ℕ
⊢ (cons h✝ p✝).getVert (n✝ + 1) ∈ (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.getVert 0 ∈ nil.support

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ nil.getVert (n✝ + 1) ∈ nil.support

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
⊢ (cons h✝ p✝).getVert 0 ∈ (cons h✝ p✝).support

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (i : ℕ), p✝.getVert i ∈ p✝.support
n✝ : ℕ
⊢ (cons h✝ p✝).getVert (n✝ + 1) ∈ (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mp.inl
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (⊤.induce {v, w}).Adj v w

pp: case Adj.mp.inr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (⊤.induce {v, w}).Adj w v

Tactic:
<;>

Goal state after:
case Adj.mp.inl
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (⊤.induce {v, w}).Adj v w

case Adj.mp.inr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (⊤.induce {v, w}).Adj w v
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj.mpr.inl.inl
V : Type u
G : SimpleGraph V
w x✝ : V
hvw : G.Adj x✝ w
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

pp: case Adj.mpr.inl.inr
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha hvw : G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

pp: case Adj.mpr.inr.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

pp: case Adj.mpr.inr.inr
V : Type u
G : SimpleGraph V
v x✝ : V
hvw : G.Adj v x✝
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

Tactic:
<;>

Goal state after:
case Adj.mpr.inl.inl
V : Type u
G : SimpleGraph V
w x✝ : V
hvw : G.Adj x✝ w
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝

case Adj.mpr.inl.inr
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha hvw : G.Adj x✝¹ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

case Adj.mpr.inr.inl
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
ha : G.Adj x✝¹ x✝
hvw : G.Adj x✝ x✝¹
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝

case Adj.mpr.inr.inr
V : Type u
G : SimpleGraph V
v x✝ : V
hvw : G.Adj v x✝
ha : G.Adj x✝ x✝
⊢ (G.subgraphOfAdj hvw).Adj x✝ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case fst
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h✝ : n < p.darts.length
h : n < p.length
⊢ p.darts[n].toProd.1 = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }.toProd.1

pp: case snd
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h✝ : n < p.darts.length
h : n < p.length
⊢ p.darts[n].toProd.2 = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }.toProd.2

Tactic:
<;>

Goal state after:
case fst
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h✝ : n < p.darts.length
h : n < p.length
⊢ p.darts[n].toProd.1 = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }.toProd.1

case snd
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h✝ : n < p.darts.length
h : n < p.length
⊢ p.darts[n].toProd.2 = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }.toProd.2
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x✝ : V
⊢ x✝ ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x✝ ∈ (G'.deleteVerts (s ∪ s')).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x✝¹ x✝ : V
⊢ ((G'.deleteVerts s).deleteVerts s').Adj x✝¹ x✝ ↔ (G'.deleteVerts (s ∪ s')).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x✝ : V
⊢ x✝ ∈ ((G'.deleteVerts s).deleteVerts s').verts ↔ x✝ ∈ (G'.deleteVerts (s ∪ s')).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
x✝¹ x✝ : V
⊢ ((G'.deleteVerts s).deleteVerts s').Adj x✝¹ x✝ ↔ (G'.deleteVerts (s ∪ s')).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ (G'.deleteVerts s).verts ⊆ G'.verts

pp: case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ ∀ ⦃v w : V⦄, (G'.deleteVerts s).Adj v w → G'.Adj v w

Tactic:
<;>

Goal state after:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ (G'.deleteVerts s).verts ⊆ G'.verts

case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ ∀ ⦃v w : V⦄, (G'.deleteVerts s).Adj v w → G'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support ≠ []

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).support ≠ []

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support ≠ []

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).support ≠ []
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (G'.verts ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (G'.verts ∩ s)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (G'.verts ∩ s)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (s ∩ G'.verts)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝

Tactic:
<;>

Goal state after:
case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝ : V
⊢ x✝ ∈ (G'.deleteVerts (s ∩ G'.verts)).verts ↔ x✝ ∈ (G'.deleteVerts s).verts

case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
x✝¹ x✝ : V
⊢ (G'.deleteVerts (s ∩ G'.verts)).Adj x✝¹ x✝ ↔ (G'.deleteVerts s).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
a : V
⊢ nil.support.head ⋯ = a

pp: case cons
V : Type u
G : SimpleGraph V
a b v✝ : V
h✝ : G.Adj a v✝
p✝ : G.Walk v✝ b
⊢ (cons h✝ p✝).support.head ⋯ = a

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
a : V
⊢ nil.support.head ⋯ = a

case cons
V : Type u
G : SimpleGraph V
a b v✝ : V
h✝ : G.Adj a v✝
p✝ : G.Walk v✝ b
⊢ (cons h✝ p✝).support.head ⋯ = a
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ s(u', v') ∈ p.edges → ∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')

pp: case mpr
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ (∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')) → s(u', v') ∈ p.edges

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ s(u', v') ∈ p.edges → ∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')

case mpr
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ (∃ i < p.length, s(p.getVert i, p.getVert (i + 1)) = s(u', v')) → s(u', v') ∈ p.edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
a b u✝ : V
⊢ nil.support.getLast ⋯ = u✝

pp: case cons
V : Type u
G : SimpleGraph V
a b u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.getLast ⋯ = w✝
⊢ (cons h✝ p✝).support.getLast ⋯ = w✝

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
a b u✝ : V
⊢ nil.support.getLast ⋯ = u✝

case cons
V : Type u
G : SimpleGraph V
a b u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.getLast ⋯ = w✝
⊢ (cons h✝ p✝).support.getLast ⋯ = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ u :: nil.support.tail = nil.support

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ u :: (cons h✝ p✝).support.tail = (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ u :: nil.support.tail = nil.support

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ u :: (cons h✝ p✝).support.tail = (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support = u :: nil.support.tail

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).support = u :: (cons h✝ p✝).support.tail

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.support = u :: nil.support.tail

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).support = u :: (cons h✝ p✝).support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ u ∈ nil.support

pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ u ∈ (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ u ∈ nil.support

case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ u ∈ (cons h✝ p✝).support