mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ (1 - 2 ^ #P.parts * ↑m / (↑(#U) * ε)) * ↑(#(G.nonuniformWitness ε U V)) =
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V))

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet

Tactic:
simp [edge]

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet = {s(v, w)} \ Sym2.diagSet

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet ⊆ {s(v, w)}

Tactic:
simp [edge]

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
a b : V
⊢ (G'.Adj \ Sym2.ToRel s) a b → (G'.Adj \ Sym2.ToRel s) b a

Tactic:
by

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

Goal state before:
pp: V : Type u_1
v w : V
⊢ (edge v w).edgeSet ⊆ {s(v, w)}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
s t : V
h : s ≠ t
⊢ (edge s t).edgeSet = {s(s, t)}

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
h : G.Adj s t
⊢ G ⊔ edge s t = G

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_1
u v : V
s : Set (Sym2 V)
h : s(u, v) ∈ s
⊢ (edge u v).deleteEdges s = ⊥

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ Disjoint G (edge u v) ↔ ¬G.Adj u v

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Adj u v
⊢ G \ edge u v = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ 2 ^ #P.parts = 2 ^ (#P.parts - 1) * 2

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ⨆ e ∈ G.edgeSet, fromEdgeSet {e} = G

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
⊢ G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe

Tactic:
by

Goal state after:
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).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), edge u v = x} = G

Tactic:
by

Goal state after:
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).coe ≤ G'.coe

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
H : (G ⊔ edge s t).Subgraph
h : ¬H.Adj s t
⊢ H.spanningCoe ≤ G

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).spanningCoe = (SimpleGraph.induce s G).spanningCoe

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ Fintype ↑(edge s t).edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.IsInduced ↔ ∃ s, G' = ⊤.induce s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ s(s, t) ∉ G.edgeFinset

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ (G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet
hn : ¬G.Adj s t
h : s ≠ t
⊢ #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 ∪ s')

Tactic:
by

Goal state after:
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 ∪ s')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert 0 = u

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : w.length ≤ i
⊢ w.getVert i = v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
⊢ G.Adj (w.getVert i) (w.getVert (i + 1))

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
n : ℕ
p : G.Walk v w
h : G.Adj u v
hn : n ≠ 0
⊢ (cons h p).getVert n = p.getVert (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V)) ≤
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ (#P.parts - 1) * ↑m

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.getVert i ∈ p.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ p.getVert n = p.support[n]

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n < p.support.length
⊢ n ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ some (p.getVert n) = p.support[n]?

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : ℕ
⊢ p.getVert n = p.support.getD n v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ p.getVert (List.idxOf w p.support) = w

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.getVert ∘ Fin.val = p.support.get

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝ : V
⊢ x✝ ∈ Set.range p.getVert → x✝ ∈ Set.range p.support.get

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
x✝¹ : V
x✝ : x✝¹ ∈ Set.range p.support.get
n : Fin p.support.length
h✝ : p.support.get n = x✝¹
⊢ p.getVert ↑n = x✝¹

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv : v ∈ (G'.induce s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
⊢ ∀ {a b : ↑(G'.induce s).verts},
    (SimpleGraph.induce {v | ↑v ∈ s} G'.coe).Adj
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, hv⟩,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, hv⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      (G'.induce s).coe.Adj a b

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
u v : V
⊢ (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ h.toWalk.length = 1

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
x✝ : G.Adj u v
⊢ x✝.toWalk.length = 1

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.length ≤ 1
hq : q.length ≤ 1
⊢ p = q

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ ↑(#(G.nonuniformWitness ε U V)) - 2 ^ (#P.parts - 1) * ↑m ≤ ↑(#((star hP G ε hU V).biUnion id))

Tactic:
by

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
⊢ (⊤.deleteVerts u).coe ≤ (⊤.deleteVerts u).coe

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
h : i < p.edges.length
⊢ p.edges[i] = s(p.getVert i, p.getVert (i + 1))

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support ≠ []

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s u : Set V
r : DecidableRel G.Adj
x y : ↑(⊤.deleteVerts u).verts
h : G.Adj ↑x ↑y
⊢ ↑x ∈ ⊤.verts

Tactic:
by

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

Goal state before:
pp: V : Type u
G✝ : SimpleGraph V
u v w : V
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s u : Set V
r : DecidableRel G.Adj
x y : ↑(⊤.deleteVerts u).verts
h : G.Adj ↑x ↑y
⊢ ↑y ∈ ⊤.verts

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s✝ s : Set V
x✝ : ↑(G'.deleteVerts s).verts
v : V
hv : v ∈ (G'.deleteVerts s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∉ s}

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s✝ s : Set V
x✝ : ↑{v | ↑v ∉ s}
v : ↑G'.verts
hv : v ∈ {v | ↑v ∉ s}
⊢ ↑v ∈ (G'.deleteVerts s).verts

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' : G.Subgraph
s✝ s : Set V
⊢ ∀ {a b : ↑(G'.deleteVerts s).verts},
    (SimpleGraph.induce {v | ↑v ∉ s} G'.coe).Adj
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨⟨v, ⋯⟩, ⋯⟩,
            invFun := fun x ↦
              match x with
              | ⟨v, hv⟩ => ⟨↑v, ⋯⟩,
            left_inv := ⋯, right_inv := ⋯ }
          b) ↔
      (G'.deleteVerts s).coe.Adj a b

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.head ⋯ = a

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) ≤ ↑(#((star hP G ε hU V).biUnion id))

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.getLast ⋯ = b

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
h₀ : p.support[k]? = some [u', v'][0]
h₁ : p.support[k + 1]? = some [u', v'][1]
⊢ k ≤ p.length

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support

Tactic:
by

Goal state after:
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
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
h₀ : some (p.getVert k) = some [u', v'][0]
h₁ : p.support[k + 1]? = some [u', v'][1]
⊢ k + 1 ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ {w | w ∈ p.support}

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
⊢ u ∈ nil.support ↔ u = v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
h : u ≠ v
p : G.Walk u v
⊢ v ∈ p.support.tail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hadj : G.Adj u v
⊢ p.support <:+ (cons hadj p).support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
hadj : G.Adj u v
⊢ p.support ⊆ (cons hadj p).support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ↑p.support = {u} + ↑p.support.tail

Tactic:
by

Goal state after:
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
h✝ : [u', v'] <:+: p.support
k : ℕ
hk : [u', v'].length + k ≤ p.support.length
h : ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
h₀ : p.getVert k = [u', v'][0]
h₁ : p.getVert (k + 1) = [u', v'][1]
⊢ k < p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
d : G.Dart
v w : V
h : d.toProd.2 = v
p : G.Walk v w
⊢ List.IsChain G.DartAdj (d :: p.darts)

Tactic:
by

Goal state after: