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

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

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

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✝.take n).length = min n p✝.length
⊢ ((cons h✝ p✝).take 0).length = min 0 (cons h✝ p✝).length

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✝.take n).length = min n p✝.length
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).length = min (n✝ + 1) (cons h✝ p✝).length

Tactic:
<;>

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

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

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✝.take n).length = min n p✝.length
⊢ ((cons h✝ p✝).take 0).length = min 0 (cons h✝ p✝).length

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✝.take n).length = min n p✝.length
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).length = min (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 u✝ : V
n m : ℕ
⊢ (nil.take n).getVert m = nil.getVert (min n m)

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n m : ℕ
⊢ ((cons h✝ p✝).take n).getVert m = (cons h✝ p✝).getVert (min n m)

Tactic:
<;>

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

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
n m : ℕ
⊢ ((cons h✝ p✝).take n).getVert m = (cons h✝ p✝).getVert (min n m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

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

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

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m : ℕ
⊢ ((cons h✝ p✝).take 0).getVert m = (cons h✝ p✝).getVert (min 0 m)

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (min (n✝ + 1) m)

Tactic:
<;>

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

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

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m : ℕ
⊢ ((cons h✝ p✝).take 0).getVert m = (cons h✝ p✝).getVert (min 0 m)

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 m : ℕ), (p✝.take n).getVert m = p✝.getVert (min n m)
m n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).getVert m = (cons h✝ p✝).getVert (min (n✝ + 1) m)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail → p.IsTrail

pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsTrail → p.reverse.IsTrail

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsTrail → p.IsTrail

case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsTrail → p.reverse.IsTrail
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case isTrail
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsTrail

pp: case support_nodup
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.support.Nodup

Tactic:
<;>

Goal state after:
case isTrail
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.IsTrail

case support_nodup
V : Type u
G : SimpleGraph V
u : V
⊢ Walk.nil.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath ∧ u ∉ p.support

pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ p.IsPath ∧ u ∉ p.support → (cons h p).IsPath

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath → p.IsPath ∧ u ∉ p.support

case mpr
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ p.IsPath ∧ u ∉ p.support → (cons h p).IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

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

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

Tactic:
<;>

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

case cons
V : Type u
G : SimpleGraph V
u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ u
⊢ (cons h✝ p✝).IsPath ↔ (cons h✝ p✝).Nil
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath → p.IsPath

pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath → p.reverse.IsPath

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.IsPath → p.IsPath

case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.IsPath → p.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p.IsPath

pp: case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath

Tactic:
<;>

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.reverse.IsPath
⊢ p.IsPath

case mpr
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsPath
⊢ p.reverse.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Paths

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

Tactic:
rw [← isPath_reverse_iff] at h ⊢
  rw [reverse_append] at h
  apply h.of_append_left

Goal state after:
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.take (m + n) ≍ (nil.take n).append ((nil.drop n).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n : ℕ
⊢ (cons h✝ p✝).take (m + n) ≍ ((cons h✝ p✝).take n).append (((cons h✝ p✝).drop n).take m)

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n : ℕ
⊢ nil.take (m + n) ≍ (nil.take n).append ((nil.drop n).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n : ℕ
⊢ (cons h✝ p✝).take (m + n) ≍ ((cons h✝ p✝).take n).append (((cons h✝ p✝).drop n).take m)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse.IsPath ↔ p.IsPath ∧ w ∉ p.support

Tactic:
← p.isPath_reverse_iff,

Goal state after:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).reverse.IsPath ↔ p.reverse.IsPath ∧ w ∉ p.support
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.take (m + 0) ≍ (nil.take 0).append ((nil.drop 0).take m)

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.take (m + (n✝ + 1)) ≍ (nil.take (n✝ + 1)).append ((nil.drop (n✝ + 1)).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
⊢ (cons h✝ p✝).take (m + 0) ≍ ((cons h✝ p✝).take 0).append (((cons h✝ p✝).drop 0).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n✝ : ℕ
⊢ (cons h✝ p✝).take (m + (n✝ + 1)) ≍ ((cons h✝ p✝).take (n✝ + 1)).append (((cons h✝ p✝).drop (n✝ + 1)).take m)

Tactic:
<;>

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

case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.take (m + (n✝ + 1)) ≍ (nil.take (n✝ + 1)).append ((nil.drop (n✝ + 1)).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
⊢ (cons h✝ p✝).take (m + 0) ≍ ((cons h✝ p✝).take 0).append (((cons h✝ p✝).drop 0).take 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✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n✝ : ℕ
⊢ (cons h✝ p✝).take (m + (n✝ + 1)) ≍ ((cons h✝ p✝).take (n✝ + 1)).append (((cons h✝ p✝).drop (n✝ + 1)).take m)
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ (nil.take n).Nil ↔ nil.Nil ∨ n = 0

pp: case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).take n).Nil ↔ (cons h✝ p✝).Nil ∨ n = 0

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ (nil.take n).Nil ↔ nil.Nil ∨ n = 0

case cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ ((cons h✝ p✝).take n).Nil ↔ (cons h✝ p✝).Nil ∨ n = 0
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.take 0).Nil ↔ nil.Nil ∨ 0 = 0

pp: case nil.succ
V : Type u
G : SimpleGraph V
u : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).Nil ↔ nil.Nil ∨ n✝ + 1 = 0

pp: case cons.zero
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 ↔ (cons h✝ p✝).Nil ∨ 0 = 0

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).Nil ↔ (cons h✝ p✝).Nil ∨ n✝ + 1 = 0

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u : V
⊢ (nil.take 0).Nil ↔ nil.Nil ∨ 0 = 0

case nil.succ
V : Type u
G : SimpleGraph V
u : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).Nil ↔ nil.Nil ∨ n✝ + 1 = 0

case cons.zero
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 ↔ (cons h✝ p✝).Nil ∨ 0 = 0

case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).Nil ↔ (cons h✝ p✝).Nil ∨ n✝ + 1 = 0
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).support = List.take (n + 1) 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✝ : ∀ (n : ℕ), (p✝.take n).support = List.take (n + 1) p✝.support
n : ℕ
⊢ ((cons h✝ p✝).take n).support = List.take (n + 1) (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
n : ℕ
⊢ (nil.take n).support = List.take (n + 1) 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✝ : ∀ (n : ℕ), (p✝.take n).support = List.take (n + 1) p✝.support
n : ℕ
⊢ ((cons h✝ p✝).take n).support = List.take (n + 1) (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).support = List.take (0 + 1) nil.support

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

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

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✝.take n).support = List.take (n + 1) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).support = List.take (n✝ + 1 + 1) (cons h✝ p✝).support

Tactic:
<;>

Goal state after:
case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.take 0).support = List.take (0 + 1) nil.support

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

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

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✝.take n).support = List.take (n + 1) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).support = List.take (n✝ + 1 + 1) (cons h✝ p✝).support
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case zero.nil
V : Type u
G : SimpleGraph V
v : V
h : nil.length ≤ 0
⊢ nil.take 0 = nil.copy ⋯ ⋯

pp: case zero.cons
V : Type u
G : SimpleGraph V
v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).take 0 = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
<;>

Goal state after:
case zero.nil
V : Type u
G : SimpleGraph V
v : V
h : nil.length ≤ 0
⊢ nil.take 0 = nil.copy ⋯ ⋯

case zero.cons
V : Type u
G : SimpleGraph V
v u v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : (cons h✝ p✝).length ≤ 0
⊢ (cons h✝ p✝).take 0 = (cons h✝ p✝).copy ⋯ ⋯
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this : Fintype ↑G.edgeSet
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length

Tactic:
let s := {n | ∃ (u v : V) (p : G.Walk u v), p.IsTrail ∧ p.length = n}

Goal state after:
V : Type u
G : SimpleGraph V
N : Nonempty V
inst✝ : Finite ↑G.edgeSet
this : Fintype ↑G.edgeSet
s : Set ℕ := {n | ∃ u v p, p.IsTrail ∧ p.length = n}
⊢ ∃ u v p, ∃ (_ : p.IsTrail), ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsTrail → p'.length ≤ p.length
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).darts = List.take 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✝.take n).darts = List.take n p✝.darts
n : ℕ
⊢ ((cons h✝ p✝).take n).darts = List.take n (cons h✝ p✝).darts

Tactic:
<;>

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

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).darts = List.take (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✝.take n).darts = List.take n p✝.darts
⊢ ((cons h✝ p✝).take 0).darts = List.take 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✝.take n).darts = List.take n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).darts = List.take (n✝ + 1) (cons h✝ p✝).darts

Tactic:
<;>

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

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).darts = List.take (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✝.take n).darts = List.take n p✝.darts
⊢ ((cons h✝ p✝).take 0).darts = List.take 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✝.take n).darts = List.take n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).darts = List.take (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.take n).edges = List.take 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✝.take n).edges = List.take n p✝.edges
n : ℕ
⊢ ((cons h✝ p✝).take n).edges = List.take n (cons h✝ p✝).edges

Tactic:
<;>

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

pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).edges = List.take (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✝.take n).edges = List.take n p✝.edges
⊢ ((cons h✝ p✝).take 0).edges = List.take 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✝.take n).edges = List.take n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).edges = List.take (n✝ + 1) (cons h✝ p✝).edges

Tactic:
<;>

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

case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.take (n✝ + 1)).edges = List.take (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✝.take n).edges = List.take n p✝.edges
⊢ ((cons h✝ p✝).take 0).edges = List.take 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✝.take n).edges = List.take n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).take (n✝ + 1)).edges = List.take (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.reverse.penultimate = nil.snd

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✝).reverse.penultimate = (cons h✝ p✝).snd

Tactic:
<;>

Goal state after:
case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.reverse.penultimate = nil.snd

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✝).reverse.penultimate = (cons h✝ p✝).snd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.drop 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✝).drop 0 = (cons h✝ p✝).copy ⋯ ⋯

Tactic:
<;>

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

Tactic:
<;>

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
⊢ n = m

pp: case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
⊢ n = m

Tactic:
<;>

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : n = 0
⊢ n = m

case neg
V : Type u
G : SimpleGraph V
u✝ v✝ v w u : V
h : G.Adj v w
p : G.Walk w u
ihp :
  p.IsPath → ∀ ⦃n : ℕ⦄, n ∈ {i | i ≤ p.length} → ∀ ⦃m : ℕ⦄, m ∈ {i | i ≤ p.length} → p.getVert n = p.getVert m → n = m
hp : (cons h p).IsPath
n : ℕ
hn : n ≤ p.length + 1
m : ℕ
hm : m ≤ p.length + 1
hnm : (cons h p).getVert n = (cons h p).getVert m
hn0 : ¬n = 0
⊢ n = m