mathlib-initiative/mathlib-tactics huggingface dataset:
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
hnil : ¬p.Nil
⊢ w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e

Tactic:
by

Goal state after:
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).support = p.support

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u u' : V
hu : u = u'
⊢ nil.copy hu hu = nil

Tactic:
by

Goal state after:
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).length = p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w u' w' : V
h : G.Adj u v
p : G.Walk v w
hu : u = u'
hw : w = w'
⊢ (cons h p).copy hu hw = cons ⋯ (p.copy ⋯ hw)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w v' w' : V
h : G.Adj u v
p : G.Walk v' w'
hv : v' = v
hw : w' = w
⊢ cons h (p.copy hv hw) = (cons ⋯ p).copy ⋯ hw

Tactic:
by

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.append nil = p

Tactic:
by

Goal state after:
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
K : SimpleGraph V
hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet
⊢ (p.transfer H hp).transfer K hp' = p.transfer K ⋯

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w✝ : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (p.append q).edges

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
S : Set V
uS : u ∈ S
vS : v ∉ S
⊢ ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w✝ : V
p : G.Walk u v
H : SimpleGraph V
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ q.edges
⊢ e ∈ (p.append q).edges

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
h : G.Adj v w
q : G.Walk w x
⊢ (p.concat h).append q = p.append (cons h q)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List V
hne : l ≠ []
hchain : List.IsChain G.Adj l
⊢ (ofSupport l hne hchain).support = l

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List V
hne : l ≠ []
hchain : List.IsChain G.Adj l
⊢ (ofSupport l hne hchain).length = l.length - 1

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
d : G.Dart
⊢ [d] ≠ []

Tactic:
by

Goal state after:
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
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
⊢ (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

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
d : G.Dart
⊢ List.IsChain G.DartAdj [d]

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
⊢ ∀ e ∈ p.reverse.edges, e ∈ H.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ ∃ x q, ∃ (h' : G.Adj x w), cons h p = q.concat h'

Tactic:
induction p generalizing u with
  | nil => exact ⟨_, nil, h, rfl⟩
  | cons h' p ih =>
    obtain ⟨y, q, h'', hc⟩ := ih h'
    exact ⟨y, cons h q, h'', hc ▸ concat_cons _ _ _ ▸ rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ ∃ x q, ∃ (h' : G.Adj x w), cons h p = q.concat h'

Tactic:
by

Goal state after:
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).reverse = p.reverse.transfer H ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u✝ v✝¹ u'✝ v' w✝ : V
p : G.Walk u✝ v✝¹
H : SimpleGraph V
s s' : Set V
u v✝ v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ ∀ x ∈ w.support, x ∈ s

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).darts = l

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).edges = List.map Dart.edge l

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w✝ : V
p : G.Walk u v
H : SimpleGraph V
s s' : Set V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ ∀ x ∈ w.support, x ∈ s

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝ v u' : V
hu : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons hu w).support, x ∈ s
⊢ (Walk.induce s (cons hu w) hw).support = (cons hu w).support.attachWith (Membership.mem s) hw

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
l : List G.Dart
hne : l ≠ []
hchain : List.IsChain G.DartAdj l
⊢ (ofDarts l hne hchain).length = l.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
u v✝ v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (Embedding.induce s).toHom (Walk.induce s (cons huu' w) hw) = cons huu' w

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s s' : Set V
hs : s ⊆ s'
u v✝ v u' : V
huu' : G.Adj u u'
w : G.Walk u' v
hw : ∀ x ∈ (cons huu' w).support, x ∈ s
⊢ Walk.map (G.induceHomOfLE hs).toHom (Walk.induce s (cons huu' w) hw) = Walk.induce s' (cons huu' w) ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v✝ u' v' w✝ : V
p✝ : G.Walk u v✝
H : SimpleGraph V
s✝ s' : Set V
s : Set (Sym2 V)
v w : V
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∈ (G.deleteEdges s).edgeSet

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p✝ : G.Walk u v
H : SimpleGraph V
s s' : Set V
e : Sym2 V
p : G.Walk v w
hp : e ∉ p.edges
x✝ : Sym2 V
⊢ x✝ ∈ p.edges → x✝ ∉ {e}

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 u w
⊢ p.reverseAux q = p.reverse.append q

Tactic:
by

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

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).reverse = p.reverse.append (cons ⋯ nil)

Tactic:
by

Goal state after:
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).reverse = p.reverse.copy hv hu

Tactic:
by

Goal state after:
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).reverse = q.reverse.append p.reverse

Tactic:
by

Goal state after:
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).reverse = cons ⋯ p.reverse

Tactic:
by

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.reverse = p

Tactic:
by

Goal state after:
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).length = p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ Walk.map (Hom.ofLE ⋯) (toDeleteEdges s p hp) = p

Tactic:
by

Goal state after:
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).length = p.length + q.length

Tactic:
by

Goal state after:
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 u w
⊢ (p.reverseAux q).length = p.length + q.length

Tactic:
by

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.length = p.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p = (nil.append p).append nil

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
q : G.Walk u v
⊢ q = (nil.append nil).append q

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
q : G.Walk u v
⊢ q = (q.append nil).append nil

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj w u'
⊢ p.IsSubwalk (cons h q)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj v' w
r₁ : G.Walk u' u
r₂ : G.Walk v v'
⊢ ((r₁.append p).append r₂).concat h = (r₁.append p).append (r₂.concat h)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj v' w
⊢ p.IsSubwalk (q.concat h)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ u₃ v₃ : V
p₁ : G.Walk u₁ v₁
p₂ : G.Walk u₂ v₂
p₃ : G.Walk u₃ v₃
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₃
⊢ p₁.IsSubwalk p₃

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u' u v : V
q : G.Walk u v
⊢ nil.IsSubwalk q ↔ ∃ ru rv, q = ru.append rv

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ : V
q : G.Walk u₁ v₁
p : G.Walk u₂ v₂
h : p.IsSubwalk q
⊢ p.length ≤ q.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = (nil.append (p.take n)).append (p.drop n)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = ((p.take n).append (p.drop n)).append nil

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 1 - ε ^ 5 / 50 ≤ (↑m / (↑m + 1)) ^ 2

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
⊢ 0 ≤ ε

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
⊢ s.length + p₁.length ≤ p₂.length

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ ↑m ≠ 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ p₂.length

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length + p₁.length ≤ p₂.length

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 0 < 100 / ε ^ 5

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ (1 + 1 / ↑m) ^ 2 ≤ (1 + ε ^ 5 / 100) ^ 2

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ s.length + p₁.length + 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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ (1 + ε ^ 5 / 100) ^ 2 = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000)

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
x✝ : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.support.length ≤ s.length + p₁.length + 1 - s.length

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000)

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) ≤ 1 + ε ^ 5 * 49⁻¹

Tactic:
by

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
i : ℕ
⊢ p.reverse.getVert i = p.getVert (p.length - i)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk v u

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ 1 + ε ^ 5 * 49⁻¹ = 1 + ε ^ 5 / 49

Tactic:
by

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
⊢ p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : ¬v = u
⊢ u ∈ p.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v' : V
p : G.Walk v' v
hwp : w ∈ p.support
h : u ≠ w
hadj : G.Adj u v'
⊢ (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.takeUntil u ⋯ = nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
x✝ : u = w
⊢ (p.takeUntil w hwp).Nil

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
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
⊢ ((↑m + 1) / ↑m) ^ 2 ≤ 1 + ε ^ 5 / 49

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
v w u : V
h : u ∈ nil.support
⊢ G.Walk u v

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : v = u
⊢ G.Walk u w

Tactic:
by

Goal state after: