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

Goal state before:
pp: case cons
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 : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : Walk.map f' (Walk.map f p✝) = Walk.map (f'.comp f) p✝
⊢ Walk.map f' (Walk.map f (cons h✝ p✝)) = Walk.map (f'.comp f) (cons h✝ p✝)

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 : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).length = nil.length

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
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).length = p✝.length
⊢ (Walk.map f (cons h✝ p✝)).length = (cons h✝ p✝).length

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 w u✝ : V
q : G.Walk u✝ w
⊢ Walk.map f (nil.append q) = (Walk.map f nil).append (Walk.map f q)

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 w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), Walk.map f (p✝.append q) = (Walk.map f p✝).append (Walk.map f q)
q : G.Walk w✝ w
⊢ Walk.map f ((cons h✝ p✝).append q) = (Walk.map f (cons h✝ p✝)).append (Walk.map f q)

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 : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).support = List.map (⇑f) nil.support

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
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).support = List.map (⇑f) p✝.support
⊢ (Walk.map f (cons h✝ p✝)).support = List.map (⇑f) (cons h✝ p✝).support

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 : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).darts = List.map f.mapDart nil.darts

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
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).darts = List.map f.mapDart p✝.darts
⊢ (Walk.map f (cons h✝ p✝)).darts = List.map f.mapDart (cons h✝ p✝).darts

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 : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).edges = List.map (Sym2.map ⇑f) nil.edges

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
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).edges = List.map (Sym2.map ⇑f) p✝.edges
⊢ (Walk.map f (cons h✝ p✝)).edges = List.map (Sym2.map ⇑f) (cons h✝ p✝).edges

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 ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, nil = cons h q

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 ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, cons h✝ p✝ = cons h q

Tactic:
simp [*]

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

Goal state before:
pp: case nil.zero
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
⊢ (Walk.map f nil).getVert 0 = f (nil.getVert 0)

Tactic:
simp [*]

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

Goal state before:
pp: case nil.succ
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ : V
n✝ : ℕ
⊢ (Walk.map f nil).getVert (n✝ + 1) = f (nil.getVert (n✝ + 1))

Tactic:
simp [*]

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

Goal state before:
pp: case cons.zero
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
⊢ (Walk.map f (cons h✝ p✝)).getVert 0 = f ((cons h✝ p✝).getVert 0)

Tactic:
simp [*]

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

Goal state before:
pp: case cons.succ
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
n✝ : ℕ
⊢ (Walk.map f (cons h✝ p✝)).getVert (n✝ + 1) = f ((cons h✝ p✝).getVert (n✝ + 1))

Tactic:
simp [*]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u✝ : V
⊢ nil.transfer G ⋯ = nil

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.transfer G ⋯ = p✝
⊢ (cons h✝ p✝).transfer G ⋯ = cons h✝ p✝

Tactic:
simp [*]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
GH : G ≤ H
u✝ : V
hp : ∀ e ∈ nil.edges, e ∈ H.edgeSet
⊢ nil.transfer H hp = Walk.map (Hom.ofLE GH) nil

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
GH : G ≤ H
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), p✝.transfer H hp = Walk.map (Hom.ofLE GH) p✝
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ (cons h✝ p✝).transfer H hp = Walk.map (Hom.ofLE GH) (cons h✝ p✝)

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).edges = p✝.edges
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).edges = (cons h✝ p✝).edges

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).support = p✝.support
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).support = (cons h✝ p✝).support

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).length = p✝.length
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).length = (cons h✝ p✝).length

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H K : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet) (hp' : ∀ e ∈ (p✝.transfer H hp).edges, e ∈ K.edgeSet),
    (p✝.transfer H hp).transfer K hp' = p✝.transfer K ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
hp' : ∀ e ∈ ((cons h✝ p✝).transfer H hp).edges, e ∈ K.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).transfer K hp' = (cons h✝ p✝).transfer K ⋯

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 w x : V
r : G.Walk w x
u✝ : V
q : G.Walk u✝ w
⊢ nil.append (q.append r) = (nil.append q).append r

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x : V
r : G.Walk w x
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (q : G.Walk w✝ w), p✝.append (q.append r) = (p✝.append q).append r
q : G.Walk w✝ w
⊢ (cons h✝ p✝).append (q.append r) = ((cons h✝ p✝).append q).append r

Tactic:
simp [*]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u✝ : V
q : G.Walk u✝ w
hpq : ∀ e ∈ (nil.append q).edges, e ∈ H.edgeSet
⊢ (nil.append q).transfer H hpq = (nil.transfer H ⋯).append (q.transfer H ⋯)

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (hpq : ∀ e ∈ (p✝.append q).edges, e ∈ H.edgeSet),
    (p✝.append q).transfer H hpq = (p✝.transfer H ⋯).append (q.transfer H ⋯)
q : G.Walk w✝ w
hpq : ∀ e ∈ ((cons h✝ p✝).append q).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).append q).transfer H hpq = ((cons h✝ p✝).transfer H ⋯).append (q.transfer H ⋯)

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (hp : ∀ e ∈ p✝.edges, e ∈ H.edgeSet), (p✝.transfer H hp).reverse = p✝.reverse.transfer H ⋯
hp : ∀ e ∈ (cons h✝ p✝).edges, e ∈ H.edgeSet
⊢ ((cons h✝ p✝).transfer H hp).reverse = (cons h✝ p✝).reverse.transfer H ⋯

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

Tactic:
induction p with
  | nil => simp!
  | cons _ _ ih => simp [ih, Nat.succ_add, add_assoc]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 < nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

