awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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))
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))
⊢ ((cons h_1 p).take k).IsSubwalk (v₂ := (cons h_1 p).getVert (k + 1)) ((cons h_1 p).take (k + 1))

Tactic:
cases k
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
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:
isSubwalk_of_append_left rfl

Premises used: SimpleGraph.Walk.isSubwalk_of_append_left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
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:
exact isSubwalk_of_append_left rfl

Premises used: SimpleGraph.Walk.isSubwalk_of_append_left, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v_1 : V
h_1 : G.Adj u v_1
p : G.Walk v_1 v
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:
simp [isSubwalk_iff_support_isInfix, take_support_eq_support_take_succ, List.IsPrefix.isInfix]

Premises used: List.IsPrefix.isInfix, SimpleGraph.Walk.isSubwalk_iff_support_isInfix, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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)
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))
⊢ (p.take n).IsSubwalk (p.take k)

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]

Premises used: SimpleGraph.Walk.isSubwalk_take, List.IsPrefix.isInfix, SimpleGraph.Walk.isSubwalk_of_append_left, SimpleGraph.Walk.isSubwalk_iff_support_isInfix, rfl, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
p : G.Walk u v
⊢ (p.drop n).IsSubwalk (p.drop n)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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)
apply : IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop k)
⊢ IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop n)

Tactic:
apply IsSubwalk.trans ?_ ih

Premises used: SimpleGraph.Walk.IsSubwalk.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v : V
n k : ℕ
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:
p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail

Premises used: SimpleGraph.Walk.drop_zero, SimpleGraph.Walk.IsSubwalk.copy, SimpleGraph.Walk.getVert_zero, Eq.rec, SimpleGraph.Walk.isSubwalk_rfl, Eq.symm, SimpleGraph.Walk.IsSubwalk.tail, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v : V
n k : ℕ
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:
exact p.drop_zero ▸ (p.isSubwalk_rfl.copy rfl rfl p.getVert_zero.symm rfl).tail
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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))
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))
⊢ 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))

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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)
⊢ 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:
simp [drop, ih]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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_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:
simp [drop, ih]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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)
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))
⊢ IsSubwalk (u₁ := p.getVert (k + 1)) (p.drop (k + 1)) (p.drop k)

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]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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)
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)
⊢ (p.drop k).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]

Premises used: SimpleGraph.Walk.drop
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).getVert 0 = u
⊢ w.getVert 0 = u

Tactic:
cases w
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ getVert (G := G) (u := u) nil 0 = u

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).getVert 0 = u

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
⊢ getVert (G := G) (u := u) nil i = u

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
i : ℕ
hi : length.{u} (V := V) (G := G) (u := u_1) nil ≤ i
⊢ getVert (G := G) (u := u_1) nil i = u_1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
cons₁ : ∀ (n : ℕ) (hi : (Walk.cons h p).length ≤ n + 1), (Walk.cons h p).getVert (n + 1) = w
⊢ (Walk.cons h p).getVert i = w

Tactic:
cases i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
hi : (cons h p).length ≤ 0
⊢ (cons h p).getVert 0 = w

Tactic:
cases hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
n : ℕ
hi : (cons h p).length ≤ n + 1
⊢ (cons h p).getVert (n + 1) = w

Tactic:
ih (Nat.succ_le_succ_iff.1 hi)

Premises used: Nat.succ_le_succ_iff, Iff.mp, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
n : ℕ
hi : (cons h p).length ≤ n + 1
⊢ (cons h p).getVert (n + 1) = w

Tactic:
exact ih (Nat.succ_le_succ_iff.1 hi)

Premises used: Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
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 : (Walk.cons h p).length ≤ i), (Walk.cons h p).getVert i = w
⊢ w.getVert i = v

Tactic:
induction w generalizing i with
  | nil => rfl
  | cons _ _ ih =>
    cases i
    · cases hi
    · exact ih (Nat.succ_le_succ_iff.1 hi)

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert w.length = v

Tactic:
w.getVert_of_length_le rfl.le

Premises used: SimpleGraph.Walk.getVert_of_length_le, Eq.le, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
i : ℕ
hi : i < length.{u} (V := V) (G := G) (u := u_1) nil
⊢ G.Adj (getVert (G := G) (u := u_1) nil i) (getVert (G := G) (u := u_1) nil (i + 1))

Tactic:
cases hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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))
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))
⊢ G.Adj ((Walk.cons hxy p).getVert i) ((Walk.cons hxy p).getVert (i + 1))

Tactic:
cases i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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))
hi : 0 < (cons hxy p).length
⊢ G.Adj ((cons hxy p).getVert 0) ((cons hxy p).getVert (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp [getVert, hxy]

Premises used: SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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))
n : ℕ
hi : n + 1 < (cons hxy p).length
⊢ G.Adj ((cons hxy p).getVert (n + 1)) ((cons hxy p).getVert (n + 1 + 1))

