awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v_1 v v_2 : V
h : G.Adj u v_2
p : G.Walk v_2 v
⊢ { fst := u, snd := v_2, adj := h : G.Dart }.toProd.2 = v_2

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h' : G.Adj u v_1
p' : G.Walk v_1 v
e : Sym2 V
h : e ∈ (cons h' p').edges
head : { fst := u, snd := v_1, adj := h' : G.Dart }.edge ∈ G.edgeSet
tail : List.Mem e (List.map Dart.edge p'.darts) → e ∈ G.edgeSet
⊢ e ∈ G.edgeSet

Tactic:
cases h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h' : G.Adj u v_1
p' : G.Walk v_1 v
⊢ { fst := u, snd := v_1, adj := h' : G.Dart }.edge ∈ G.edgeSet

Tactic:
h'

Premises used: Set.Mem, setOf, Sym2.fromRel
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h' : G.Adj u v_1
p' : G.Walk v_1 v
⊢ { fst := u, snd := v_1, adj := h' : G.Dart }.edge ∈ G.edgeSet

Tactic:
exact h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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
e : Sym2 V
h' : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Tactic:
edges_subset_edgeSet p' h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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
e : Sym2 V
h' : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Tactic:
exact edges_subset_edgeSet p' h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v x y : V
p : G.Walk u v
h : s(x, y) ∈ p.edges
⊢ G.Adj x y

Tactic:
p.edges_subset_edgeSet h

Premises used: Set.Mem, setOf, Sym2.fromRel, SimpleGraph.Walk.edges_subset_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := List G.Dart) (darts (u := u) nil) []

Tactic:
rfl

Premises used: SimpleGraph.Walk.darts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).darts = { fst := u, snd := v, adj := h } :: p.darts

Tactic:
rfl

Premises used: SimpleGraph.Walk.darts, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (darts (u := u) Walk.nil) = support (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    v :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support →
      u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (Walk.cons h p).darts = (Walk.cons h p).support
⊢ u :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ u_1 :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (darts (u := u_1) nil) = support (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : v_1 :: List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support
⊢ u_1 :: List.map (fun (x : G.Dart) ↦ x.toProd.2) (cons h p).darts = (cons h p).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.2) p.darts = p.support.tail

Tactic:
simpa using congr_arg List.tail (cons_map_snd_darts p)

Premises used: List.tail, congr_arg, SimpleGraph.Walk.cons_map_snd_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    List.map (fun (x : G.Dart) ↦ x.toProd.1) (darts (u := u) Walk.nil) ++ [u] = support (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [w] = p.support →
      List.map (fun (x : G.Dart) ↦ x.toProd.1) (Walk.cons h p).darts ++ [w] = (Walk.cons h p).support
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [v] = p.support

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) (darts (u := u_1) nil) ++ [u_1] = support (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts ++ [w] = p.support
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) (cons h p).darts ++ [w] = (cons h p).support

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun (x : G.Dart) ↦ x.toProd.1) p.darts = p.support.dropLast

Tactic:
simpa! using congr_arg List.dropLast (map_fst_darts_append p)

Premises used: List.dropLast, SimpleGraph.Walk.map_fst_darts_append, congr_arg
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ Eq.{u + 1} (α := List (Sym2 V)) (edges (G := G) (u := u) nil) []

Tactic:
rfl

Premises used: List.map, rfl, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).edges = s(u, v) :: p.edges

Tactic:
rfl

Premises used: List.map, SimpleGraph.Dart.edge, rfl, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    List.length.{u} (α := V) (support (G := G) (u := u) Walk.nil) = length.{u} (V := V) (G := G) (u := u) Walk.nil + 1
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.support.length = p.length + 1 → (Walk.cons h p).support.length = (Walk.cons h p).length + 1
⊢ p.support.length = p.length + 1

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ List.length.{u} (α := V) (support (G := G) (u := u_1) nil) = length.{u} (V := V) (G := G) (u := u_1) nil + 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : p.support.length = p.length + 1
⊢ (cons h p).support.length = (cons h p).length + 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V}, List.length.{u} (α := G.Dart) (darts (u := u) Walk.nil) = length.{u} (V := V) (G := G) (u := u) Walk.nil
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    p.darts.length = p.length → (Walk.cons h p).darts.length = (Walk.cons h p).length
⊢ p.darts.length = p.length

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ List.length.{u} (α := G.Dart) (darts (u := u_1) nil) = length.{u} (V := V) (G := G) (u := u_1) nil

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : p.darts.length = p.length
⊢ (cons h p).darts.length = (cons h p).length

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.edges.length = p.length

Tactic:
simp [edges]

Premises used: SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
i : ℕ
hi : i < p.darts.length
⊢ i < p.support.dropLast.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
hi : i < p.darts.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi).toProd.1 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support.dropLast i ⋯

Tactic:
grind [map_fst_darts]

Premises used: SimpleGraph.Walk.map_fst_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
i : ℕ
hi : i < p.darts.length
⊢ i < p.support.tail.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
hi : i < p.darts.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi).toProd.2 =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support.tail i ⋯

Tactic:
grind [map_snd_darts]