Tactic:
simp [*]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 < nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

Tactic:
simp [*]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i < p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).getVert 0 =
    if 0 < (cons h✝ p✝).length then (cons h✝ p✝).getVert 0 else q.getVert (0 - (cons h✝ p✝).length)

Tactic:
simp [*]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i < p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
n✝ : ℕ
⊢ ((cons h✝ p✝).append q).getVert (n✝ + 1) =
    if n✝ + 1 < (cons h✝ p✝).length then (cons h✝ p✝).getVert (n✝ + 1) else q.getVert (n✝ + 1 - (cons h✝ p✝).length)

Tactic:
simp [*]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).getVert 0 = if 0 ≤ nil.length then nil.getVert 0 else q.getVert (0 - nil.length)

Tactic:
simp [*]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
n✝ : ℕ
⊢ (nil.append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ nil.length then nil.getVert (n✝ + 1) else q.getVert (n✝ + 1 - nil.length)

Tactic:
simp [*]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i ≤ p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).getVert 0 =
    if 0 ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert 0 else q.getVert (0 - (cons h✝ p✝).length)

Tactic:
simp [*]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ :
  ∀ (q : G.Walk w✝ w) (i : ℕ),
    (p✝.append q).getVert i = if i ≤ p✝.length then p✝.getVert i else q.getVert (i - p✝.length)
q : G.Walk w✝ w
n✝ : ℕ
⊢ ((cons h✝ p✝).append q).getVert (n✝ + 1) =
    if n✝ + 1 ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert (n✝ + 1) else q.getVert (n✝ + 1 - (cons h✝ p✝).length)

Tactic:
simp [*]

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

Goal state before:
pp: case refine_2.refine_2
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₂.getVert (s.length + p₁.length) = w

pp: case refine_2.refine_3
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₂ = (((p₂.take s.length).copy ⋯ ⋯).append p₁).append ((p₂.drop (s.length + p₁.length)).copy ?refine_2.refine_2 ⋯)

Tactic:
· simp [p₂.getVert_eq_support_getElem this, ← h, ← p₁.getVert_eq_support_getElem le_rfl]

Goal state after:
case refine_2.refine_3
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₂ = (((p₂.take s.length).copy ⋯ ⋯).append p₁).append ((p₂.drop (s.length + p₁.length)).copy ⋯ ⋯)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
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
⊢ (⋯ ▸ nil).append (Eq.rec (motive := fun x x_1 ↦ x ∈ u✝ :: p✝.support → G.Walk x w✝) (fun h ↦ cons h✝ p✝) ⋯ ⋯) =
    cons h✝ p✝

Tactic:
simp [*]

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

Goal state before:
pp: case neg
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
h' : ¬u✝ = u
⊢ (cons h✝ (p✝.takeUntil u ⋯)).append (p✝.dropUntil u ⋯) = cons h✝ p✝

Tactic:
simp [*]

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

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u v w : V
⊢ (nil.append nil).support = nil.support ++ nil.support.tail

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w
p_ih✝ : ∀ (p' : G.Walk w w), (p✝.append p').support = p✝.support ++ p'.support.tail
⊢ ((cons h✝ p✝).append nil).support = (cons h✝ p✝).support ++ nil.support.tail

Tactic:
simp [*]

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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝¹.append p').support = p✝¹.support ++ p'.support.tail
v✝ : V
h✝ : G.Adj w✝ v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).support = (cons h✝¹ p✝¹).support ++ (cons h✝ p✝).support.tail

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 w u✝ : V
p' : G.Walk u✝ w
⊢ (nil.append p').darts = nil.darts ++ p'.darts

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (p' : G.Walk w✝ w), (p✝.append p').darts = p✝.darts ++ p'.darts
p' : G.Walk w✝ w
⊢ ((cons h✝ p✝).append p').darts = (cons h✝ p✝).darts ++ p'.darts

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 v w
h : u ∈ p.support
⊢ (p.takeUntil u h).support <+: p.support

Tactic:
by
  grw [takeUntil_eq_take, support_copy, support_take, List.take_prefix]

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
⊢ nil.reverse.darts = (List.map Dart.symm nil.darts).reverse

Tactic:
simp [*]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.darts = (List.map Dart.symm p✝.darts).reverse
⊢ (cons h✝ p✝).reverse.darts = (List.map Dart.symm (cons h✝ p✝).darts).reverse

Tactic:
simp [*]

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

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:
have := hcyc.2

Goal state after:
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
this : (p.append q).support.tail.Nodup
⊢ q.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - n ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia

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
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - m ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
simp only [Walk.length_reverse, Set.mem_ofPred_eq]; lia

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ {a, b, c} = {a, b, c}

Tactic:
simp [*]

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

Goal state before:
pp: case mpr.refine_2
α : Type u_1
G : SimpleGraph α
a b : α
hab✝ : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ a ∈ {a, b, c} ∧ b ∈ {a, b, c}

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFree n ↔ IsEmpty ((completeGraph (Fin n)).Copy G)

Tactic:
contrapose!
  exact not_cliqueFree_iff_top_isContained n

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
h : s(u, v) ∈ p.edges
⊢ p.length = 1

Tactic:
suffices p.length - 1 = 0 by grind [length_edges]
  rw [← hp.getVert_eq_start_iff <| p.length.sub_le 1]
  exact (hp.eq_penultimate_of_mem_edges <| Sym2.eq_swap ▸ h).symm

Goal state after: