awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u w : V
q : G.Walk u w
nil :
  Nil.{u} (V := V) (G := G) (v := u) (append Walk.nil Walk.nil) ↔
    Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ Nil.{u} (V := V) (G := G) (v := u) Walk.nil
⊢ (append Walk.nil q).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ q.Nil
have nil₁ : ∀ {v : V} (h : G.Adj u v) (p : G.Walk v w),
  (append Walk.nil (cons h p)).Nil ↔ Nil.{u} (V := V) (G := G) (v := u) Walk.nil ∧ (cons h p).Nil
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ ((cons h p).append q).Nil ↔ (cons h p).Nil ∧ q.Nil
have cons : ((cons h p).append nil).Nil ↔ (cons h p).Nil ∧ Nil.{u} (V := V) (G := G) (v := v) nil
Tactic: cases q
Cleared hypotheses: w, q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
cons : ((Walk.cons h p).append nil).Nil ↔ (Walk.cons h p).Nil ∧ Nil.{u} (V := V) (G := G) (v := v) nil
⊢ ((Walk.cons h p).append q).Nil ↔ (Walk.cons h p).Nil ∧ q.Nil
have cons₁ : ∀ {v_2 : V} (h_1 : G.Adj v v_2) (p_1 : G.Walk v_2 w),
  ((Walk.cons h p).append (Walk.cons h_1 p_1)).Nil ↔ (Walk.cons h p).Nil ∧ (Walk.cons h_1 p_1).Nil
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
⊢ p.reverse.Nil ↔ p.Nil
have nil : Nil.{u} (V := V) (G := G) (v := v) (reverse nil) ↔ Nil.{u} (V := V) (G := G) (v := v) nil
Tactic: cases p
Cleared hypotheses: w, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
nil : Nil.{u} (V := V) (G := G) (v := v) (reverse Walk.nil) ↔ Nil.{u} (V := V) (G := G) (v := v) Walk.nil
⊢ p.reverse.Nil ↔ p.Nil
have cons : ∀ {v_1 : V} (h : G.Adj v v_1) (p : G.Walk v_1 w), (cons h p).reverse.Nil ↔ (cons h p).Nil
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ (p.drop n).length = p.length - n
have nil : ∀ {u : V} (n : ℕ),
  length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n) =
    length.{u} (V := V) (G := G) (u := u) nil - n
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) =
      length.{u} (V := V) (G := G) (u := u) Walk.nil - n
⊢ (p.drop n).length = p.length - n
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.drop n).length = p.length - n) → ∀ (n : ℕ), ((cons h p).drop n).length = (cons h p).length - n
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) nil n) (drop nil n) =
    length.{u} (V := V) (G := G) (u := u_1) nil - n
have nil : length.{u} (V := V) (G := G) (u := getVert (G := G) (u := u_1) nil 0) (drop nil 0) =
  length.{u} (V := V) (G := G) (u := u_1) nil - 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
nil :
  length.{u} (V := V) (G := G) (u := 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
⊢ length.{u} (V := V) (G := G) (u := 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
have nil₁ : ∀ (n : ℕ),
  length.{u} (V := V) (G := G) (u := 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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).length = p.length - n
n : ℕ
⊢ ((cons h p).drop n).length = (cons h p).length - n
have cons : length (u := (cons h p).getVert 0) ((cons h p).drop 0) = (cons h p).length - 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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).length = p.length - n
n : ℕ
cons : length (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) = (Walk.cons h p).length - 0
⊢ ((Walk.cons h p).drop n).length = (Walk.cons h p).length - n
have cons₁ : ∀ (n : ℕ),
  length (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) = (Walk.cons h p).length - (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ (p.drop n).getVert m = p.getVert (n + m)
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n) m)
    (getVert (G := G) (u := u) nil (n + m))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
nil :
  ∀ {u : V} (n : ℕ),
    Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u) Walk.nil n) (drop Walk.nil n) m)
      (getVert (G := G) (u := u) Walk.nil (n + m))
⊢ (p.drop n).getVert m = p.getVert (n + m)
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.drop n).getVert m = p.getVert (n + m)) →
    ∀ (n : ℕ), ((cons h p).drop n).getVert m = (cons h p).getVert (n + m)
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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) (drop nil n) m)
    (getVert (G := G) (u := u_1) nil (n + m))
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u_1 : V
n : ℕ
nil :
  Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil 0) (drop Walk.nil 0) m)
    (getVert (G := G) (u := u_1) Walk.nil (0 + m))
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil n) (drop Walk.nil n) m)
    (getVert (G := G) (u := u_1) Walk.nil (n + m))
have nil₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := V) (getVert (G := G) (u := getVert (G := G) (u := u_1) Walk.nil (n + 1)) (drop Walk.nil (n + 1)) m)
    (getVert (G := G) (u := u_1) Walk.nil (n + 1 + m))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 : ℕ