Tactic:
ih (Nat.succ_lt_succ_iff.1 hi)

Premises used: Nat.succ_lt_succ_iff, Iff.mp, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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))
n : ℕ
hi : n + 1 < (cons hxy p).length
⊢ G.Adj ((cons hxy p).getVert (n + 1)) ((cons hxy p).getVert (n + 1 + 1))

Tactic:
exact ih (Nat.succ_lt_succ_iff.1 hi)

Premises used: Nat.succ_lt_succ_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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))
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 < (Walk.cons hxy p).length), G.Adj ((Walk.cons hxy p).getVert i) ((Walk.cons hxy p).getVert (i + 1))
⊢ G.Adj (w.getVert i) (w.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)

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v w : V
n : ℕ
p : G.Walk v w
h : G.Adj u v
⊢ (cons h p).getVert (n + 1) = p.getVert n

Tactic:
rfl

Premises used: rfl, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
obtain : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)
⊢ (cons h p).getVert n = p.getVert (n - 1)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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)
rw₁ rw₂ : p.getVert n = p.getVert n
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)

Tactic:
rw [getVert_cons_succ, Nat.add_sub_cancel]

Premises used: SimpleGraph.Walk.getVert_cons_succ, Nat.add_sub_cancel
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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)
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    (∀ (i : ℕ), p.getVert i ∈ p.support) → ∀ (i : ℕ), (Walk.cons h p).getVert i ∈ (Walk.cons h p).support
⊢ p.getVert i ∈ p.support

Tactic:
induction p generalizing i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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)
nil₁ :
  ∀ (n : ℕ),
    Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) (getVert (G := G) (u := u_1) Walk.nil (n + 1))
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) (getVert (G := G) (u := u_1) Walk.nil i)

Tactic:
cases i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
cons₁ : ∀ (n : ℕ), (Walk.cons h p).getVert (n + 1) ∈ (Walk.cons h p).support
⊢ (Walk.cons h p).getVert i ∈ (Walk.cons h p).support

Tactic:
cases i
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) (getVert (G := G) (u := u_1) nil 0)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
n : ℕ
⊢ Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) (getVert (G := G) (u := u_1) nil (n + 1))

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
⊢ (cons h p).getVert 0 ∈ (cons h p).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
n : ℕ
⊢ (cons h p).getVert (n + 1) ∈ (cons h p).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u : V
n : ℕ
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 ⋯

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
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 ⋯

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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 ≤ (Walk.cons h_1 p).length
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) ⋯
⊢ (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) ⋯

Tactic:
simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]

Premises used: SimpleGraph.Walk.getVert_cons, SimpleGraph.Walk.support_cons, List.getElem_cons, Ne.symm, Nat.zero_ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
⊢ 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) ⋯

Tactic:
getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)

Premises used: dite, Nat.sub_le_of_le_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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
⊢ 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) ⋯

Tactic:
exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)

Premises used: Nat.sub_le_of_le_add
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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 ⋯
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) ⋯
⊢ (Walk.cons h_1 p).getVert n =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h_1 p).support n ⋯

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)

Premises used: SimpleGraph.Walk.getVert_cons, SimpleGraph.Walk.support_cons, List.getElem_cons, Ne.symm, Nat.sub_le_of_le_add, Nat.zero_ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
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 ⋯
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v) (h_1 : n ≤ (Walk.cons h p).length),
    (Walk.cons h p).getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h p).support n ⋯
⊢ p.getVert n = getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n ⋯

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)

Premises used: SimpleGraph.Walk.getVert_cons, SimpleGraph.Walk.support_cons, List.getElem_cons, Ne.symm, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, Nat.sub_le_of_le_add, Nat.zero_ne_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n < p.support.length
⊢ n ≤ p.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
h : n ≤ p.length
rw :
  some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n ⋯) =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
rw₁ rw₂ :
  getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n =
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n
⊢ some (p.getVert n) = getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support n

Tactic:
rw [getVert_eq_support_getElem p h, ← List.getElem?_eq_getElem]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem, List.getElem?_eq_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
pos : ∀ (h : n ≤ p.length), p.getVert n = p.support.getD n v
neg : ∀ (h : ¬n ≤ p.length), p.getVert n = p.support.getD n v
⊢ p.getVert n = p.support.getD n v

Tactic:
by_cases h : n ≤ p.length

Premises used: SimpleGraph.Walk.length
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : n ≤ p.length
⊢ p.getVert n = p.support.getD n v

Tactic:
simp [← getVert_eq_support_getElem? p h]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem?
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
h : ¬n ≤ p.length
⊢ p.getVert n = p.support.getD n v

Tactic:
grind [getVert_of_length_le, length_support]

Premises used: SimpleGraph.Walk.length_support, SimpleGraph.Walk.getVert_of_length_le