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 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
⊢ ((Walk.cons h p).drop n).edges = List.drop n (Walk.cons h p).edges
have 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
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
⊢ p.take 0 = Walk.copy nil ⋯ ⋯
have nil : Eq.{u + 1} (α := G.Walk u (getVert (G := G) (u := u) nil 0)) (take nil 0) (Walk.copy nil sorry sorry)
Tactic: cases p
Cleared hypotheses: v, 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
nil : Eq.{u + 1} (α := G.Walk u (getVert (G := G) (u := u) Walk.nil 0)) (take Walk.nil 0) (Walk.copy Walk.nil ⋯ ⋯)
⊢ p.take 0 = Walk.copy Walk.nil ⋯ ⋯
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).take 0 = Walk.copy Walk.nil sorry sorry
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.take n).length = min n p.length
have nil : ∀ {u : V} (n : ℕ),
  length.{u} (V := V) (G := G) (u := u) (v := getVert (G := G) (u := u) nil n) (take nil n) =
    min n (length.{u} (V := V) (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 : ℕ),
    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)
⊢ (p.take n).length = min n p.length
have 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 : ℕ), ((cons h p).take n).length = min n (cons h p).length
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 := u_1) (v := getVert (G := G) (u := u_1) nil n) (take nil n) =
    min n (length.{u} (V := V) (G := G) (u := u_1) nil)
have nil : 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: 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 := 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)
⊢ 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)
have 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)
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.take n).length = min n p.length
n : ℕ
⊢ ((cons h p).take n).length = min n (cons h p).length
have cons : length (v := (cons h p).getVert 0) ((cons h p).take 0) = min 0 (cons h p).length
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.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
⊢ ((Walk.cons h p).take n).length = min n (Walk.cons h p).length
have 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
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.take n).getVert m = p.getVert (min n m)
have nil : ∀ {u : V} (n m : ℕ),
  Eq.{u + 1} (α := V) (getVert (G := G) (u := u) (v := getVert (G := G) (u := u) nil n) (take nil n) m)
    (getVert (G := G) (u := u) nil (min n m))
Tactic: induction p generalizing n m
Cleared hypotheses: p, n, m
-- 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 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))
⊢ (p.take n).getVert m = p.getVert (min n m)
have 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 : ℕ), ((cons h p).take n).getVert m = (cons h p).getVert (min n m)
Tactic: induction p generalizing n m
Cleared hypotheses: p, n, m
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n m : ℕ
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil n) (take nil n) m)
    (getVert (G := G) (u := u_1) nil (min n m))
have nil : Eq.{u + 1} (α := V) (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0) m)
  (getVert (G := G) (u := u_1) nil (min 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 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))
⊢ 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))
have 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))
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 m : ℕ), (p.take n).getVert m = p.getVert (min n m)
n m : ℕ
⊢ ((cons h p).take n).getVert m = (cons h p).getVert (min n m)
have cons : getVert (v := (cons h p).getVert 0) ((cons h p).take 0) m = (cons h p).getVert (min 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 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)
⊢ ((Walk.cons h p).take n).getVert m = (Walk.cons h p).getVert (min n m)
have 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)
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
m : ℕ
⊢ Eq.{u + 1} (α := V) (getVert (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil 0) (take nil 0) m)
    (getVert (G := G) (u := u_1) nil (min 0 m))
have nil : 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: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ 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))
have 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)))
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
m 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)) m)
    (getVert (G := G) (u := u_1) nil (min (n + 1) m))
