mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
⊢ (Walk.map f nil).getVert n = f (nil.getVert n)

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✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
n : ℕ
⊢ (Walk.map f (cons h✝ p✝)).getVert n = f ((cons h✝ p✝).getVert n)

Tactic:
<;>

Goal state after:
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
n : ℕ
⊢ (Walk.map f nil).getVert n = f (nil.getVert n)

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✝ : ∀ (n : ℕ), (Walk.map f p✝).getVert n = f (p✝.getVert n)
n : ℕ
⊢ (Walk.map f (cons h✝ p✝)).getVert n = f ((cons h✝ p✝).getVert n)
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

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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ ¬nil.Nil ↔ ∃ u, ∃ (h : G.Adj v u), ∃ q, nil = cons h q

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
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)

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))

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)

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

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

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))

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)

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))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

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

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

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
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case nil.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

pp: case nil.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝

Tactic:
<;>

Goal state after:
case nil.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

case nil.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝
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

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

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

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✝
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

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

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

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✝)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h : G.Adj u✝ v✝
ih : ¬nil.Nil → (w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e)
hnil : ¬(cons h nil).Nil
⊢ w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e

pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w 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✝).Nil → (w ∈ (cons h✝ p✝).support ↔ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e)
hnil : ¬(cons h (cons h✝ p✝)).Nil
⊢ w ∈ (cons h (cons h✝ p✝)).support ↔ ∃ e ∈ (cons h (cons h✝ p✝)).edges, w ∈ e

Tactic:
<;>

Goal state after:
case cons.nil
V : Type u
G : SimpleGraph V
u v w u✝ v✝ : V
h : G.Adj u✝ v✝
ih : ¬nil.Nil → (w ∈ nil.support ↔ ∃ e ∈ nil.edges, w ∈ e)
hnil : ¬(cons h nil).Nil
⊢ w ∈ (cons h nil).support ↔ ∃ e ∈ (cons h nil).edges, w ∈ e

case cons.cons
V : Type u
G : SimpleGraph V
u v w 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✝).Nil → (w ∈ (cons h✝ p✝).support ↔ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e)
hnil : ¬(cons h (cons h✝ p✝)).Nil
⊢ w ∈ (cons h (cons h✝ p✝)).support ↔ ∃ e ∈ (cons h (cons h✝ p✝)).edges, w ∈ e
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

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

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

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

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

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

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

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

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

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

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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.append nil = nil

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✝
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)
⊢ 1 - ε ^ 5 / 50 ≤ (1 - 1 / (↑m + 1)) ^ 2

Tactic:
sub_sq,

Goal state after:
α : 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)
⊢ 1 - ε ^ 5 / 50 ≤ 1 ^ 2 - 2 * 1 * (1 / (↑m + 1)) + (1 / (↑m + 1)) ^ 2
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 ⋯

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

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

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 ⋯
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

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

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

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
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:
rw [concat_eq_append, ← append_assoc, cons_nil_append]

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 ⋯)

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

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

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 ⋯)
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 ⋯

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

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

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 ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).length = nil.length + q.length

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✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).length = p✝.length + q.length
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).length = (cons h✝ p✝).length + q.length

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
q : G.Walk u✝ w
⊢ (nil.append q).length = nil.length + q.length

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✝ : ∀ (q : G.Walk w✝ w), (p✝.append q).length = p✝.length + q.length
q : G.Walk w✝ w
⊢ ((cons h✝ p✝).append q).length = (cons h✝ p✝).length + q.length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

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✝ :
  ∀ (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
i : ℕ
⊢ ((cons h✝ p✝).append q).getVert i =
    if i < (cons h✝ p✝).length then (cons h✝ p✝).getVert i else q.getVert (i - (cons h✝ p✝).length)

Tactic:
<;>

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

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✝ :
  ∀ (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
i : ℕ
⊢ ((cons h✝ p✝).append q).getVert i =
    if i < (cons h✝ p✝).length then (cons h✝ p✝).getVert i else q.getVert (i - (cons h✝ p✝).length)
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)

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)

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)

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

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

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)

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)

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)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

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✝ :
  ∀ (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
i : ℕ
⊢ ((cons h✝ p✝).append q).getVert i =
    if i ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert i else q.getVert (i - (cons h✝ p✝).length)

Tactic:
<;>

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

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✝ :
  ∀ (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
i : ℕ
⊢ ((cons h✝ p✝).append q).getVert i =
    if i ≤ (cons h✝ p✝).length then (cons h✝ p✝).getVert i else q.getVert (i - (cons h✝ p✝).length)