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

Tactic:
cases m
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
m n : ℕ
nil :
  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)) 0)
    (getVert (G := G) (u := u_1) Walk.nil (min (n + 1) 0))
nil₁ :
  ∀ (n_1 : ℕ),
    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))
        (n_1 + 1))
      (getVert (G := G) (u := u_1) Walk.nil (min (n + 1) (n_1 + 1)))
⊢ 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))

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

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

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

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} (α := V) (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0) (n + 1))
    (getVert (G := G) (u := u_1) nil (min 0 (n + 1)))

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} (α := V) (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil (n + 1)) (take nil (n + 1)) 0)
    (getVert (G := G) (u := u_1) nil (min (n + 1) 0))

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 n_1 : ℕ
⊢ Eq.{u + 1} (α := V)
    (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil (n + 1)) (take nil (n + 1)) (n_1 + 1))
    (getVert (G := G) (u := u_1) nil (min (n + 1) (n_1 + 1)))

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

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

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

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

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 : ℕ
rw : HEq (α := G.Walk u (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
⊢ HEq (α := G.Walk u (p.getVert (n + m))) (p.take (n + m)) ((p.take n).append ((p.drop n).take 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 u (getVert (G := G) (u := u) Walk.nil (m + n))) (take Walk.nil (m + n)) (β :=
      G.Walk u (getVert (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) m))
      (append (take Walk.nil n) (take (drop Walk.nil n) m))
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (n : ℕ), HEq (α := G.Walk v (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))) →
      ∀ (n : ℕ),
        HEq (α := G.Walk u ((Walk.cons h p).getVert (m + n))) ((Walk.cons h p).take (m + n))
          (((Walk.cons h p).take n).append (((Walk.cons h p).drop n).take m))
⊢ HEq (α := G.Walk u (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take 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 u_1 (getVert (G := G) (u := u_1) Walk.nil (m + 0))) (take Walk.nil (m + 0)) (β :=
    G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0) m))
    (append (take Walk.nil 0) (take (drop Walk.nil 0) m))
nil₁ :
  ∀ (n : ℕ),
    HEq.{u + 1} (α := G.Walk u_1 (getVert (G := G) (u := u_1) Walk.nil (m + (n + 1)))) (take Walk.nil (m + (n + 1)))
      (β := G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)) m))
      (append (take Walk.nil (n + 1)) (take (drop Walk.nil (n + 1)) m))
⊢ HEq.{u + 1} (α := G.Walk u_1 (getVert (G := G) (u := u_1) Walk.nil (m + n))) (take Walk.nil (m + n)) (β :=
    G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n) m))
    (append (take Walk.nil n) (take (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 v_1 (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
n : ℕ
cons :
  HEq (α := G.Walk u_1 ((Walk.cons h p).getVert (m + 0))) ((Walk.cons h p).take (m + 0)) (β :=
    G.Walk u_1 (getVert (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) m))
    (append ((Walk.cons h p).take 0) (take ((Walk.cons h p).drop 0) m))
cons₁ :
  ∀ (n : ℕ),
    HEq (α := G.Walk u_1 ((Walk.cons h p).getVert (m + (n + 1)))) ((Walk.cons h p).take (m + (n + 1))) (β :=
      G.Walk u_1 (getVert (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) m))
      (append ((Walk.cons h p).take (n + 1)) (take ((Walk.cons h p).drop (n + 1)) m))
⊢ HEq (α := G.Walk u_1 ((Walk.cons h p).getVert (m + n))) ((Walk.cons h p).take (m + n))
    (((Walk.cons h p).take n).append (((Walk.cons h p).drop n).take 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 u_1 (getVert (G := G) (u := u_1) nil (m + 0))) (take nil (m + 0)) (β :=
    G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0) m))
    (append (take nil 0) (take (drop nil 0) m))

Tactic:
simp [take, drop]

Premises used: SimpleGraph.Walk.take, 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 u_1 (getVert (G := G) (u := u_1) nil (m + (n + 1)))) (take nil (m + (n + 1))) (β :=
    G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) nil (n + 1)) (drop nil (n + 1)) m))
    (append (take nil (n + 1)) (take (drop nil (n + 1)) m))

Tactic:
simp [take, drop]

Premises used: SimpleGraph.Walk.take, 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 v_1 (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
⊢ HEq (α := G.Walk u_1 ((cons h p).getVert (m + 0))) ((cons h p).take (m + 0)) (β :=
    G.Walk u_1 (getVert (u := (cons h p).getVert 0) ((cons h p).drop 0) m))
    (append ((cons h p).take 0) (take ((cons h p).drop 0) m))

Tactic:
simp [take, drop]

Premises used: SimpleGraph.Walk.take, 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 v_1 (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
n : ℕ
cons :
  HEq (α := G.Walk u_1 ((Walk.cons h p).getVert (m + (n + 1)))) (Walk.cons h (p.take (m + n)))
    (Walk.cons h ((p.take n).append ((p.drop n).take m)))
⊢ HEq (α := G.Walk u_1 ((Walk.cons h p).getVert (m + (n + 1)))) ((Walk.cons h p).take (m + (n + 1))) (β :=
    G.Walk u_1 (getVert (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) m))
    (append ((Walk.cons h p).take (n + 1)) (take ((Walk.cons h p).drop (n + 1)) m))

Tactic:
simp [take, drop]

Premises used: SimpleGraph.Walk.take, 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 v_1 (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
n : ℕ
⊢ HEq (α := G.Walk u_1 ((cons h p).getVert (m + (n + 1)))) (cons h (p.take (m + n)))
    (cons h ((p.take n).append ((p.drop n).take m)))

Tactic:
grind [drop_getVert]

Premises used: SimpleGraph.Walk.drop_getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.take n).append ((p.drop n).take m) ≍ ((p.take n).append ((p.drop n).take 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 :
  Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n) ↔
    Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∨ n = 0
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), ((Walk.cons h p).take n).Nil ↔ (Walk.cons h p).Nil ∨ n = 0
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
nil :
  Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) Walk.nil 0) (take Walk.nil 0) ↔
    Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∨ Eq (α := ℕ) 0 0
