mathlib-initiative/mathlib-tactics huggingface dataset:
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

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

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.darts = (List.map Dart.symm nil.darts).reverse

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ { fst := u', snd := v', adj := h✝² } ∈ p.darts

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
<;>

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ { fst := u', snd := v', adj := h✝² } ∈ p.darts

case refine_2
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := v', snd := u', adj := ⋯ } ∈ p.darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd

pp: case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd

Tactic:
<;>

Goal state after:
case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd

case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h✝ : n < (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

pp: case inr
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h✝ : n = (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

Tactic:
<;>

Goal state after:
case inl
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h✝ : n < (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

case inr
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h✝ : n = (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ.nil
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
⊢ (nil.drop (n✝ + 1 + 1)).IsSubwalk (nil.drop (n✝ + 1))

pp: case succ.cons
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).drop (n✝ + 1 + 1)).IsSubwalk ((cons h✝ p✝).drop (n✝ + 1))

Tactic:
<;>

Goal state after:
case succ.nil
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
⊢ (nil.drop (n✝ + 1 + 1)).IsSubwalk (nil.drop (n✝ + 1))

case succ.cons
V : Type u_1
G : SimpleGraph V
v : V
n k n✝ : ℕ
ih : ∀ {u : V} (p : G.Walk u v), (p.drop (n✝ + 1)).IsSubwalk (p.drop n✝)
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).drop (n✝ + 1 + 1)).IsSubwalk ((cons h✝ p✝).drop (n✝ + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
⊢ (nil.append q).Nil ↔ nil.Nil ∧ q.Nil

pp: case cons
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append q).Nil ↔ (cons h✝ p✝).Nil ∧ q.Nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
⊢ (nil.append q).Nil ↔ nil.Nil ∧ q.Nil

case cons
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append q).Nil ↔ (cons h✝ p✝).Nil ∧ q.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.nil
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.append nil).Nil ↔ nil.Nil ∧ nil.Nil

pp: case nil.cons
V : Type u
G : SimpleGraph V
u w v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).Nil ↔ nil.Nil ∧ (cons h✝ p✝).Nil

pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append nil).Nil ↔ (cons h✝ p✝).Nil ∧ nil.Nil

pp: case cons.cons
V : Type u
G : SimpleGraph V
u v w v✝¹ : V
h✝¹ : G.Adj u v✝¹
p✝¹ : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).Nil ↔ (cons h✝¹ p✝¹).Nil ∧ (cons h✝ p✝).Nil

Tactic:
<;>

Goal state after:
case nil.nil
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.append nil).Nil ↔ nil.Nil ∧ nil.Nil

case nil.cons
V : Type u
G : SimpleGraph V
u w v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
⊢ (nil.append (cons h✝ p✝)).Nil ↔ nil.Nil ∧ (cons h✝ p✝).Nil

case cons.nil
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).append nil).Nil ↔ (cons h✝ p✝).Nil ∧ nil.Nil

case cons.cons
V : Type u
G : SimpleGraph V
u v w v✝¹ : V
h✝¹ : G.Adj u v✝¹
p✝¹ : G.Walk v✝¹ v
v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ w
⊢ ((cons h✝¹ p✝¹).append (cons h✝ p✝)).Nil ↔ (cons h✝¹ p✝¹).Nil ∧ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.reverse.Nil ↔ 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✝).reverse.Nil ↔ (cons h✝ p✝).Nil

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
v : V
⊢ nil.reverse.Nil ↔ 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✝).reverse.Nil ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).length = nil.length - n

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✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n : ℕ
⊢ ((cons h✝ p✝).drop n).length = (cons h✝ p✝).length - n

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).length = nil.length - n

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✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n : ℕ
⊢ ((cons h✝ p✝).drop n).length = (cons h✝ p✝).length - n
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).length = nil.length - 0

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).length = nil.length - (n✝ + 1)

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
⊢ ((cons h✝ p✝).drop 0).length = (cons h✝ p✝).length - 0

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).length = (cons h✝ p✝).length - (n✝ + 1)

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).length = nil.length - 0

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).length = nil.length - (n✝ + 1)

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
⊢ ((cons h✝ p✝).drop 0).length = (cons h✝ p✝).length - 0

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).length = (cons h✝ p✝).length - (n✝ + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ (nil.drop n).getVert m = nil.getVert (n + m)

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n : ℕ
⊢ ((cons h✝ p✝).drop n).getVert m = (cons h✝ p✝).getVert (n + m)

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ (nil.drop n).getVert m = nil.getVert (n + m)

case cons
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n : ℕ
⊢ ((cons h✝ p✝).drop n).getVert m = (cons h✝ p✝).getVert (n + m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ (nil.drop 0).getVert m = nil.getVert (0 + m)

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).getVert m = nil.getVert (n✝ + 1 + m)

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
⊢ ((cons h✝ p✝).drop 0).getVert m = (cons h✝ p✝).getVert (0 + m)

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (n✝ + 1 + m)

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ (nil.drop 0).getVert m = nil.getVert (0 + m)

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).getVert m = nil.getVert (n✝ + 1 + m)

