awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
refine_1 : ∀ (h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support), s(u', v') ∈ p.edges
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges
have refine_2 : ∀ (h : s(u', v') ∈ p.edges), [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
⊢ s(u', v') ∈ p.edges
have this : G.Adj u' v'
Tactic: have := h.elim adj_of_infix_support (adj_of_infix_support · |>.symm)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : s(u', v') ∈ p.edges
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
have this : sorry.toWalk.IsSubwalk p ∨ sorry.toWalk.IsSubwalk p
Tactic: have := (isSubwalk_toWalk_iff_mem_edges <| p.adj_of_mem_edges h).mpr h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₁
⊢ p₁ = p₂
have h₃ : p₁.support <:+: p₂.support
Tactic: rw [isSubwalk_iff_support_isInfix] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.IsSubwalk p₂
h₂ : p₂.IsSubwalk p₁
h₃ : p₁.support <:+: p₂.support
⊢ p₁ = p₂
have h₄ : p₂.support <:+: p₁.support
Tactic: rw [isSubwalk_iff_support_isInfix] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
⊢ (p.take n).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
have succ : (p.take k).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
Tactic: apply ih.trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
⊢ (p.take k).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
have succ : ∀
  (ih :
    IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (v₁ := getVert (G := G) (u := u) nil n) (u₂ := u) (v₂ :=
      getVert (G := G) (u := u) nil k) (take nil n) (take nil k)),
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (v₁ := getVert (G := G) (u := u) nil k) (u₂ := u) (v₂ :=
    getVert (G := G) (u := u) nil (k + 1)) (take nil k) (take nil (k + 1))
Tactic: cases p
Cleared hypotheses: v, p, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.take n).IsSubwalk (p.take k)
succ :
  ∀
    (ih :
      IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (v₁ := getVert (G := G) (u := u) nil n) (u₂ := u) (v₂ :=
        getVert (G := G) (u := u) nil k) (take nil n) (take nil k)),
    IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (v₁ := getVert (G := G) (u := u) nil k) (u₂ := u) (v₂ :=
      getVert (G := G) (u := u) nil (k + 1)) (take nil k) (take nil (k + 1))
⊢ (p.take k).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
have succ₁ : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (ih : ((cons h p).take n).IsSubwalk ((cons h p).take k)),
  ((cons h p).take k).IsSubwalk (v₂ := (cons h p).getVert (k + 1)) ((cons h p).take (k + 1))
Tactic: cases p
Cleared hypotheses: p, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 k : ℕ
h : n ≤ k
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
ih : ((cons h_1 p).take n).IsSubwalk ((cons h_1 p).take k)
⊢ ((cons h_1 p).take k).IsSubwalk (v₂ := (cons h_1 p).getVert (k + 1)) ((cons h_1 p).take (k + 1))
have succ : ∀ (h : n ≤ 0) (ih : ((cons h_1 p).take n).IsSubwalk (v₂ := (cons h_1 p).getVert 0) ((cons h_1 p).take 0)),
  IsSubwalk (v₁ := (cons h_1 p).getVert 0) (v₂ := (cons h_1 p).getVert (HAdd.hAdd (α := ℕ) 0 1)) ((cons h_1 p).take 0)
    ((cons h_1 p).take (HAdd.hAdd (α := ℕ) 0 1))
Tactic: cases k
Cleared hypotheses: k, h, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 k : ℕ
h : n ≤ k
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
ih : ((cons h_1 p).take n).IsSubwalk ((cons h_1 p).take k)
succ :
  ∀ (h : n ≤ 0) (ih : ((cons h_1 p).take n).IsSubwalk (v₂ := (cons h_1 p).getVert 0) ((cons h_1 p).take 0)),
    IsSubwalk (v₁ := (cons h_1 p).getVert 0) (v₂ := (cons h_1 p).getVert (HAdd.hAdd (α := ℕ) 0 1)) ((cons h_1 p).take 0)
      ((cons h_1 p).take (HAdd.hAdd (α := ℕ) 0 1))
