awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil 0) (take Walk.nil 0))
    (List.take 0 (darts (u := u_1) Walk.nil))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := List G.Dart)
      (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (take Walk.nil (n + 1)))
      (List.take (n + 1) (darts (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil n) (take Walk.nil n))
    (List.take n (darts (u := u_1) Walk.nil))

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).darts = List.take n p.darts
n : ℕ
cons : darts (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) = List.take 0 (Walk.cons h p).darts
cons₁ :
  ∀ (n : ℕ),
    darts (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) =
      List.take (n + 1) (Walk.cons h p).darts
⊢ ((Walk.cons h p).take n).darts = List.take n (Walk.cons h p).darts

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0))
    (List.take 0 (darts (u := u_1) nil))

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u_1) (v := getVert (G := G) (u := u_1) nil (n + 1)) (take nil (n + 1)))
    (List.take (n + 1) (darts (u := u_1) nil))

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).darts = List.take n p.darts
⊢ darts (v := (cons h p).getVert 0) ((cons h p).take 0) = List.take 0 (cons h p).darts

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).darts = List.take n p.darts
n : ℕ
⊢ darts (v := (cons h p).getVert (n + 1)) ((cons h p).take (n + 1)) = List.take (n + 1) (cons h p).darts

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List (Sym2 V))
      (edges (G := G) (u := u) (v := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n))
      (List.take n (edges (G := G) (u := u) Walk.nil))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.take n).edges = List.take n p.edges) →
      ∀ (n : ℕ), ((Walk.cons h p).take n).edges = List.take n (Walk.cons h p).edges
⊢ (p.take n).edges = List.take n p.edges

Tactic:
induction p generalizing n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil 0) (take Walk.nil 0))
    (List.take 0 (edges (G := G) (u := u_1) Walk.nil))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := List (Sym2 V))
      (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (take Walk.nil (n + 1)))
      (List.take (n + 1) (edges (G := G) (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil n) (take Walk.nil n))
    (List.take n (edges (G := G) (u := u_1) Walk.nil))

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).edges = List.take n p.edges
n : ℕ
cons : edges (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) = List.take 0 (Walk.cons h p).edges
cons₁ :
  ∀ (n : ℕ),
    edges (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) =
      List.take (n + 1) (Walk.cons h p).edges
⊢ ((Walk.cons h p).take n).edges = List.take n (Walk.cons h p).edges

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0))
    (List.take 0 (edges (G := G) (u := u_1) nil))

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List (Sym2 V))
    (edges (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil (n + 1)) (take nil (n + 1)))
    (List.take (n + 1) (edges (G := G) (u := u_1) nil))

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).edges = List.take n p.edges
⊢ edges (v := (cons h p).getVert 0) ((cons h p).take 0) = List.take 0 (cons h p).edges

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.take n).edges = List.take n p.edges
n : ℕ
⊢ edges (v := (cons h p).getVert (n + 1)) ((cons h p).take (n + 1)) = List.take (n + 1) (cons h p).edges

Tactic:
simp [*, take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ (p.concat h).penultimate = v

Tactic:
simp [concat_eq_append, getVert_append]

Premises used: SimpleGraph.Walk.concat_eq_append, SimpleGraph.Walk.getVert_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.snd = p.penultimate

Tactic:
simpa using getVert_reverse p 1

Premises used: SimpleGraph.Walk.getVert_reverse, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Eq.{u + 1} (α := V) (penultimate (G := G) (u := u) (reverse Walk.nil)) (snd (G := G) (u := u) Walk.nil)
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).reverse.penultimate = (Walk.cons h p).snd
⊢ p.reverse.penultimate = p.snd

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := V) (penultimate (G := G) (u := u) (reverse nil)) (snd (G := G) (u := u) nil)

Tactic:
simp [snd, getVert_append]

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).reverse.penultimate = (cons h p).snd

Tactic:
simp [snd, getVert_append]

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : Eq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) Walk.nil 0) u) (drop Walk.nil 0) (Walk.copy Walk.nil ⋯ ⋯)
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).drop 0 = (Walk.cons h p).copy ⋯ ⋯
⊢ p.drop 0 = p.copy ⋯ ⋯

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) nil 0) u) (drop nil 0) (Walk.copy nil ⋯ ⋯)

Tactic:
simp [Walk.drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).drop 0 = (cons h p).copy ⋯ ⋯

Tactic:
simp [Walk.drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : p.length ≤ n
rw : (p.drop n).length = 0
rw₁ : p.length - n = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ (p.drop n).Nil

Tactic:
rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h]

Premises used: SimpleGraph.Walk.drop_length, Nat.sub_eq_zero_of_le, SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n))
      (List.drop (min n (length.{u} (V := V) (G := G) (u := u) Walk.nil)) (support (G := G) (u := u) Walk.nil))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support) →
      ∀ (n : ℕ), ((Walk.cons h p).drop n).support = List.drop (min n (Walk.cons h p).length) (Walk.cons h p).support
⊢ (p.drop n).support = List.drop (min n p.length) p.support

Tactic:
induction p generalizing n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0))
    (List.drop (min 0 (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)) (support (G := G) (u := u_1) Walk.nil))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := List V)
      (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)))
      (List.drop (min (n + 1) (length.{u} (V := V) (G := G) (u := u_1) Walk.nil))
        (support (G := G) (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n))
    (List.drop (min n (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)) (support (G := G) (u := u_1) Walk.nil))

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support
n : ℕ
cons :
  support (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) =
    List.drop (min 0 (Walk.cons h p).length) (Walk.cons h p).support
cons₁ :
  ∀ (n : ℕ),
    support (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) =
      List.drop (min (n + 1) (Walk.cons h p).length) (Walk.cons h p).support
⊢ ((Walk.cons h p).drop n).support = List.drop (min n (Walk.cons h p).length) (Walk.cons h p).support

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0))
    (List.drop (min 0 (length.{u} (V := V) (G := G) (u := u_1) nil)) (support (G := G) (u := u_1) nil))

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Eq.{u + 1} (α := List V) (support (G := G) (u := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)))
    (List.drop (min (n + 1) (length.{u} (V := V) (G := G) (u := u_1) nil)) (support (G := G) (u := u_1) nil))

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support
⊢ support (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop (min 0 (cons h p).length) (cons h p).support

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (n : ℕ), (p.drop n).support = List.drop (min n p.length) p.support
n : ℕ
⊢ support (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) =
    List.drop (min (n + 1) (cons h p).length) (cons h p).support

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ((p.take n).append (p.drop n)).support = p.support
⊢ (p.take n).append (p.drop n) = p

Tactic:
apply ext_support

Premises used: SimpleGraph.Walk.ext_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
⊢ ((p.take n).append (p.drop n)).support = p.support

Tactic:
rw [support_append, take_support_eq_support_take_succ, drop_support_eq_support_drop_min,
    List.tail_drop]

Premises used: List.tail_drop, SimpleGraph.Walk.support_append, SimpleGraph.Walk.drop_support_eq_support_drop_min, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
pos : ∀ (h : n < p.length), List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
neg : ∀ (h : p.length ≤ n), List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support

Tactic:
by_cases! h : n < p.length

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n < p.length
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support

Tactic:
simp [min_eq_left_of_lt h]

Premises used: min_eq_left_of_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
neg : List.take (n + 1) p.support ++ [] = p.support
⊢ List.take (n + 1) p.support ++ List.drop (min n p.length + 1) p.support = p.support

Tactic:
rw [Nat.min_eq_right h, ← length_support, List.drop_length]

Premises used: SimpleGraph.Walk.length_support, Nat.min_eq_right, List.drop_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : p.length ≤ n
⊢ List.take (n + 1) p.support ++ [] = p.support

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq.{u + 1} (α := G.Walk (snd (G := G) (u := v) nil) v) (tail nil) nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.drop, SimpleGraph.Walk.tail, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.drop, SimpleGraph.Walk.tail, rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
nil : (Walk.cons h Walk.nil).tail = Walk.copy Walk.nil ⋯ ⋯
cons :
  ∀ {v_1 : V} (h_1 : G.Adj v v_1) (p : G.Walk v_1 w), (Walk.cons h (Walk.cons h_1 p)).tail = (Walk.cons h_1 p).copy ⋯ ⋯
⊢ (Walk.cons h p).tail = p.copy ⋯ ⋯

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).tail = Walk.copy nil ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
v_1 : V
h_1 : G.Adj v v_1
p : G.Walk v_1 w
⊢ (cons h (cons h_1 p)).tail = (cons h_1 p).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ Eq.{u + 1} (α := G.Walk v (penultimate (G := G) (u := v) nil)) (dropLast nil) nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.take, SimpleGraph.Walk.dropLast, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ (cons h nil).dropLast = nil

