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

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ t ∈ 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
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
⊢ (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length

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
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).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
h : p.support.Nodup
⊢ p.edges.Nodup

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ 0 ≤ p.length

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
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ False

Tactic:
have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length := by
    exact length_takeUntil_lt_length _ h

Goal state after:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
⊢ False
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
x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
⊢ w ∉ (p.takeUntil x ⋯).support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.length - 1 ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).support.tail ~r c.support.tail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ w ∈ (c.rotate u h).support ↔ w ∈ c.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).darts ~r c.darts

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).length = c.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
h : G.Adj v w
⊢ (p.concat h).edgeSet = insert s(v, w) p.edgeSet

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
c : G.Walk v v
h : u ∈ c.support
⊢ (c.rotate u h).Nil ↔ c.Nil

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
c : G.Walk v v
h : u ∈ c.support
⊢ c.rotate u h = nil ↔ c = 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
⊢ (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
⊢ u ∈ p.support ↔ ∃ n, p.getVert n = u ∧ n ≤ 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 u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).edgeSet = p.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
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).Nil ↔ p.Nil ∧ q.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
hp : p.Nil
hq : q.Nil
⊢ (p.append q).Nil

Tactic:
by

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

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

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
n : ℕ
⊢ (p.drop n).length = p.length - n

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
n m : ℕ
⊢ (p.drop n).getVert m = p.getVert (n + m)

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
n m : ℕ
⊢ p.drop (n + m) ≍ (p.drop n).drop m

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
n m : ℕ
⊢ (p.drop n).drop m ≍ ((p.drop n).drop m).copy ⋯ ⋯

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
n : ℕ
⊢ (p.drop n).Nil ↔ p.length ≤ n

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
n : ℕ
hn : n ≠ 0
⊢ (cons h p).drop n = (p.drop (n - 1)).copy ⋯ ⋯

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
n : ℕ
⊢ (p.drop n).darts = List.drop n p.darts

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 V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 ≤ ↑(#(A.sup id)) * ↑(#(B.sup id))

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
n : ℕ
⊢ (p.drop n).edges = List.drop n p.edges

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.take 0 = nil.copy ⋯ ⋯

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
n : ℕ
⊢ (p.take n).length = min n p.length

Tactic:
by

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

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).IsTrail ↔ p.IsTrail

Tactic:
by

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

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).IsPath ↔ p.IsPath

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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).IsTrail → p.IsTrail

Tactic:
by

Goal state after:
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).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u u' v : V
w : G.Walk u' v
hw : w.IsTrail
hu : G.Adj u u'
hu' : s(u, u') ∉ w.edges
⊢ (cons hu w).IsTrail

Tactic:
by

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

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

Tactic:
by

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

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

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).IsTrail ↔ p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
edges : Finset (Sym2 V) := w.edges.toFinset
this : edges.card = w.length
⊢ edges ⊆ G.edgeFinset

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
u v : V
w : G.Walk u v
h : w.IsTrail
⊢ w.length ≤ G.edgeFinset.card

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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
n m : ℕ
⊢ (p.take n).getVert m = p.getVert (min n m)

Tactic:
by

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

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

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).IsPath → p.IsPath

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsTrail
⊢ p₁.IsTrail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h : p₁.IsSubwalk p₂
h₂ : p₂.IsPath
⊢ p₁.IsPath

Tactic:
by

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

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).IsPath ↔ p.IsPath ∧ w ∉ p.support

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
hq : ¬q.Nil
⊢ p.support.Disjoint q.tail.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
⊢ ¬q.Nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x : V
hx : x ∈ p.support
hyv : x ≠ v
hy : x ∈ q.support
hq : ¬q.Nil
⊢ x ∈ q.tail.support

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hpq : (p.append q).IsPath
x y : V
hyv : y ≠ v
hx : x ∈ p.support
hy : y ∈ q.support
⊢ x ≠ y

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝ : V
h : G.Adj u v✝
p✝ : G.Walk v✝ u
hp : (cons h p✝).IsCircuit
⊢ G ≠ ⊥

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
n m : ℕ
⊢ p.take (n + m) ≍ (p.take n).append ((p.drop n).take m)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : p.IsCircuit
⊢ 3 ≤ 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 : V
p : G.Walk u v
n m : ℕ
⊢ (p.take n).append ((p.drop n).take m) ≍ ((p.take n).append ((p.drop n).take m)).copy ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
hc : (cons h p).IsCycle
⊢ ¬p.Nil

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
h' : p.reverse = nil
⊢ p = nil

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.IsCycle
⊢ p.reverse.IsCycle

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
h : p.reverse.IsCycle
⊢ p.IsCycle

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬p.Nil
hcyc : (p.append q).IsCycle
⊢ q.IsPath

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
n : ℕ
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
h : ¬q.Nil
hcyc : (p.append q).IsCycle
⊢ ¬q.reverse.Nil

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
h : p.IsCycle
hn : 0 < n
⊢ (p.drop n).IsPath

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
n : ℕ
⊢ (p.take n).support = List.take (n + 1) 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 : V
p : G.Walk u v
n m : ℕ
⊢ (p.take n).take m = (p.take (min n m)).copy ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
hn : n < p.length
h : (p.take (p.length - 1)).IsPath
this : ((p.take (p.length - 1)).take n).IsPath
⊢ (p.take n).IsPath

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
n : ℕ
p : G.Walk u u
h : p.IsCycle
hn : n < p.length
⊢ (p.take n).IsPath

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
this : s.Finite
x : V
⊢ nil.IsTrail ∧ nil.length = 0

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ p.take n = p.copy ⋯ ⋯

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
n : ℕ
hn : n ≠ 0
⊢ (cons h p).take n = cons h ((p.take (n - 1)).copy ⋯ ⋯)

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite ↑G.edgeSet
this✝ : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsPath ∧ p.length = n}
this : s.Finite
x : V
⊢ nil.IsPath ∧ nil.length = 0

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
n : ℕ
⊢ (p.take n).darts = List.take n p.darts

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsPath), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length

Tactic:
by

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.IsPath

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
n : ℕ
⊢ (p.take n).edges = List.take n p.edges

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).penultimate = v

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.snd = p.penultimate

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.penultimate = p.snd

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.tail.darts = p.darts.tail

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.length < Fintype.card V

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.tail.edges = p.edges.tail

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.drop 0 = p.copy ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
⊢ (p.drop n).Nil

Tactic:
by

Goal state after: