awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' : V
p : G.Walk u v
nil :
  IsSubwalk.{u_1} (V := V) (G := G) (u₁ := u) (u₂ := u') Walk.nil Walk.nil ↔
    ∃ (hu : u' = u) (hv : u' = u), Eq (α := G.Walk u u) Walk.nil (Walk.copy Walk.nil hu hv)
cons :
  ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v),
    (Walk.cons h p).IsSubwalk (u₂ := u') Walk.nil ↔
      ∃ (hu : u' = u) (hv : u' = v), Walk.cons h p = Walk.copy Walk.nil hu hv
⊢ p.IsSubwalk (u₂ := u') Walk.nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = Walk.copy Walk.nil hu hv

Tactic:
cases p with
  | nil =>
    constructor
    · rintro ⟨_ | _, _, ⟨⟩⟩
      simp
    · rintro ⟨rfl, _, _⟩
      simp
  | cons h p =>
    constructor
    · rintro ⟨_ | _, _, h⟩ <;> simp at h
    · rintro ⟨rfl, rfl, ⟨⟩⟩

Premises used: SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u' u v : V
q : G.Walk u v
⊢ IsSubwalk (u₁ := u') nil q ↔ ∃ (ru : G.Walk u u') (rv : G.Walk u' v), q = ru.append rv

Tactic:
simp [IsSubwalk]

Premises used: SimpleGraph.Walk.IsSubwalk
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ : V
q : G.Walk u₁ v₁
p : G.Walk u₂ v₂
h : p.IsSubwalk q
⊢ p.length ≤ q.length

Tactic:
grind [IsSubwalk, length_append]

Premises used: SimpleGraph.Walk.IsSubwalk, SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w u : V
p₁ : G.Walk v w
p₂ : G.Walk w u
p₃ : G.Walk v u
h : p₃ = p₁.append p₂
⊢ p₁.IsSubwalk p₃

Tactic:
⟨nil, p₂, h⟩

Premises used: SimpleGraph.Walk.IsSubwalk, SimpleGraph.Walk.nil, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w u : V
p₁ : G.Walk v w
p₂ : G.Walk w u
p₃ : G.Walk v u
h : p₃ = p₁.append p₂
⊢ p₂.IsSubwalk p₃

Tactic:
⟨p₁, nil, append_nil _ ▸ h⟩

Premises used: Eq.rec, SimpleGraph.Walk.IsSubwalk, SimpleGraph.Walk.nil, Exists.intro, SimpleGraph.Walk.append_nil, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = (append nil (p.take n)).append (p.drop n)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
n : ℕ
⊢ p = ((p.take n).append (p.drop n)).append nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
⊢ p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support

Tactic:
⟨fun ⟨ru, rv, h⟩ ↦ ?_, fun ⟨s, t, h⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.Walk.isSubwalk_iff_support_isInfix.match_2, SimpleGraph.Walk.support, List.IsInfix, SimpleGraph.Walk.IsSubwalk, Iff.intro, _private.0.SimpleGraph.Walk.isSubwalk_iff_support_isInfix.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
refine_1 :
  p₁.IsSubwalk p₂ →
    ∀ (ru : G.Walk v' v) (rv : G.Walk w w') (h : p₂ = (ru.append p₁).append rv), p₁.support <:+: p₂.support
refine_2 : p₁.support <:+: p₂.support → ∀ (s t : List V) (h : s ++ p₁.support ++ t = p₂.support), p₁.IsSubwalk p₂
⊢ p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support

Tactic:
refine ⟨fun ⟨ru, rv, h⟩ ↦ ?_, fun ⟨s, t, h⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.IsSubwalk p₂
ru : G.Walk v' v
rv : G.Walk w w'
h : p₂ = (ru.append p₁).append rv
⊢ p₁.support <:+: p₂.support

Tactic:
grind [support_append, support_append_eq_support_dropLast_append]

Premises used: SimpleGraph.Walk.support_append_eq_support_dropLast_append, SimpleGraph.Walk.support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
⊢ s.length + p₁.length ≤ p₂.length

Tactic:
grind [_=_ length_support]

Premises used: SimpleGraph.Walk.length_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
⊢ s.length + p₁.length ≤ p₂.length

Tactic:
have : (s.length + p₁.length) ≤ p₂.length := by grind [_=_ length_support]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.IsSubwalk p₂

Tactic:
⟨p₂.take s.length |>.copy rfl ?_, p₂.drop (s.length + p₁.length) |>.copy ?_ rfl, ?_⟩

Premises used: SimpleGraph.Walk.length, SimpleGraph.Walk.copy, SimpleGraph.Walk.IsSubwalk, HAdd.hAdd, SimpleGraph.Walk.take, Exists.intro, SimpleGraph.Walk.drop, List.length, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 : p₂.getVert s.length = v
refine_2₁ : p₂.getVert (s.length + p₁.length) = w
refine_2₂ : p₂ = ((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)
⊢ p₁.IsSubwalk p₂

Tactic:
refine ⟨p₂.take s.length |>.copy rfl ?_, p₂.drop (s.length + p₁.length) |>.copy ?_ rfl, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ p₂.length

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.getVert s.length = v

Tactic:
simp [p₂.getVert_eq_support_getElem (by lia : s.length ≤ p₂.length), ← h,
        List.getElem_zero]

Premises used: SimpleGraph.Walk.getVert_eq_support_getElem, List.getElem_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length + p₁.length ≤ p₂.length

Tactic:
omega
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₂.getVert (s.length + p₁.length) = w

Tactic:
simp [p₂.getVert_eq_support_getElem (by omega), ← h, ← p₁.getVert_eq_support_getElem le_rfl]

Premises used: le_rfl, SimpleGraph.Walk.getVert_eq_support_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 :
  p₂.support =
    (((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)).support
⊢ p₂ = ((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)

Tactic:
apply ext_support

Premises used: SimpleGraph.Walk.ext_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 :
  s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      List.drop (min (s.length + p₁.length) p₂.length + 1) (s ++ p₁.support ++ t)
⊢ p₂.support =
    (((Walk.copy (p₂.take s.length) ⋯ ⋯).append p₁).append (Walk.copy (p₂.drop (s.length + p₁.length)) ⋯ ⋯)).support

Tactic:
simp only [← h, support_append, support_copy, take_support_eq_support_take_succ,
      List.take_append, drop_support_eq_support_drop_min, List.tail_drop]

Premises used: List.tail_drop, SimpleGraph.Walk.support_copy, List.take_append, SimpleGraph.Walk.support_append, SimpleGraph.Walk.drop_support_eq_support_drop_min, SimpleGraph.Walk.take_support_eq_support_take_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length + p₁.length ≤ p₂.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s.length ≤ s.length + p₁.length + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ p₁.support.length ≤ s.length + p₁.length + 1 - s.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
refine_2 :
  s ++ v :: p₁.support.tail ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) (v :: p₁.support.tail) ++
          List.take (s.length + 1 - (s ++ v :: p₁.support.tail).length) t ++
        (v :: p₁.support.tail).tail ++
      (HAppend.hAppend (α := List V) [] [] ++
        List.drop (s.length + p₁.length + 1 - (s ++ v :: p₁.support.tail).length) t)
⊢ s ++ p₁.support ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) p₁.support ++
          List.take (s.length + 1 - (s ++ p₁.support).length) t ++
        p₁.support.tail ++
      List.drop (min (s.length + p₁.length) p₂.length + 1) (s ++ p₁.support ++ t)

Tactic:
rw [Nat.min_eq_left (by grind), List.drop_append, List.drop_append,
      List.drop_eq_nil_of_le (by lia), List.drop_eq_nil_of_le (by grind), ← p₁.cons_tail_support]

Premises used: SimpleGraph.Walk.cons_tail_support, Nat.min_eq_left, List.drop_append, List.drop_eq_nil_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
v w v' w' : V
p₁ : G.Walk v w
p₂ : G.Walk v' w'
h_1 : p₁.support <:+: p₂.support
s t : List V
h : s ++ p₁.support ++ t = p₂.support
this : s.length + p₁.length ≤ p₂.length
⊢ s ++ v :: p₁.support.tail ++ t =
    List.take (s.length + 1) s ++ List.take (s.length + 1 - s.length) (v :: p₁.support.tail) ++
          List.take (s.length + 1 - (s ++ v :: p₁.support.tail).length) t ++
        (v :: p₁.support.tail).tail ++
      (HAppend.hAppend (α := List V) [] [] ++
        List.drop (s.length + p₁.length + 1 - (s ++ v :: p₁.support.tail).length) t)

Tactic:
simp +arith [-cons_tail_support]

Premises used: SimpleGraph.Walk.cons_tail_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
rw :
  (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) ↔
    ∃ (k : ℕ),
      p₁.darts.length + k ≤ p₂.darts.length ∧
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
⊢ p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts

Tactic:
rw [isSubwalk_iff_support_isInfix, List.infix_iff_getElem?, List.infix_iff_getElem?]

Premises used: List.infix_iff_getElem?, SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
⊢ p₁.darts.length + k ≤ p₂.darts.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
⊢ p₁.support.length + k ≤ p₂.support.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
refine_1 :
  (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) →
    ∀ (k : ℕ) (hk : p₁.support.length + k ≤ p₂.support.length)
      (h :
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h))
      (i : ℕ) (hi : i < p₁.darts.length),
      getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
        some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi)
refine_2 :
  (∃ (k : ℕ),
      p₁.darts.length + k ≤ p₂.darts.length ∧
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)) →
    ∀ (k : ℕ) (hk : p₁.darts.length + k ≤ p₂.darts.length)
      (h :
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h))
      (i : ℕ) (hi : i < p₁.support.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) p₁.support i hi)