Tactic:
rfl

Premises used: SimpleGraph.Walk.copy, SimpleGraph.Walk.take, SimpleGraph.Walk.dropLast, rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w w' : V
h : G.Adj u v
h₂ : G.Adj v w
p : G.Walk w w'
⊢ (cons h (cons h₂ p)).dropLast = cons h (cons h₂ p).dropLast

Tactic:
rfl

Premises used: SimpleGraph.Walk.take, SimpleGraph.Walk.dropLast, Nat.pred, rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).dropLast = cons x ((cons h q).dropLast.copy ⋯ ⋯)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u_1 v_1 w t u v : V
p : G.Walk u v
h : G.Adj v t
⊢ v = (p.concat h).penultimate

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v : V
p : G.Walk u v
h : G.Adj v t
nil : ∀ {u : V} (h : G.Adj u t), (concat Walk.nil h).dropLast = Walk.copy Walk.nil ⋯ ⋯
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯) →
      ∀ (h_1 : G.Adj w t), ((Walk.cons h p).concat h_1).dropLast = (Walk.cons h p).copy ⋯ ⋯
⊢ (p.concat h).dropLast = p.copy ⋯ ⋯

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 : V
h : G.Adj u_1 t
⊢ (concat nil h).dropLast = Walk.copy nil ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯
h : G.Adj w t
cons : Walk.cons h_1 ((p.concat h).dropLast.copy ⋯ ⋯) = (Walk.cons h_1 p).copy ⋯ ⋯
cons₁ : ¬(p.concat h).Nil
⊢ ((Walk.cons h_1 p).concat h).dropLast = (Walk.cons h_1 p).copy ⋯ ⋯

Tactic:
rw! [concat_cons, dropLast_cons_of_not_nil]

Premises used: SimpleGraph.Walk.dropLast_cons_of_not_nil, SimpleGraph.Walk.concat_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯
h : G.Adj w t
⊢ cons h_1 ((p.concat h).dropLast.copy ⋯ ⋯) = (cons h_1 p).copy ⋯ ⋯

Tactic:
simp [*, ← length_eq_zero_iff]

Premises used: SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
t u v u_1 v_1 w : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w
p_ih : ∀ (h : G.Adj w t), (p.concat h).dropLast = p.copy ⋯ ⋯
h : G.Adj w t
⊢ ¬(p.concat h).Nil

Tactic:
simp [*, ← length_eq_zero_iff]

Premises used: SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
nil : ∀ (hp : ¬Nil.{u} (V := V) (G := G) (v := u) Walk.nil), Walk.cons ⋯ (tail Walk.nil) = Walk.nil
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (hp : ¬(Walk.cons h p).Nil),
    Walk.cons ⋯ (Walk.cons h p).tail = Walk.cons h p
⊢ Walk.cons ⋯ p.tail = p

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
hp : ¬Nil.{u} (V := V) (G := G) (v := u) nil
⊢ cons ⋯ (tail nil) = nil

Tactic:
simp at hp ⊢
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
hp : ¬(cons h p).Nil
⊢ cons ⋯ (cons h p).tail = cons h p

