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

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

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✝ : w✝ ∈ p✝.support
⊢ w✝ ∈ (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ u✝ ∈ nil.support

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✝ : w✝ ∈ p✝.support
⊢ w✝ ∈ (cons h✝ p✝).support
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

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

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

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

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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ ↑nil.support = {u} + ↑nil.support.tail

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) nil.darts = nil.support

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✝ : v✝ :: List.map (fun x ↦ x.toProd.2) p✝.darts = p✝.support
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) (cons h✝ p✝).darts = (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) nil.darts = nil.support

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✝ : v✝ :: List.map (fun x ↦ x.toProd.2) p✝.darts = p✝.support
⊢ u✝ :: List.map (fun x ↦ x.toProd.2) (cons h✝ p✝).darts = (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ List.map (fun x ↦ x.toProd.1) nil.darts ++ [u✝] = nil.support

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✝ : List.map (fun x ↦ x.toProd.1) p✝.darts ++ [w✝] = p✝.support
⊢ List.map (fun x ↦ x.toProd.1) (cons h✝ p✝).darts ++ [w✝] = (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ List.map (fun x ↦ x.toProd.1) nil.darts ++ [u✝] = nil.support

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✝ : List.map (fun x ↦ x.toProd.1) p✝.darts ++ [w✝] = p✝.support
⊢ List.map (fun x ↦ x.toProd.1) (cons h✝ p✝).darts ++ [w✝] = (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.support.length = nil.length + 1

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✝.support.length = p✝.length + 1
⊢ (cons h✝ p✝).support.length = (cons h✝ p✝).length + 1

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.support.length = nil.length + 1

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✝.support.length = p✝.length + 1
⊢ (cons h✝ p✝).support.length = (cons h✝ p✝).length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.darts.length = nil.length

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✝.darts.length = p✝.length
⊢ (cons h✝ p✝).darts.length = (cons h✝ p✝).length

Tactic:
<;>

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

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✝.darts.length = p✝.length
⊢ (cons h✝ p✝).darts.length = (cons h✝ p✝).length
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

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

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

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

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

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✝.support[p✝.length] = w✝
⊢ (cons h✝ p✝).support[(cons h✝ p✝).length] = w✝

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.support[nil.length] = u✝

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✝.support[p✝.length] = w✝
⊢ (cons h✝ p✝).support[(cons h✝ p✝).length] = w✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
hs : s ∈ (equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1

pp: case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
hs : s ∈ (equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
h✝ : #U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
hs : s ∈ (equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1

case neg
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
h✝ : ¬#U = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)
hs : s ∈ (equitabilise ⋯).parts
⊢ #s = m ∨ #s = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.map Hom.id 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✝ : Walk.map Hom.id p✝ = p✝
⊢ Walk.map Hom.id (cons h✝ p✝) = cons h✝ p✝

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.map Hom.id 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✝ : Walk.map Hom.id p✝ = p✝
⊢ Walk.map Hom.id (cons h✝ p✝) = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case e'_3.e'_3
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
this✝ : ∀ (h : 0 < [u', v'].length), p.support[0 + i]? = some [u', v'][0]
this : ∀ (h : 1 < [u', v'].length), p.support[1 + i]? = some [u', v'][1]
⊢ u' = p.darts[i].1.1

pp: case e'_3.e'_4
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
this✝ : ∀ (h : 0 < [u', v'].length), p.support[0 + i]? = some [u', v'][0]
this : ∀ (h : 1 < [u', v'].length), p.support[1 + i]? = some [u', v'][1]
⊢ v' = p.darts[i].1.2

Tactic:
<;>

Goal state after:
case e'_3.e'_3
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
this✝ : ∀ (h : 0 < [u', v'].length), p.support[0 + i]? = some [u', v'][0]
this : ∀ (h : 1 < [u', v'].length), p.support[1 + i]? = some [u', v'][1]
⊢ u' = p.darts[i].1.1

case e'_3.e'_4
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝ : G.Adj u' v'
x✝ :
  ∃ k,
    [u', v'].length + k ≤ p.support.length ∧ ∀ (i : ℕ) (h : i < [u', v'].length), p.support[i + k]? = some [u', v'][i]
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h : ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length), p.support[i_1 + i]? = some [u', v'][i_1]
this✝ : ∀ (h : 0 < [u', v'].length), p.support[0 + i]? = some [u', v'][0]
this : ∀ (h : 1 < [u', v'].length), p.support[1 + i]? = some [u', v'][1]
⊢ v' = p.darts[i].1.2
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: case nil
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
⊢ Walk.map f' (Walk.map f nil) = Walk.map (f'.comp f) nil

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

Goal state after:
case nil
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
⊢ Walk.map f' (Walk.map f nil) = Walk.map (f'.comp f) nil

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.support ↔ w = u✝ ∨ ∃ e ∈ nil.edges, w ∈ e

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✝ : w ∈ p✝.support ↔ w = w✝ ∨ ∃ e ∈ p✝.edges, w ∈ e
⊢ w ∈ (cons h✝ p✝).support ↔ w = w✝ ∨ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.support ↔ w = u✝ ∨ ∃ e ∈ nil.edges, w ∈ e

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✝ : w ∈ p✝.support ↔ w = w✝ ∨ ∃ e ∈ p✝.edges, w ∈ e
⊢ w ∈ (cons h✝ p✝).support ↔ w = w✝ ∨ ∃ e ∈ (cons h✝ p✝).edges, w ∈ e
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

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

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

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

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

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

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

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

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

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

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

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
⊢ (Walk.map f nil).length = nil.length

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

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

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

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

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

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

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]
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).reverse = Walk.map f nil.reverse

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✝).reverse = Walk.map f p✝.reverse
⊢ (Walk.map f (cons h✝ p✝)).reverse = Walk.map f (cons h✝ p✝).reverse

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
⊢ (Walk.map f nil).reverse = Walk.map f nil.reverse

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✝).reverse = Walk.map f p✝.reverse
⊢ (Walk.map f (cons h✝ p✝)).reverse = Walk.map f (cons h✝ p✝).reverse
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

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

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

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

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

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

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

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

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

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

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
⊢ (Walk.map f nil).support = List.map (⇑f) nil.support

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

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

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

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

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

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
⊢ (Walk.map f nil).darts = List.map f.mapDart nil.darts

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

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

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
⊢ (Walk.map f nil).edges = List.map (Sym2.map ⇑f) nil.edges

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

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

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

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