awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u_1 : V
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0) m)
    (getVert (G := G) (u := u_1) nil (0 + m))

Tactic:
simp [*, drop, add_right_comm]

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

Tactic:
simp [*, drop, add_right_comm]

Premises used: add_right_comm, SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
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).getVert m = p.getVert (n + m)
⊢ getVert (u := (cons h p).getVert 0) ((cons h p).drop 0) m = (cons h p).getVert (0 + m)

Tactic:
simp [*, drop, add_right_comm]

Premises used: add_right_comm, SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
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).getVert m = p.getVert (n + m)
n : ℕ
⊢ getVert (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) m = (cons h p).getVert (n + 1 + m)

Tactic:
simp [*, drop, add_right_comm]

Premises used: add_right_comm, 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 m : ℕ
rw : HEq (α := G.Walk (p.getVert (m + n)) v) (p.drop (m + n)) ((p.drop n).drop m)
⊢ HEq (α := G.Walk (p.getVert (n + m)) v) (p.drop (n + m)) ((p.drop n).drop m)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    HEq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) Walk.nil (m + n)) u) (drop Walk.nil (m + n)) (β :=
      G.Walk (getVert (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) m) u)
      (drop (drop Walk.nil n) m)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), HEq (α := G.Walk (p.getVert (m + n)) w) (p.drop (m + n)) ((p.drop n).drop m)) →
      ∀ (n : ℕ),
        HEq (α := G.Walk ((Walk.cons h p).getVert (m + n)) w) ((Walk.cons h p).drop (m + n))
          (((Walk.cons h p).drop n).drop m)
⊢ HEq (α := G.Walk (p.getVert (m + n)) v) (p.drop (m + n)) ((p.drop n).drop m)

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

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

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u_1 : V
⊢ HEq.{u + 1} (α := G.Walk (getVert (G := G) (u := u_1) nil (m + 0)) u_1) (drop nil (m + 0)) (β :=
    G.Walk (getVert (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0) m) u_1) (drop (drop nil 0) m)

Tactic:
simp [*, drop]

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

Tactic:
simp [*, drop]

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

Tactic:
simp [*, drop]

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

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 m : ℕ
⊢ (p.drop n).drop m ≍ ((p.drop n).drop m).copy ⋯ ⋯

Tactic:
simp [Walk.copy]

Premises used: SimpleGraph.Walk.copy
-- 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 : ℕ),
    Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) ↔
      length.{u} (V := V) (G := G) (u := u) Walk.nil ≤ n
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.drop n).Nil ↔ p.length ≤ n) → ∀ (n : ℕ), ((Walk.cons h p).drop n).Nil ↔ (Walk.cons h p).length ≤ n
⊢ (p.drop n).Nil ↔ p.length ≤ n

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 :
  Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0) ↔
    length.{u} (V := V) (G := G) (u := u_1) Walk.nil ≤ 0
nil₁ :
  ∀ (n : ℕ),
    Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)) ↔
      length.{u} (V := V) (G := G) (u := u_1) Walk.nil ≤ n + 1
⊢ Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n) ↔
    length.{u} (V := V) (G := G) (u := u_1) Walk.nil ≤ n

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).Nil ↔ p.length ≤ n
n : ℕ
cons : Nil (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) ↔ (Walk.cons h p).length ≤ 0
cons₁ :
  ∀ (n : ℕ), Nil (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) ↔ (Walk.cons h p).length ≤ n + 1
⊢ ((Walk.cons h p).drop n).Nil ↔ (Walk.cons h p).length ≤ n

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u_1) nil 0) (drop nil 0) ↔
    length.{u} (V := V) (G := G) (u := u_1) nil ≤ 0

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 : ℕ
⊢ Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)) ↔
    length.{u} (V := V) (G := G) (u := u_1) nil ≤ n + 1

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).Nil ↔ p.length ≤ n
⊢ Nil (v := (cons h p).getVert 0) ((cons h p).drop 0) ↔ (cons h p).length ≤ 0

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).Nil ↔ p.length ≤ n
n : ℕ
⊢ Nil (v := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) ↔ (cons h p).length ≤ n + 1

Tactic:
simp [*, drop]

Premises used: SimpleGraph.Walk.drop
-- 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
n : ℕ
hn : n ≠ 0
h₁ : ((cons h p).drop n).support = (Walk.copy (p.drop (n - 1)) ⋯ ⋯).support
⊢ (cons h p).drop n = Walk.copy (p.drop (n - 1)) ⋯ ⋯

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 w : V
h : G.Adj u v
p : G.Walk v w
n : ℕ
hn : n ≠ 0
h₁ :
  ∀ (w_1 : ℕ) (hn : w_1 + 1 ≠ 0),
    support (u := (cons h p).getVert (w_1 + 1)) ((cons h p).drop (w_1 + 1)) =
      (Walk.copy (p.drop (w_1 + 1 - 1)) ⋯ ⋯).support
⊢ ((cons h p).drop n).support = (Walk.copy (p.drop (n - 1)) ⋯ ⋯).support

Tactic:
obtain ⟨_, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.ne_zero_iff_zero_lt.mp hn)

Premises used: Iff.mpr, Nat.ne_zero_iff_zero_lt, Nat.exists_add_one_eq, Iff.mp, rfl
-- 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
w_1 : ℕ
hn : w_1 + 1 ≠ 0
unfold : (p.drop w_1).support
| support (u := (cons h p).getVert (w_1 + 1)) ((cons h p).drop (w_1 + 1))

Tactic:
unfold drop

Premises used: SimpleGraph.Walk.drop
-- 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
w_1 : ℕ
hn : w_1 + 1 ≠ 0
h₁ : (p.drop w_1).support = (Walk.copy (p.drop (w_1 + 1 - 1)) ⋯ ⋯).support
⊢ support (u := (cons h p).getVert (w_1 + 1)) ((cons h p).drop (w_1 + 1)) =
    (Walk.copy (p.drop (w_1 + 1 - 1)) ⋯ ⋯).support

Tactic:
conv_lhs => unfold drop

Premises used: SimpleGraph.Walk.drop
-- 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
w_1 : ℕ
hn : w_1 + 1 ≠ 0
⊢ (p.drop w_1).support = (Walk.copy (p.drop (w_1 + 1 - 1)) ⋯ ⋯).support

Tactic:
simp
-- 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 G.Dart) (darts (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n))
      (List.drop n (darts (u := u) Walk.nil))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), (p.drop n).darts = List.drop n p.darts) →
      ∀ (n : ℕ), ((Walk.cons h p).drop n).darts = List.drop n (Walk.cons h p).darts
⊢ (p.drop n).darts = List.drop n p.darts

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 G.Dart) (darts (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0))
    (List.drop 0 (darts (u := u_1) Walk.nil))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := List G.Dart) (darts (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)))
      (List.drop (n + 1) (darts (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n))
    (List.drop 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.drop n).darts = List.drop n p.darts
n : ℕ
cons : darts (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) = List.drop 0 (Walk.cons h p).darts
cons₁ :
  ∀ (n : ℕ),
    darts (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) =
      List.drop (n + 1) (Walk.cons h p).darts
⊢ ((Walk.cons h p).drop n).darts = List.drop 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 := getVert (G := G) (u := u_1) nil 0) (drop nil 0))
    (List.drop 0 (darts (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 G.Dart) (darts (u := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)))
    (List.drop (n + 1) (darts (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).darts = List.drop n p.darts
⊢ darts (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop 0 (cons h p).darts

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).darts = List.drop n p.darts
n : ℕ
⊢ darts (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) = List.drop (n + 1) (cons h p).darts

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 : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n))
      (List.drop 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.drop n).edges = List.drop n p.edges) →
      ∀ (n : ℕ), ((Walk.cons h p).drop n).edges = List.drop n (Walk.cons h p).edges
⊢ (p.drop n).edges = List.drop 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 := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0))
    (List.drop 0 (edges (G := G) (u := u_1) Walk.nil))
nil₁ :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := List (Sym2 V))
      (edges (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)))
      (List.drop (n + 1) (edges (G := G) (u := u_1) Walk.nil))
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n))
    (List.drop 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.drop n).edges = List.drop n p.edges
n : ℕ
cons : edges (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) = List.drop 0 (Walk.cons h p).edges
cons₁ :
  ∀ (n : ℕ),
    edges (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) =
      List.drop (n + 1) (Walk.cons h p).edges
⊢ ((Walk.cons h p).drop n).edges = List.drop 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 := getVert (G := G) (u := u_1) nil 0) (drop nil 0))
    (List.drop 0 (edges (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 (Sym2 V)) (edges (G := G) (u := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)))
    (List.drop (n + 1) (edges (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).edges = List.drop n p.edges
⊢ edges (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop 0 (cons h p).edges

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).edges = List.drop n p.edges
n : ℕ
⊢ edges (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) = List.drop (n + 1) (cons h p).edges

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
nil : Eq.{u + 1} (α := G.Walk u (getVert (G := G) (u := u) Walk.nil 0)) (take 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).take 0 = Walk.copy Walk.nil ⋯ ⋯
⊢ p.take 0 = Walk.copy Walk.nil ⋯ ⋯

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

Tactic:
simp [take]

Premises used: SimpleGraph.Walk.take
-- 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).take 0 = Walk.copy nil ⋯ ⋯

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 : ℕ),
    length.{u} (V := V) (G := G) (u := u) (v := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n) =
      min n (length.{u} (V := V) (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).length = min n p.length) →
      ∀ (n : ℕ), ((Walk.cons h p).take n).length = min n (Walk.cons h p).length
⊢ (p.take n).length = min n p.length

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 :
  length.{u} (V := V) (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil 0) (take Walk.nil 0) =
    min 0 (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)
nil₁ :
  ∀ (n : ℕ),
    length.{u} (V := V) (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil (n + 1))
        (take Walk.nil (n + 1)) =
      min (n + 1) (length.{u} (V := V) (G := G) (u := u_1) Walk.nil)
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) Walk.nil n) (take Walk.nil n) =
    min n (length.{u} (V := V) (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).length = min n p.length
n : ℕ
cons : length (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) = min 0 (Walk.cons h p).length
cons₁ :
  ∀ (n : ℕ),
    length (v := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).take (n + 1)) = min (n + 1) (Walk.cons h p).length
⊢ ((Walk.cons h p).take n).length = min n (Walk.cons h p).length

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0) =
    min 0 (length.{u} (V := V) (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 : ℕ
⊢ length.{u} (V := V) (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil (n + 1)) (take nil (n + 1)) =
    min (n + 1) (length.{u} (V := V) (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).length = min n p.length
⊢ length (v := (cons h p).getVert 0) ((cons h p).take 0) = min 0 (cons h p).length

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

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 m : ℕ
nil :
  ∀ {u : V} (n m : ℕ),
    Eq.{u + 1} (α := V) (getVert (G := G) (u := u) (v := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n) m)
      (getVert (G := G) (u := u) Walk.nil (min n m))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n m : ℕ), (p.take n).getVert m = p.getVert (min n m)) →
      ∀ (n m : ℕ), ((Walk.cons h p).take n).getVert m = (Walk.cons h p).getVert (min n m)
⊢ (p.take n).getVert m = p.getVert (min n m)

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

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

Tactic:
cases n