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
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ w ∈ (cons h✝ p✝).support ↔ w = u ∨ w ∈ (cons h✝ p✝).support.tail

Tactic:
simp

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:
simp

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
w✝² : V
w✝¹ : G.Adj u w✝²
w✝ : G.Walk w✝² v
⊢ v ∈ (cons w✝¹ w✝).support.tail

Tactic:
simp

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:
obtain ⟨_, _, _, rfl⟩ := exists_eq_cons_of_ne h p
  simp

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:
simp

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:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
hadj : G.Adj u v
⊢ (cons hadj q).snd = v

Tactic:
simp

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
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), (cons h q).snd ∈ (cons h q).support.tail

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).penultimate = (cons h q).penultimate

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).support[0] = u

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.darts.Nodup

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) nil.support nil.support.tail

Tactic:
simp

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
ih : nil.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) nil.support nil.support.tail
⊢ (cons h✝ nil).edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝ nil).support (cons h✝ nil).support.tail

Tactic:
simp [edges_cons, ih]

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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ w✝
ih : (cons h✝ p✝).edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝ p✝).support (cons h✝ p✝).support.tail
⊢ (cons h✝¹ (cons h✝ p✝)).edges =
    List.zipWith (fun x1 x2 ↦ s(x1, x2)) (cons h✝¹ (cons h✝ p✝)).support (cons h✝¹ (cons h✝ p✝)).support.tail

Tactic:
simp [edges_cons, ih]

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

Goal state before:
pp: case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ (Walk.map f nil).Nil ↔ nil.Nil

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (Walk.map f (cons h✝ p✝)).Nil ↔ (cons h✝ p✝).Nil

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
⊢ Walk.map f nil = nil ↔ nil = nil

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
⊢ Walk.map f (cons h✝ p✝) = nil ↔ cons h✝ p✝ = nil

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
x✝ : Sym2 V
⊢ x✝ ∈ nil.edgeSet ↔ x✝ ∈ ∅

Tactic:
simp

Goal state after:
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
x✝ : Sym2 V
⊢ x✝ ∈ (cons h p).edgeSet ↔ x✝ ∈ insert s(u, v) p.edgeSet

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.Nil ↔ nil.support = [v]

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h✝ p✝).Nil ↔ (cons h✝ p✝).support = [v]

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.darts = [] ↔ nil.Nil

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h✝ p✝).darts = [] ↔ (cons h✝ p✝).Nil

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.edges = [] ↔ nil.Nil

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ (cons h✝ p✝).edges = [] ↔ (cons h✝ p✝).Nil

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).length = 0 ↔ (cons h✝ p✝).Nil

Tactic:
simp

Goal state after:
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
x✝ : Sym2 V'
⊢ x✝ ∈ (Walk.map f p).edgeSet ↔ x✝ ∈ Sym2.map ⇑f '' p.edgeSet

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ ¬nil.Nil ↔ 0 < nil.length

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v w v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ ¬(cons h✝ p✝).Nil ↔ 0 < (cons h✝ p✝).length

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
⊢ cons h✝ p✝ = nil ↔ (cons h✝ p✝).Nil

Tactic:
simp

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
h : ¬p.Nil
⊢ ∀ {u v w : V} (h : G.Adj u v) (q : G.Walk v w), w ∈ (cons h q).support.tail

Tactic:
simp

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).length = p.length

Tactic:
simp

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).support = p.support

Tactic:
simp

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edges = p.edges

Tactic:
simp

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).edgeSet = p.edgeSet

Tactic:
simp

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).reverse = mapLe h p.reverse

Tactic:
simp

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

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

