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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ Subgraph.coeSubgraph H' ≤ H

Tactic:
constructor

Goal state after:
case left
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ (Subgraph.coeSubgraph H').verts ⊆ H.verts

case right
V : Type u
G : SimpleGraph V
H : G.Subgraph
H' : H.coe.Subgraph
⊢ ∀ ⦃v w : V⦄, (Subgraph.coeSubgraph H').Adj v w → H.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s t v w : V
⊢ s(v, w) = s(s, t) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

Tactic:
Sym2.eq_iff

Goal state after:
V : Type u_1
s t v w : V
⊢ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Subgraph.coeSubgraph (Subgraph.restrict H') = H ⊓ H'

Tactic:
ext

Goal state after:
case verts
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝ : V
⊢ x✝ ∈ (Subgraph.coeSubgraph (Subgraph.restrict H')).verts ↔ x✝ ∈ (H ⊓ H').verts

case Adj
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
x✝¹ x✝ : V
⊢ (Subgraph.coeSubgraph (Subgraph.restrict H')).Adj x✝¹ x✝ ↔ (H ⊓ H').Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
s : V
⊢ edge s s = ⊥

Tactic:
ext

Goal state after:
V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
⊢ (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s')

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.deleteEdges ∅ = G'

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe

Tactic:
ext

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

Goal state before:
pp: 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
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s ↔ ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

Tactic:
constructor

Goal state after:
case mp
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
⊢ s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s → ∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)

case mpr
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
⊢ (∀ x ∈ s, ¬Sym2.map Subtype.val x = s(v, w)) → s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

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

Tactic:
constructor

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ G'.deleteEdges s' ≤ G'.deleteEdges s

Tactic:
constructor

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s

Tactic:
ext

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: V : Type u
G : SimpleGraph V
s : Set V
⊢ SimpleGraph.induce s G = (⊤.induce s).coe

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
x✝¹ x✝ : ↑s
⊢ (SimpleGraph.induce s G).Adj x✝¹ x✝ ↔ (⊤.induce s).coe.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' G'' : G.Subgraph
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ G'.induce s ≤ G''.induce s'

Tactic:
constructor

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

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce ∅ = ⊥

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.induce G'.verts = G'

Tactic:
ext

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

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

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

Tactic:
constructor

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
constructor

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

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
⊢ G.singletonSubgraph v = ⊤.induce {v}

Tactic:
ext

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.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj hvw = ⊤.induce {v, w}

Tactic:
ext

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

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (G.subgraphOfAdj hvw).Adj x✝¹ x✝ ↔ (⊤.induce {v, w}).Adj x✝¹ x✝

Tactic:
constructor

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

case Adj.mpr
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
x✝¹ x✝ : V
⊢ (⊤.induce {v, w}).Adj x✝¹ x✝ → (G.subgraphOfAdj hvw).Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: 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] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts s ≤ G'

Tactic:
constructor

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.Subgraph

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

Tactic:
ext

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: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
⊢ G'.deleteVerts (s ∩ G'.verts) = G'.deleteVerts s

Tactic:
ext

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.Traversal

Goal state before:
pp: 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')

Tactic:
constructor

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: V : Type u
G : SimpleGraph V
u : V
⊢ nil.edgeSet = ∅

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u : V
x✝ : Sym2 V
⊢ x✝ ∈ nil.edgeSet ↔ x✝ ∈ ∅
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).edgeSet = insert s(u, v) p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (cons h p).edgeSet ↔ x✝ ∈ insert s(u, v) p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).edgeSet = Sym2.map ⇑f '' p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
x✝ : Sym2 V'
⊢ x✝ ∈ (Walk.map f p).edgeSet ↔ x✝ ∈ Sym2.map ⇑f '' p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ (p.transfer H hp).edgeSet = p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
x✝ : Sym2 V
⊢ x✝ ∈ (p.transfer H hp).edgeSet ↔ x✝ ∈ p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.reverseAux q).length = nil.length + q.length

Tactic:
simp!

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case nil
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil ↔ ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv

Tactic:
constructor

Goal state after:
case nil.mp
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ nil.IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv

case nil.mpr
V : Type u_1
G : SimpleGraph V
u u' : V
⊢ (∃ (hu : u' = u) (hv : u' = u), nil = nil.copy hu hv) → nil.IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case cons
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil ↔ ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv

Tactic:
constructor

Goal state after:
case cons.mp
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).IsSubwalk nil → ∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv

case cons.mpr
V : Type u_1
G : SimpleGraph V
u v u' v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (∃ (hu : u' = u) (hv : u' = v), cons h p = nil.copy hu hv) → (cons h p).IsSubwalk nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
h✝ : G.Adj u v✝
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝

Tactic:
simp!

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k] = p₁.darts[i]

Tactic:
ext

Goal state after:
case refine_1.fst
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.1 = p₁.darts[i].toProd.1

case refine_1.snd
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k,
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h : ∀ (i : ℕ) (h : i < p₁.support.length), p₂.support[i + k]? = some p₁.support[i]
i : ℕ
hi : i < p₁.darts.length
⊢ p₂.darts[i + k].toProd.2 = p₁.darts[i].toProd.2
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ ∃ q r, p = q.append r

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support → ∃ q r, p = q.append r

case mpr
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (∃ q r, p = q.append r) → w ∈ p.support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos.inr.nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
ih : ∀ (h : u ∈ nil.support), List.count s(u, x) (nil.takeUntil u h).edges ≤ 1
a✝ : List.Mem u nil.support
⊢ List.count s(u, x) (nil.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
simp!

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos.inr.cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
ha : G.Adj (u, x).2 (u, x).1
v✝ : V
h✝ : G.Adj (u, x).1 v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (h : u ∈ (cons h✝ p✝).support), List.count s(u, x) ((cons h✝ p✝).takeUntil u h).edges ≤ 1
a✝ : List.Mem u (cons h✝ p✝).support
⊢ List.count s(u, x) ((cons h✝ p✝).takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
simp!

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.edgeSet = p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : Sym2 V
⊢ x✝ ∈ p.reverse.edgeSet ↔ x✝ ∈ p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).edgeSet = insert s(v, w) p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.concat h).edgeSet ↔ x✝ ∈ insert s(v, w) p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
x✝ : Sym2 V
⊢ x✝ ∈ (p.append q).edgeSet ↔ x✝ ∈ p.edgeSet ∪ q.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edgeSet = p.edgeSet

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
x✝ : Sym2 V
⊢ x✝ ∈ (p.copy hu hv).edgeSet ↔ x✝ ∈ p.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail ↔ p.IsTrail

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail → p.IsTrail

case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsTrail → p.reverse.IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsPath

Tactic:
constructor

Goal state after:
case isTrail
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsTrail

case support_nodup
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath ∧ u ∉ p.support

case mpr
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ p.IsPath ∧ u ∉ p.support → (cons h p).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath ↔ p.IsPath

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath → p.IsPath

case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath → p.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p.IsPath

Tactic:
convert! h.reverse

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p = p.reverse.reverse
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
convert! h.reverse

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t → ∃ s, G.IsClique ↑s ∧ map f s = t

case mpr
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique ↑s ∧ map f s = t) → (SimpleGraph.map (⇑f) G).IsClique ↑t
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s ↔
    G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s →
    G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

case mpr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) →
    (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s