⊢ ((cons h_1 p).take k).IsSubwalk (v₂ := (cons h_1 p).getVert (k + 1)) ((cons h_1 p).take (k + 1))
have succ₁ : ∀ (n_1 : ℕ) (h : n ≤ n_1 + 1)
  (ih : ((cons h_1 p).take n).IsSubwalk (v₂ := (cons h_1 p).getVert (n_1 + 1)) ((cons h_1 p).take (n_1 + 1))),
  IsSubwalk (v₁ := (cons h_1 p).getVert (n_1 + 1)) (v₂ := (cons h_1 p).getVert (n_1 + 1 + 1))
    ((cons h_1 p).take (n_1 + 1)) ((cons h_1 p).take (n_1 + 1 + 1))
Tactic: cases k
Cleared hypotheses: k, h, ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
⊢ (p.take n).IsSubwalk (p.take k)
have base : (p.take n).IsSubwalk (p.take n)
Tactic: induction k, h using Nat.le_induction with
  | base => rfl
  | succ k h ih =>
    apply ih.trans
    cases p
    · exact isSubwalk_take _ _
    · cases k
      · exact isSubwalk_of_append_left rfl
      simp [isSubwalk_iff_support_isInfix, take_support_eq_support_take_succ, List.IsPrefix.isInfix]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
base : (p.take n).IsSubwalk (p.take n)
⊢ (p.take n).IsSubwalk (p.take k)
have succ : ∀ (k : ℕ) (h : n ≤ k) (ih : (p.take n).IsSubwalk (p.take k)),
  (p.take n).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
Tactic: induction k, h using Nat.le_induction with
  | base => rfl
  | succ k h ih =>
    apply ih.trans
    cases p
    · exact isSubwalk_take _ _
    · cases k
      · exact isSubwalk_of_append_left rfl
      simp [isSubwalk_iff_support_isInfix, take_support_eq_support_take_succ, List.IsPrefix.isInfix]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
h : n ≤ k
ih : (p.drop k).IsSubwalk (p.drop n)
⊢ IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop n)
have apply : IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop k)
Tactic: apply IsSubwalk.trans ?_ ih
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
n k n_1 : ℕ
ih : ∀ {u : V} (p : G.Walk u v), IsSubwalk (u₁ := p.getVert (n_1 + 1)) (p.drop (n_1 + 1)) (p.drop n_1)
u : V
p : G.Walk u v
⊢ IsSubwalk (u₁ := p.getVert (n_1 + 1 + 1)) (u₂ := p.getVert (n_1 + 1)) (p.drop (n_1 + 1 + 1)) (p.drop (n_1 + 1))
have succ : IsSubwalk.{u_1} (V := V) (G := G) (u₁ := getVert (G := G) (u := v) nil (n_1 + 1 + 1)) (u₂ :=
  getVert (G := G) (u := v) nil (n_1 + 1)) (drop nil (n_1 + 1 + 1)) (drop nil (n_1 + 1))
Tactic: cases p
Cleared hypotheses: u, p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
n k n_1 : ℕ
ih : ∀ {u : V} (p : G.Walk u v), IsSubwalk (u₁ := p.getVert (n_1 + 1)) (p.drop (n_1 + 1)) (p.drop n_1)
u : V
p : G.Walk u v
succ :
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := getVert (G := G) (u := v) nil (n_1 + 1 + 1)) (u₂ :=
    getVert (G := G) (u := v) nil (n_1 + 1)) (drop nil (n_1 + 1 + 1)) (drop nil (n_1 + 1))
⊢ IsSubwalk (u₁ := p.getVert (n_1 + 1 + 1)) (u₂ := p.getVert (n_1 + 1)) (p.drop (n_1 + 1 + 1)) (p.drop (n_1 + 1))
have succ₁ : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
  IsSubwalk (u₁ := (cons h p).getVert (n_1 + 1 + 1)) (u₂ := (cons h p).getVert (n_1 + 1))
    ((cons h p).drop (n_1 + 1 + 1)) ((cons h p).drop (n_1 + 1))
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
⊢ IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop k)
have zero : ∀ {u : V} (p : G.Walk u v),
  IsSubwalk (u₁ := p.getVert (HAdd.hAdd (α := ℕ) 0 1)) (u₂ := p.getVert 0) (p.drop (HAdd.hAdd (α := ℕ) 0 1)) (p.drop 0)
Tactic: induction k generalizing p u with
    | zero => exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
    | succ _ ih => cases p <;> simp [drop, ih]
Cleared hypotheses: u, p, k
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k_1 : ℕ
p : G.Walk u v
k : ℕ
zero :
  ∀ {u : V} (p : G.Walk u v),
    IsSubwalk (u₁ := p.getVert (HAdd.hAdd (α := ℕ) 0 1)) (u₂ := p.getVert 0) (p.drop (HAdd.hAdd (α := ℕ) 0 1))
      (p.drop 0)
⊢ IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop k)
have succ : ∀ (n : ℕ) (ih : ∀ {u : V} (p : G.Walk u v), IsSubwalk (u₁ := p.getVert (n + 1)) (p.drop (n + 1)) (p.drop n)) {u : V}
  (p : G.Walk u v),
  IsSubwalk (u₁ := p.getVert (n + 1 + 1)) (u₂ := p.getVert (n + 1)) (p.drop (n + 1 + 1)) (p.drop (n + 1))
Tactic: induction k generalizing p u with
    | zero => exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
    | succ _ ih => cases p <;> simp [drop, ih]
Cleared hypotheses: u, p, k
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
⊢ (p.drop k).IsSubwalk (p.drop n)
have base : (p.drop n).IsSubwalk (p.drop n)
Tactic: induction k, h using Nat.le_induction with
  | base => rfl
  | succ k h ih =>
    apply IsSubwalk.trans ?_ ih
    clear h ih
    induction k generalizing p u with
    | zero => exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
    | succ _ ih => cases p <;> simp [drop, ih]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
h : n ≤ k
base : (p.drop n).IsSubwalk (p.drop n)
⊢ (p.drop k).IsSubwalk (p.drop n)
have succ : ∀ (k : ℕ) (h : n ≤ k) (ih : (p.drop k).IsSubwalk (p.drop n)),
  IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop n)
Tactic: induction k, h using Nat.le_induction with
  | base => rfl
  | succ k h ih =>
    apply IsSubwalk.trans ?_ ih
    clear h ih
    induction k generalizing p u with
    | zero => exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
    | succ _ ih => cases p <;> simp [drop, ih]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert 0 = u