Tactic:
simp at hp ⊢
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
hp : G.Adj (penultimate (G := G) (u := u_1) nil) u_1
⊢ concat (dropLast nil) hp = nil

Tactic:
simp at hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 : V
hadj : G.Adj u_1 v_1
hind : ∀ (hp : G.Adj (penultimate (G := G) (u := v_1) nil) v_1), concat (dropLast nil) hp = nil
hp : G.Adj (cons hadj nil).penultimate v_1
⊢ (cons hadj nil).dropLast.concat hp = cons hadj nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hadj : G.Adj u_1 v_1
v_2 : V
h : G.Adj v_1 v_2
p : G.Walk v_2 w
hind : ∀ (hp : G.Adj (cons h p).penultimate w), (cons h p).dropLast.concat hp = cons h p
hp : G.Adj (cons hadj (cons h p)).penultimate w
⊢ (cons hadj (cons h p)).dropLast.concat hp = cons hadj (cons h p)

Tactic:
simp [hind]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hadj : G.Adj u_1 v_1
p : G.Walk v_1 w
hind : ∀ (hp : G.Adj p.penultimate w), p.dropLast.concat hp = p
hp : G.Adj (Walk.cons hadj p).penultimate w
cons :
  ∀ (hind : ∀ (hp : G.Adj (penultimate (G := G) (u := v_1) nil) v_1), concat (dropLast nil) hp = nil)
    (hp : G.Adj (Walk.cons hadj nil).penultimate v_1), (Walk.cons hadj nil).dropLast.concat hp = Walk.cons hadj nil
cons₁ :
  ∀ {v : V} (h : G.Adj v_1 v) (p : G.Walk v w)
    (hind : ∀ (hp : G.Adj (Walk.cons h p).penultimate w), (Walk.cons h p).dropLast.concat hp = Walk.cons h p)
    (hp : G.Adj (Walk.cons hadj (Walk.cons h p)).penultimate w),
    (Walk.cons hadj (Walk.cons h p)).dropLast.concat hp = Walk.cons hadj (Walk.cons h p)
⊢ (Walk.cons hadj p).dropLast.concat hp = Walk.cons hadj p

Tactic:
cases p with
    | nil => rfl
    | _ => simp [hind]

Premises used: SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : G.Adj p.penultimate v
nil : ∀ {u : V} (hp : G.Adj (penultimate (G := G) (u := u) Walk.nil) u), concat (dropLast Walk.nil) hp = Walk.nil
cons :
  ∀ {u v w : V} (hadj : G.Adj u v) (p : G.Walk v w) (hind : ∀ (hp : G.Adj p.penultimate w), p.dropLast.concat hp = p)
    (hp : G.Adj (Walk.cons hadj p).penultimate w), (Walk.cons hadj p).dropLast.concat hp = Walk.cons hadj p
⊢ p.dropLast.concat hp = p

Tactic:
induction p with
  | nil => simp at hp
  | cons hadj p hind =>
    cases p with
    | nil => rfl
    | _ => simp [hind]

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
rw : (cons ⋯ p.tail).support = p.support
rw₁ rw₂ : p.support = p.support
⊢ u :: p.tail.support = p.support

Tactic:
rw [← support_cons (p.adj_snd hp), cons_tail_eq _ hp]

Premises used: SimpleGraph.Walk.support_cons, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.cons_tail_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
rw : (p.dropLast.concat ⋯).support = p.support
rw₁ rw₂ : p.support = p.support
⊢ p.dropLast.support ++ [v] = p.support

Tactic:
rw [← support_concat _ <| adj_penultimate hp, concat_dropLast]

Premises used: SimpleGraph.Walk.adj_penultimate, SimpleGraph.Walk.concat_dropLast, SimpleGraph.Walk.support_concat
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
⊢ p.dropLast.support = p.support.dropLast

Tactic:
simp [← support_dropLast_concat hp]

Premises used: SimpleGraph.Walk.support_dropLast_concat