⊢ ((cons h p).drop n).getVert m = (cons h p).getVert (n + m)
have cons : getVert (u := (cons h p).getVert 0) ((cons h p).drop 0) m = (cons h p).getVert (0 + m)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 : ℕ
cons : getVert (u := (Walk.cons h p).getVert 0) ((Walk.cons h p).drop 0) m = (Walk.cons h p).getVert (0 + m)
⊢ ((Walk.cons h p).drop n).getVert m = (Walk.cons h p).getVert (n + m)
have cons₁ : ∀ (n : ℕ),
  getVert (u := (Walk.cons h p).getVert (n + 1)) ((Walk.cons h p).drop (n + 1)) m = (Walk.cons h p).getVert (n + 1 + m)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ HEq (α := G.Walk (p.getVert (n + m)) v) (p.drop (n + m)) ((p.drop n).drop m)
have rw : HEq (α := G.Walk (p.getVert (m + n)) v) (p.drop (m + n)) ((p.drop n).drop m)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n m : ℕ
⊢ HEq (α := G.Walk (p.getVert (m + n)) v) (p.drop (m + n)) ((p.drop n).drop m)
have nil : ∀ {u : V} (n : ℕ),
  HEq.{u + 1} (α := G.Walk (getVert (G := G) (u := u) nil (m + n)) u) (drop nil (m + n)) (β :=
    G.Walk (getVert (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n) m) u) (drop (drop nil n) m)
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ HEq (α := G.Walk (p.getVert (m + n)) v) (p.drop (m + n)) ((p.drop n).drop m)
have 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 ((cons h p).getVert (m + n)) w) ((cons h p).drop (m + n)) (((cons h p).drop n).drop m)
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)) u_1) (drop nil (m + n)) (β :=
    G.Walk (getVert (G := G) (u := getVert (G := G) (u := u_1) nil n) (drop nil n) m) u_1) (drop (drop nil n) m)
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ 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)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)) w) ((cons h p).drop (m + n)) (((cons h p).drop n).drop m)
have cons : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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)
⊢ 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)
have 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)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ (p.drop n).Nil ↔ p.length ≤ n
have nil : ∀ {u : V} (n : ℕ),
  Nil.{u} (V := V) (G := G) (v := getVert (G := G) (u := u) nil n) (drop nil n) ↔
    length.{u} (V := V) (G := G) (u := u) nil ≤ n
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ (p.drop n).Nil ↔ p.length ≤ n
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (n : ℕ), (p.drop n).Nil ↔ p.length ≤ n) → ∀ (n : ℕ), ((cons h p).drop n).Nil ↔ (cons h p).length ≤ n
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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) (drop nil n) ↔
    length.{u} (V := V) (G := G) (u := u_1) nil ≤ n
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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.{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
have 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
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 h p).drop n).Nil ↔ (cons h p).length ≤ n
have cons : Nil (v := (cons h p).getVert 0) ((cons h p).drop 0) ↔ (cons h p).length ≤ 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ ((Walk.cons h p).drop n).Nil ↔ (Walk.cons h p).length ≤ n
have 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
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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).drop n = Walk.copy (p.drop (n - 1)) ⋯ ⋯
have h₁ : ((cons h p).drop n).support = (Walk.copy (p.drop (n - 1)) sorry sorry).support
Tactic: apply ext_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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).drop n).support = (Walk.copy (p.drop (n - 1)) ⋯ ⋯).support
have 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)) sorry sorry).support
Tactic: obtain ⟨_, rfl⟩ := Nat.exists_add_one_eq.mpr (Nat.ne_zero_iff_zero_lt.mp hn)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
| support (u := (cons h p).getVert (w_1 + 1)) ((cons h p).drop (w_1 + 1))
have unfold : (p.drop w_1).support
Tactic: unfold drop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ 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
have h₁ : (p.drop w_1).support = (Walk.copy (p.drop (w_1 + 1 - 1)) sorry sorry).support
Tactic: conv_lhs => unfold drop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ (p.drop n).darts = List.drop n p.darts
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List G.Dart) (darts (u := getVert (G := G) (u := u) nil n) (drop nil n))
    (List.drop n (darts (u := u) nil))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ (p.drop n).darts = List.drop n p.darts
have 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 : ℕ), ((cons h p).drop n).darts = List.drop n (cons h p).darts
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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) (drop nil n))
    (List.drop n (darts (u := u_1) nil))
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ 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))
have 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))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 h p).drop n).darts = List.drop n (cons h p).darts
have cons : darts (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop 0 (cons h p).darts
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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
⊢ ((Walk.cons h p).drop n).darts = List.drop n (Walk.cons h p).darts
have 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
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ (p.drop n).edges = List.drop n p.edges
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n))
    (List.drop n (edges (G := G) (u := u) nil))
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ (p.drop n).edges = List.drop n p.edges
have 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 : ℕ), ((cons h p).drop n).edges = List.drop n (cons h p).edges
Tactic: induction p generalizing n
Cleared hypotheses: p, n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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) (drop nil n))
    (List.drop n (edges (G := G) (u := u_1) nil))
have nil : 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: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ 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))
have 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))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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 h p).drop n).edges = List.drop n (cons h p).edges
have cons : edges (u := (cons h p).getVert 0) ((cons h p).drop 0) = List.drop 0 (cons h p).edges
Tactic: cases n
Cleared hypotheses: n