nil₁ :
  ∀ (n : ℕ),
    Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) Walk.nil (n + 1)) (take Walk.nil (n + 1)) ↔
      Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∨ n + 1 = 0
⊢ Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) Walk.nil n) (take Walk.nil n) ↔
    Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∨ n = 0

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

Tactic:
cases n
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) nil 0) (take nil 0) ↔
    Nil.{u} (V := V) (G := G) (v := u) nil ∨ Eq (α := ℕ) 0 0

Tactic:
simp [take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) nil (n + 1)) (take nil (n + 1)) ↔
    Nil.{u} (V := V) (G := G) (v := u) nil ∨ n + 1 = 0

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
⊢ Nil (w := (cons h p).getVert 0) ((cons h p).take 0) ↔ (cons h p).Nil ∨ Eq (α := ℕ) 0 0

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
n : ℕ
⊢ Nil (w := (cons h p).getVert (n + 1)) ((cons h p).take (n + 1)) ↔ (cons h p).Nil ∨ n + 1 = 0

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

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

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 : ℕ
h : ((p.take n).take m).support = (Walk.copy (p.take (min n m)) ⋯ ⋯).support
⊢ (p.take n).take m = Walk.copy (p.take (min n m)) ⋯ ⋯

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 m : ℕ
⊢ ((p.take n).take m).support = (Walk.copy (p.take (min n m)) ⋯ ⋯).support

Tactic:
simp [take_support_eq_support_take_succ, List.take_take, Nat.min_left_comm]

Premises used: List.take_take, Nat.min_left_comm, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v u : V
p : G.Walk u v
h : p.length ≤ 0
zero : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ 0), take nil 0 = Walk.copy nil ⋯ ⋯
zero₁ :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (cons h p).length ≤ 0),
    (cons h p).take 0 = (cons h p).copy ⋯ ⋯
⊢ p.take 0 = p.copy ⋯ ⋯

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
h : length.{u} (V := V) (G := G) (u := v) nil ≤ 0
⊢ take nil 0 = Walk.copy nil ⋯ ⋯

Tactic:
simp [take] at h ⊢

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

Tactic:
simp [take] at h ⊢

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u : V
p : G.Walk u v
h : p.length ≤ n + 1
succ : ∀ (h : length.{u} (V := V) (G := G) (u := v) nil ≤ n + 1), take nil (n + 1) = Walk.copy nil ⋯ ⋯
succ₁ :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : (cons h p).length ≤ n + 1),
    (cons h p).take (n + 1) = (cons h p).copy ⋯ ⋯
⊢ p.take (n + 1) = p.copy ⋯ ⋯

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
h : length.{u} (V := V) (G := G) (u := v) nil ≤ n + 1
⊢ take nil (n + 1) = Walk.copy nil ⋯ ⋯

Tactic:
simp [take]

Premises used: SimpleGraph.Walk.take
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
h : (cons h_1 p).length ≤ n + 1
⊢ p.length ≤ n

Tactic:
rw [length_cons, Nat.add_le_add_iff_right] at h

Premises used: Nat.add_le_add_iff_right, SimpleGraph.Walk.length_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations
Goal:
V : Type u
G : SimpleGraph V
v : V
n : ℕ
ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯
u v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
h_2 : (cons h_1 p).length ≤ n + 1
h : p.length ≤ n
⊢ (cons h_1 p).take (n + 1) = (cons h_1 p).copy ⋯ ⋯

Tactic:
simp [take, ih h]

Premises used: SimpleGraph.Walk.take
-- 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
zero : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ 0), p.take 0 = p.copy ⋯ ⋯
succ :
  ∀ (n : ℕ) (ih : ∀ {u : V} {p : G.Walk u v} (h : p.length ≤ n), p.take n = p.copy ⋯ ⋯) {u : V} {p : G.Walk u v}
    (h : p.length ≤ n + 1), p.take (n + 1) = p.copy ⋯ ⋯
⊢ p.take n = p.copy ⋯ ⋯

Tactic:
induction n generalizing p u with
  | zero => cases p <;> simp [take] at h ⊢
  | succ n ih =>
    cases p
    · simp [take]
    rw [length_cons, Nat.add_le_add_iff_right] at h
    simp [take, ih h]

Premises used: Nat.add_le_add_iff_right, SimpleGraph.Walk.take, SimpleGraph.Walk.length_cons
-- 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).take n).support = (cons h (Walk.copy (p.take (n - 1)) ⋯ ⋯)).support
⊢ (cons h p).take n = cons h (Walk.copy (p.take (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
⊢ ((cons h p).take n).support = (cons h (Walk.copy (p.take (n - 1)) ⋯ ⋯)).support

Tactic:
grind [support_copy, take_support_eq_support_take_succ]

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

Tactic:
induction p generalizing n