case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
⊢ ((cons h✝ p✝).drop 0).getVert m = (cons h✝ p✝).getVert (0 + m)

case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).getVert m = p✝.getVert (n + m)
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (n✝ + 1 + m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ nil.drop (m + n) ≍ (nil.drop n).drop m

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n : ℕ
⊢ (cons h✝ p✝).drop (m + n) ≍ ((cons h✝ p✝).drop n).drop m

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ nil.drop (m + n) ≍ (nil.drop n).drop m

case cons
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n : ℕ
⊢ (cons h✝ p✝).drop (m + n) ≍ ((cons h✝ p✝).drop n).drop m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.drop (m + 0) ≍ (nil.drop 0).drop m

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.drop (m + (n✝ + 1)) ≍ (nil.drop (n✝ + 1)).drop m

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
⊢ (cons h✝ p✝).drop (m + 0) ≍ ((cons h✝ p✝).drop 0).drop m

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n✝ : ℕ
⊢ (cons h✝ p✝).drop (m + (n✝ + 1)) ≍ ((cons h✝ p✝).drop (n✝ + 1)).drop m

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.drop (m + 0) ≍ (nil.drop 0).drop m

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.drop (m + (n✝ + 1)) ≍ (nil.drop (n✝ + 1)).drop m

case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
⊢ (cons h✝ p✝).drop (m + 0) ≍ ((cons h✝ p✝).drop 0).drop m

case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n✝ : ℕ
⊢ (cons h✝ p✝).drop (m + (n✝ + 1)) ≍ ((cons h✝ p✝).drop (n✝ + 1)).drop m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).Nil ↔ nil.length ≤ n

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

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).Nil ↔ nil.length ≤ n

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✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
n : ℕ
⊢ ((cons h✝ p✝).drop n).Nil ↔ (cons h✝ p✝).length ≤ n
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).Nil ↔ nil.length ≤ 0

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).Nil ↔ nil.length ≤ n✝ + 1

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
⊢ ((cons h✝ p✝).drop 0).Nil ↔ (cons h✝ p✝).length ≤ 0

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).Nil ↔ (cons h✝ p✝).length ≤ n✝ + 1

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).Nil ↔ nil.length ≤ 0

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).Nil ↔ nil.length ≤ n✝ + 1

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
⊢ ((cons h✝ p✝).drop 0).Nil ↔ (cons h✝ p✝).length ≤ 0

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).Nil ↔ (cons h✝ p✝).length ≤ n✝ + 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).darts = List.drop n nil.darts

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

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).darts = List.drop n nil.darts

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✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
n : ℕ
⊢ ((cons h✝ p✝).drop n).darts = List.drop n (cons h✝ p✝).darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).darts = List.drop 0 nil.darts

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).darts = List.drop (n✝ + 1) nil.darts

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
⊢ ((cons h✝ p✝).drop 0).darts = List.drop 0 (cons h✝ p✝).darts

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).darts = List.drop (n✝ + 1) (cons h✝ p✝).darts

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).darts = List.drop 0 nil.darts

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).darts = List.drop (n✝ + 1) nil.darts

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
⊢ ((cons h✝ p✝).drop 0).darts = List.drop 0 (cons h✝ p✝).darts

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).darts = List.drop (n✝ + 1) (cons h✝ p✝).darts
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).edges = List.drop n nil.edges

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

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.drop n).edges = List.drop n nil.edges

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✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
n : ℕ
⊢ ((cons h✝ p✝).drop n).edges = List.drop n (cons h✝ p✝).edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).edges = List.drop 0 nil.edges

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).edges = List.drop (n✝ + 1) nil.edges

pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
⊢ ((cons h✝ p✝).drop 0).edges = List.drop 0 (cons h✝ p✝).edges

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).edges = List.drop (n✝ + 1) (cons h✝ p✝).edges

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).edges = List.drop 0 nil.edges

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).edges = List.drop (n✝ + 1) nil.edges

case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
⊢ ((cons h✝ p✝).drop 0).edges = List.drop 0 (cons h✝ p✝).edges

case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).edges = List.drop (n✝ + 1) (cons h✝ p✝).edges
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.take 0 = nil.copy ⋯ ⋯

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

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.take 0 = nil.copy ⋯ ⋯

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✝).take 0 = nil.copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.take n).length = min n 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✝ : ∀ (n : ℕ), (p✝.take n).length = min n p✝.length
n : ℕ
⊢ ((cons h✝ p✝).take n).length = min n (cons h✝ p✝).length

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.take n).length = min n 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✝ : ∀ (n : ℕ), (p✝.take n).length = min n p✝.length
n : ℕ
⊢ ((cons h✝ p✝).take n).length = min n (cons h✝ p✝).length