have nil : 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: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Operations (goal)
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))
⊢ 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))
have 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)))
Tactic: cases m
Cleared hypotheses: m
-- 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 m : ℕ), (p.take n).getVert m = p.getVert (min n m)
m : ℕ
⊢ getVert (v := (cons h p).getVert 0) ((cons h p).take 0) m = (cons h p).getVert (min 0 m)
have cons : getVert (v := (cons h p).getVert 0) ((cons h p).take 0) 0 = (cons h p).getVert (min 0 0)
Tactic: cases m
Cleared hypotheses: m
-- 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 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)
⊢ getVert (v := (Walk.cons h p).getVert 0) ((Walk.cons h p).take 0) m = (Walk.cons h p).getVert (min 0 m)
have 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))
Tactic: cases m
Cleared hypotheses: m
-- 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 m : ℕ), (p.take n).getVert m = p.getVert (min n m)
m n : ℕ
⊢ getVert (v := (cons h p).getVert (n + 1)) ((cons h p).take (n + 1)) m = (cons h p).getVert (min (n + 1) m)
have cons : getVert (v := (cons h p).getVert (n + 1)) ((cons h p).take (n + 1)) 0 = (cons h p).getVert (min (n + 1) 0)
Tactic: cases m
Cleared hypotheses: m
-- 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 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)
⊢ 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)
have 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))
Tactic: cases m
Cleared hypotheses: m
-- 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 u (p.getVert (n + m))) (p.take (n + m)) ((p.take n).append ((p.drop n).take m))
have rw : HEq (α := G.Walk u (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take 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 u (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
have nil : ∀ {u : V} (n : ℕ),
  HEq.{u + 1} (α := G.Walk u (getVert (G := G) (u := u) nil (m + n))) (take nil (m + n)) (β :=
    G.Walk u (getVert (G := G) (u := getVert (G := G) (u := u) nil n) (drop nil n) m))
    (append (take nil n) (take (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 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))
⊢ HEq (α := G.Walk u (p.getVert (m + n))) (p.take (m + n)) ((p.take n).append ((p.drop n).take m))
have 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 ((cons h p).getVert (m + n))) ((cons h p).take (m + n))
        (((cons h p).take n).append (((cons h p).drop n).take 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 u_1 (getVert (G := G) (u := u_1) nil (m + n))) (take nil (m + n)) (β :=
    G.Walk u_1 (getVert (G := G) (u := getVert (G := G) (u := u_1) nil n) (drop nil n) m))
    (append (take nil n) (take (drop nil n) m))
have nil : 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: 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 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))
⊢ 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))
have 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))
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 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))) ((cons h p).take (m + n))
    (((cons h p).take n).append (((cons h p).drop n).take m))
have cons : 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: 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 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))
⊢ 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))
have 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))
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 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 + 1))) (β :=
    G.Walk u_1 (getVert (u := (cons h p).getVert (n + 1)) ((cons h p).drop (n + 1)) m))
    (append ((cons h p).take (n + 1)) (take ((cons h p).drop (n + 1)) m))
have cons : 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: simp [take, 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.take n).Nil ↔ p.Nil ∨ n = 0
have nil : Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) nil n) (take nil n) ↔
  Nil.{u} (V := V) (G := G) (v := u) nil ∨ n = 0
Tactic: cases p
Cleared hypotheses: v, 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 : ℕ
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
⊢ (p.take n).Nil ↔ p.Nil ∨ n = 0
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), ((cons h p).take n).Nil ↔ (cons h p).Nil ∨ n = 0
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
n : ℕ
⊢ Nil.{u} (V := V) (G := G) (v := u) (w := getVert (G := G) (u := u) nil n) (take nil n) ↔
    Nil.{u} (V := V) (G := G) (v := u) nil ∨ n = 0
have nil : 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: 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
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.{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
have 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
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
n : ℕ
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ ((cons h p).take n).Nil ↔ (cons h p).Nil ∨ n = 0
have cons : Nil (w := (cons h p).getVert 0) ((cons h p).take 0) ↔ (cons h p).Nil ∨ Eq (α := ℕ) 0 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 : 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
⊢ ((Walk.cons h p).take n).Nil ↔ (Walk.cons h p).Nil ∨ n = 0
have 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
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.take n).support = List.take (n + 1) p.support
have nil : ∀ {u : V} (n : ℕ),
  Eq.{u + 1} (α := List V) (support (G := G) (u := u) (v := getVert (G := G) (u := u) nil n) (take nil n))
    (List.take (n + 1) (support (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 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))
⊢ (p.take n).support = List.take (n + 1) p.support
have 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 : ℕ), ((cons h p).take n).support = List.take (n + 1) (cons h p).support
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 V) (support (G := G) (u := u_1) (v := getVert (G := G) (u := u_1) nil n) (take nil n))
    (List.take (n + 1) (support (G := G) (u := u_1) nil))
have nil : 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: 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 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))
⊢ 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))
have 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))
Tactic: cases n
Cleared hypotheses: n