have nil : getVert (G := G) (u := u) nil 0 = u
Tactic: cases w
Cleared hypotheses: v, w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
nil : getVert (G := G) (u := u) Walk.nil 0 = u
⊢ w.getVert 0 = u
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (cons h p).getVert 0 = u
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (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
ih : ∀ {i : ℕ} (hi : p.length ≤ i), p.getVert i = w
i : ℕ
hi : (cons h p).length ≤ i
⊢ (cons h p).getVert i = w
have cons : ∀ (hi : (cons h p).length ≤ 0), (cons h p).getVert 0 = w
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (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
ih : ∀ {i : ℕ} (hi : p.length ≤ i), p.getVert i = w
i : ℕ
hi : (Walk.cons h p).length ≤ i
cons : ∀ (hi : (Walk.cons h p).length ≤ 0), (Walk.cons h p).getVert 0 = w
⊢ (Walk.cons h p).getVert i = w
have cons₁ : ∀ (n : ℕ) (hi : (Walk.cons h p).length ≤ n + 1), (Walk.cons h p).getVert (n + 1) = w
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : w.length ≤ i
⊢ w.getVert i = v
have nil : ∀ {u : V} {i : ℕ} (hi : length.{u} (V := V) (G := G) (u := u) nil ≤ i), getVert (G := G) (u := u) nil i = u
Tactic: induction w generalizing i with
  | nil => rfl
  | cons _ _ ih =>
    cases i
    · cases hi
    · exact ih (Nat.succ_le_succ_iff.1 hi)
Cleared hypotheses: w, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : w.length ≤ i
nil :
  ∀ {u : V} {i : ℕ} (hi : length.{u} (V := V) (G := G) (u := u) Walk.nil ≤ i), getVert (G := G) (u := u) Walk.nil i = u
⊢ w.getVert i = v
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (ih : ∀ {i : ℕ} (hi : p.length ≤ i), p.getVert i = w) {i : ℕ}
  (hi : (cons h p).length ≤ i), (cons h p).getVert i = w
Tactic: induction w generalizing i with
  | nil => rfl
  | cons _ _ ih =>
    cases i
    · cases hi
    · exact ih (Nat.succ_le_succ_iff.1 hi)
Cleared hypotheses: w, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < p.length), G.Adj (p.getVert i) (p.getVert (i + 1))
i : ℕ
hi : i < (cons hxy p).length
⊢ G.Adj ((cons hxy p).getVert i) ((cons hxy p).getVert (i + 1))
have cons : ∀ (hi : 0 < (cons hxy p).length), G.Adj ((cons hxy p).getVert 0) ((cons hxy p).getVert (HAdd.hAdd (α := ℕ) 0 1))
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 v_1 w : V
hxy : G.Adj u_1 v_1
p : G.Walk v_1 w
ih : ∀ {i : ℕ} (hi : i < p.length), G.Adj (p.getVert i) (p.getVert (i + 1))
i : ℕ
hi : i < (Walk.cons hxy p).length
cons :
  ∀ (hi : 0 < (Walk.cons hxy p).length),
    G.Adj ((Walk.cons hxy p).getVert 0) ((Walk.cons hxy p).getVert (HAdd.hAdd (α := ℕ) 0 1))
⊢ G.Adj ((Walk.cons hxy p).getVert i) ((Walk.cons hxy p).getVert (i + 1))
have cons₁ : ∀ (n : ℕ) (hi : n + 1 < (Walk.cons hxy p).length),
  G.Adj ((Walk.cons hxy p).getVert (n + 1)) ((Walk.cons hxy p).getVert (n + 1 + 1))
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
⊢ G.Adj (w.getVert i) (w.getVert (i + 1))
have nil : ∀ {u : V} {i : ℕ} (hi : i < length.{u} (V := V) (G := G) (u := u) nil),
  G.Adj (getVert (G := G) (u := u) nil i) (getVert (G := G) (u := u) nil (i + 1))
Tactic: induction w generalizing i with
  | nil => cases hi
  | cons hxy _ ih =>
    cases i
    · simp [getVert, hxy]
    · exact ih (Nat.succ_lt_succ_iff.1 hi)
Cleared hypotheses: w, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
i : ℕ
hi : i < w.length
nil :
  ∀ {u : V} {i : ℕ} (hi : i < length.{u} (V := V) (G := G) (u := u) Walk.nil),
    G.Adj (getVert (G := G) (u := u) Walk.nil i) (getVert (G := G) (u := u) Walk.nil (i + 1))
⊢ G.Adj (w.getVert i) (w.getVert (i + 1))
have cons : ∀ {u v w : V} (hxy : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ {i : ℕ} (hi : i < p.length), G.Adj (p.getVert i) (p.getVert (i + 1))) {i : ℕ} (hi : i < (cons hxy p).length),
  G.Adj ((cons hxy p).getVert i) ((cons hxy p).getVert (i + 1))
Tactic: induction w generalizing i with
  | nil => cases hi
  | cons hxy _ ih =>
    cases i
    · simp [getVert, hxy]
    · exact ih (Nat.succ_lt_succ_iff.1 hi)
Cleared hypotheses: w, i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
n : ℕ
p : G.Walk v w
h : G.Adj u v
hn : n ≠ 0
⊢ (cons h p).getVert n = p.getVert (n - 1)
have obtain : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)
have rw : p.getVert n = p.getVert (n + 1 - 1)
Tactic: rw [getVert_cons_succ, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
rw : p.getVert n = p.getVert (n + 1 - 1)
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)
have rw₁ : p.getVert n = p.getVert n
Tactic: rw [getVert_cons_succ, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.getVert i ∈ p.support
have nil : ∀ {u : V} (i : ℕ), Membership.mem (γ := List V) (support (G := G) (u := u) nil) (getVert (G := G) (u := u) nil i)
Tactic: induction p generalizing i
Cleared hypotheses: p, i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
nil :
  ∀ {u : V} (i : ℕ),
    Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) (getVert (G := G) (u := u) Walk.nil i)
⊢ p.getVert i ∈ p.support
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (∀ (i : ℕ), p.getVert i ∈ p.support) → ∀ (i : ℕ), (cons h p).getVert i ∈ (cons h p).support
Tactic: induction p generalizing i
Cleared hypotheses: p, i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
i : ℕ
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) (getVert (G := G) (u := u_1) nil i)
have nil : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) (getVert (G := G) (u := u_1) nil 0)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
i : ℕ
nil : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) (getVert (G := G) (u := u_1) Walk.nil 0)
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) (getVert (G := G) (u := u_1) Walk.nil i)
have nil₁ : ∀ (n : ℕ),
  Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) (getVert (G := G) (u := u_1) Walk.nil (n + 1))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (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 : ∀ (i : ℕ), p.getVert i ∈ p.support
i : ℕ
⊢ (cons h p).getVert i ∈ (cons h p).support
have cons : (cons h p).getVert 0 ∈ (cons h p).support
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (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 : ∀ (i : ℕ), p.getVert i ∈ p.support
i : ℕ
cons : (Walk.cons h p).getVert 0 ∈ (Walk.cons h p).support
⊢ (Walk.cons h p).getVert i ∈ (Walk.cons h p).support
have cons₁ : ∀ (n : ℕ), (Walk.cons h p).getVert (n + 1) ∈ (Walk.cons h p).support
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
n : ℕ
h : n + 1 ≤ (cons h_1 p).length
⊢ (cons h_1 p).getVert (n + 1) =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h_1 p).support (n + 1) ⋯
have cons : p.getVert (n + 1 - 1) =
  if h : n + 1 = 0 then u else getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (n + 1 - 1) sorry
Tactic: simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
h : n ≤ (cons h_1 p).length
⊢ (cons h_1 p).getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h_1 p).support n ⋯
have cons : ∀ (h : 0 ≤ (cons h_1 p).length),
  (cons h_1 p).getVert 0 = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h_1 p).support 0 sorry
Tactic: cases n with
    | zero => simp
    | succ n =>
      simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
h : n ≤ (Walk.cons h_1 p).length
cons :
  ∀ (h : 0 ≤ (Walk.cons h_1 p).length),
    (Walk.cons h_1 p).getVert 0 =
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h_1 p).support 0 ⋯
⊢ (Walk.cons h_1 p).getVert n =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h_1 p).support n ⋯
have cons₁ : ∀ (n : ℕ) (h : n + 1 ≤ (Walk.cons h_1 p).length),
  (Walk.cons h_1 p).getVert (n + 1) =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h_1 p).support (n + 1) sorry
Tactic: cases n with
    | zero => simp
    | succ n =>
      simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
⊢ p.getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n ⋯
have nil : ∀ (h : n ≤ length.{u} (V := V) (G := G) (u := u) nil),
  getVert (G := G) (u := u) nil n =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) nil) n sorry
Tactic: cases p with
  | nil => simp
  | cons => cases n with
    | zero => simp
    | succ n =>
      simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)
Cleared hypotheses: v, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Traversal (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
nil :
  ∀ (h : n ≤ length.{u} (V := V) (G := G) (u := u) Walk.nil),
    getVert (G := G) (u := u) Walk.nil n =
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) Walk.nil) n ⋯
⊢ p.getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n ⋯
have cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : n ≤ (cons h p).length),
  (cons h p).getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h p).support n sorry
Tactic: cases p with
  | nil => simp
  | cons => cases n with
    | zero => simp
    | succ n =>
      simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)
Cleared hypotheses: p, h