⊢ (∃ (k : ℕ),
      p₁.support.length + k ≤ p₂.support.length ∧
        ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)) ↔
    ∃ (k : ℕ),
      p₁.darts.length + k ≤ p₂.darts.length ∧
        ∀ (i : ℕ) (h : i < p₁.darts.length),
          getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
            some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)

Tactic:
refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
⊢ i + k < p₂.darts.length

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
refine_1 :
  getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯ =
    getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi
⊢ getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
    some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi)

Tactic:
rw [getElem?_pos _ _ <| by grind, Option.some_inj]

Premises used: getElem?_pos, Option.some_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
refine_1 :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯).toProd.1 =
    (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.1
refine_1₁ :
  (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯).toProd.2 =
    (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.2
⊢ getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯ =
    getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯).toProd.1 =
    (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.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.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.support.length + k ≤ p₂.support.length ∧
      ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
k : ℕ
hk : p₁.support.length + k ≤ p₂.support.length
h :
  ∀ (i : ℕ) (h : i < p₁.support.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) p₁.support i h)
i : ℕ
hi : i < p₁.darts.length
⊢ (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) ⋯).toProd.2 =
    (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i hi).toProd.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.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
h_1 :
  ∃ (k : ℕ),
    p₁.darts.length + k ≤ p₂.darts.length ∧
      ∀ (i : ℕ) (h : i < p₁.darts.length),
        getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
          some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h :
  ∀ (i : ℕ) (h : i < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts i h)
i : ℕ
hi : i < p₁.support.length
⊢ i + k < p₂.support.length

Tactic:
grind