Premises used: SimpleGraph.Walk.map_snd_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) Walk.nil) 0 ⋯ = u
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h p).support 0 ⋯ = u
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support 0 ⋯ = u

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u : V
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) nil) 0 ⋯ = u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h p).support 0 ⋯ = u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
nil :
  ∀ {u : V},
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u) Walk.nil)
        (length.{u} (V := V) (G := G) (u := u) Walk.nil) ⋯ =
      u
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length ⋯ = w →
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (Walk.cons h p).support (Walk.cons h p).length ⋯ = w
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length ⋯ = v

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u_1 : V
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (support (G := G) (u := u_1) nil)
      (length.{u} (V := V) (G := G) (u := u_1) nil) ⋯ =
    u_1

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
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 : getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support p.length ⋯ = w
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (cons h p).support (cons h p).length ⋯ = w

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ↔ [u', v'] <:+: p.support

Tactic:
.trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm

Premises used: Iff.intro, Iff.trans, List.infix_iff_getElem?, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
refine_1 :
  ∀ (h : { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts),
    ∃ (k : ℕ),
      [u', v'].length + k ≤ p.support.length ∧
        ∀ (i : ℕ) (h : i < [u', v'].length),
          getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
            some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
refine_2 :
  (∃ (k : ℕ),
      [u', v'].length + k ≤ p.support.length ∧
        ∀ (i : ℕ) (h : i < [u', v'].length),
          getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
            some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)) →
    ∀ (i : ℕ) (hi : [u', v'].length + i ≤ p.support.length)
      (h_1 :
        ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
          getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
            some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)),
      { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts
⊢ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ↔ [u', v'] <:+: p.support

Tactic:
refine .trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h : { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
refine_1 :
  ∀ (i : ℕ) (hi : i < p.darts.length)
    (h :
      getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi =
        { fst := u', snd := v', adj := h_1 }),
    ∃ (k : ℕ),
      [u', v'].length + k ≤ p.support.length ∧
        ∀ (i : ℕ) (h : i < [u', v'].length),
          getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
            some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
⊢ ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)

Tactic:
have ⟨i, hi, h⟩ := List.getElem_of_mem h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
i : ℕ
hi : i < p.darts.length
h :
  getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi = { fst := u', snd := v', adj := h_1 }
⊢ [u', v'].length + i ≤ p.support.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
i : ℕ
hi : i < p.darts.length
h :
  getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi = { fst := u', snd := v', adj := h_1 }
j : ℕ
hj : j < [u', v'].length
⊢ getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (j + i) =
    some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] j hj)

Tactic:
grind [fst_darts_getElem, snd_darts_getElem]

Premises used: SimpleGraph.Walk.snd_darts_getElem, SimpleGraph.Walk.fst_darts_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
i : ℕ
hi : i < p.darts.length
h :
  getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i hi = { fst := u', snd := v', adj := h_1 }
⊢ ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)

Tactic:
exact ⟨i, by grind, fun j hj ↦ by grind [fst_darts_getElem, snd_darts_getElem]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
⊢ ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)

Tactic:
have := h 0
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
⊢ ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)

Tactic:
have := h 1
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
⊢ i < p.darts.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
h₁ : u' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i ⋯).1.1
h₂ : v' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i ⋯).1.2
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts

Tactic:
convert! p.darts.getElem_mem (n := i) (by grind)

Premises used: List.getElem_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
⊢ u' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i ⋯).1.1

Tactic:
grind [fst_darts_getElem, snd_darts_getElem]

Premises used: SimpleGraph.Walk.snd_darts_getElem, SimpleGraph.Walk.fst_darts_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 :
  ∃ (k : ℕ),
    [u', v'].length + k ≤ p.support.length ∧
      ∀ (i : ℕ) (h : i < [u', v'].length),
        getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i + k) =
          some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i h)
i : ℕ
hi : [u', v'].length + i ≤ p.support.length
h :
  ∀ (i_1 : ℕ) (h : i_1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (i_1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] i_1 h)
this_1 :
  ∀ (h : 0 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (0 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 0 h)
this :
  ∀ (h : 1 < [u', v'].length),
    getElem? (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p.support (1 + i) =
      some (getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) [u', v'] 1 h)
⊢ v' = (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p.darts i ⋯).1.2

Tactic:
grind [fst_darts_getElem, snd_darts_getElem]

Premises used: SimpleGraph.Walk.snd_darts_getElem, SimpleGraph.Walk.fst_darts_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
⊢ d ∈ p.darts ↔ [d.toProd.1, d.toProd.2] <:+: p.support

Tactic:
mem_darts_iff_infix_support ..

Premises used: SimpleGraph.Walk.mem_darts_iff_infix_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d ∈ (cons h p').darts
simp : ∀ (hd : d = { fst := u, snd := v_1, adj := h } ∨ d ∈ p'.darts), d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
⊢ d.toProd.1 ∈ (cons h p').support

Tactic:
simp only [support_cons, darts_cons, List.mem_cons] at hd ⊢

Premises used: SimpleGraph.Walk.support_cons, SimpleGraph.Walk.darts_cons, List.mem_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic
Goal:
V : Type u
G : SimpleGraph V
u v v_1 : V
h : G.Adj u v_1
p' : G.Walk v_1 v
d : G.Dart
hd : d = { fst := u, snd := v_1, adj := h } ∨ d ∈ p'.darts
inl :
  { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 = u ∨
    { fst := u, snd := v_1, adj := h : G.Dart }.toProd.1 ∈ p'.support
inr : ∀ (hd : d ∈ p'.darts), d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
⊢ d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support

Tactic:
rcases hd with rfl | hd

Premises used: rfl