Tactic:
simp

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✝¹
u✝ v✝ : V
p✝ : G.Walk u✝ v✝
H : SimpleGraph V
u w v : V
h✝ : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h✝ p).edges, e ∈ H.edgeSet
⊢ s(u, v) ∈ (cons' u v w h✝ p).edges

Tactic:
simp

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
x✝ : Sym2 V
⊢ x✝ ∈ (p.transfer H hp).edgeSet ↔ x✝ ∈ p.edgeSet

Tactic:
simp

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:
simp

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:
simp

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
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 0 < 2

Tactic:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
h : G.Adj w u'
r1 : G.Walk u' u
r2 : G.Walk v v'
⊢ cons h ((r1.append p).append r2) = ((cons h r1).append p).append r2

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil.mpr
V : Type u_1
G : SimpleGraph V
u' : V
w✝ : u' = u'
h✝ : nil = nil.copy ⋯ w✝
⊢ nil.IsSubwalk nil

Tactic:
simp

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:
simp [IsSubwalk]

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:
simp

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:
simp

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert p.length = p.getVert (p.length - p.length)
hi : ¬p.length < p.length
⊢ (cons ⋯ nil).getVert (p.length - p.length) = (cons h p).getVert (p.length + 1 - p.length)

Tactic:
simp

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
hi : ¬i < p.length
hi' : p.length < i
⊢ (cons ⋯ nil).getVert (i - p.length - Nat.succ 0 + Nat.succ 0) = (cons h p).getVert 0

Tactic:
simp

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

Goal state before:
pp: case e_8
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse = cons ⋯ p.reverse

Tactic:
simp

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

Goal state before:
pp: case e_4
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ p.reverse.reverse = p

Tactic:
simp

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

Goal state before:
pp: case e_6
V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRecAux Hnil Hconcat p.reverse ≍ ⋯ ▸ concatRecAux Hnil Hconcat p.reverse

Tactic:
simp

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

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

Tactic:
· simp!

Goal state after:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), (p✝.takeUntil u h).append (p✝.dropUntil u h) = p✝
a✝ : List.Mem u p✝.support
⊢ ((cons h✝ p✝).takeUntil u ⋯).append ((cons h✝ p✝).dropUntil u ⋯) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case h_1
V : Type u
G : SimpleGraph V
u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
h : u ∈ nil.support
⊢ ⋯.mpr nil = nil

Tactic:
simp

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

Goal state before:
pp: case h_2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w✝ : V
x✝² : G.Walk u w✝
x✝¹ : V
x✝ : x✝¹ ∈ x✝².support
v✝ : V
r✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : u ∈ (cons r✝ p✝).support
⊢ (if hx : u = u then Eq.ndrec (motive := fun u_1 ↦ u_1 ∈ (cons r✝ p✝).support → G.Walk u_1 v) (fun h ↦ cons r✝ p✝) hx h
    else p✝.dropUntil u ⋯) =
    cons r✝ p✝

Tactic:
simp

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 = (nil.append (p.takeUntil w h)).append (p.dropUntil w h)

Tactic:
simp

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 = ((p.takeUntil w h).append (p.dropUntil w h)).append nil

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ nil.support
⊢ List.count u✝ (nil.takeUntil u✝ h).support = 1

Tactic:
simp

Goal state after:
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), List.count u (p✝.takeUntil u h).support = 1
h✝ : G.Adj u v✝
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 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.support = p.support.dropLast.concat v

Tactic:
simp

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
hadj : G.Adj v w
⊢ p.support <+: (p.concat hadj).support

Tactic:
simp

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
hadj : G.Adj v w
⊢ p.support ⊆ (p.concat hadj).support

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ : V
h : u✝ ∈ nil.support
⊢ List.count s(u✝, x) (nil.takeUntil u✝ h).edges ≤ 1

Tactic:
simp

Goal state after:
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 x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
⊢ u = p.support.head ⋯

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
⊢ v = p.support.getLast ⋯

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
d : G.Dart
p : G.Walk u v
⊢ d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ u = (p.darts.head ⋯).toProd.1

Tactic:
simp

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u✝ v✝ w u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ v = (p.darts.getLast ⋯).toProd.2

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
u✝ : V
q : G.Walk u✝ w
hx : u✝ ∈ nil.support
⊢ (nil.append q).takeUntil u✝ ⋯ = nil.takeUntil u✝ hx

Tactic:
simp

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.edges.Nodup

Tactic:
simp

Goal state after: