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' : 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
refine_2 :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
⊢ 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)

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₁.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
pos :
  ∀ (hi' : i = p₁.length),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
neg :
  ∀ (hi' : ¬i = p₁.length),
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
      getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi

Tactic:
by_cases hi' : i = p₁.length

Premises used: SimpleGraph.Walk.length
-- 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
hi' : i = p₁.length
⊢ ∀ (h : i - 1 < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i - 1 + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts (i - 1) h)

Tactic:
have := h <| i - 1
-- 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
hi' : i = p₁.length
this :
  ∀ (h : i - 1 < p₁.darts.length),
    getElem? (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₂.darts (i - 1 + k) =
      some (getElem (valid := fun (as : List G.Dart) (i : ℕ) ↦ i < as.length) p₁.darts (i - 1) h)
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi

Tactic:
grind [not_nil_iff_lt_length, snd_darts_getElem]

Premises used: SimpleGraph.Walk.snd_darts_getElem, SimpleGraph.Walk.not_nil_iff_lt_length
-- 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
hi' : ¬i = p₁.length
⊢ ∀ (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:
have := h i
-- 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
hi' : ¬i = p₁.length
this :
  ∀ (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)
⊢ getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₂.support (i + k) ⋯ =
    getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) p₁.support i hi

Tactic:
grind [fst_darts_getElem]

Premises used: SimpleGraph.Walk.fst_darts_getElem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v v' : V
p : G.Walk u v
⊢ IsSubwalk (u₁ := v') nil p ↔ v' ∈ p.support

Tactic:
isSubwalk_iff_support_isInfix.trans <| p.support.singleton_infix_iff _

Premises used: List.singleton_infix_iff, SimpleGraph.Walk.support, Iff.trans, 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
h : G.Adj u' v'
⊢ h.toWalk.IsSubwalk p ↔ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts

Tactic:
simp [isSubwalk_iff_darts_isInfix, List.singleton_infix_iff]

Premises used: List.singleton_infix_iff, SimpleGraph.Walk.isSubwalk_iff_darts_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
d : G.Dart
p : G.Walk u v
⊢ ⋯.toWalk.IsSubwalk p ↔ d ∈ p.darts

Tactic:
isSubwalk_toWalk_iff_mem_darts ..

Premises used: SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_darts
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
rw :
  { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts ↔
    ∃ a ∈ p.darts, a.edge = s(u', v')
⊢ h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges

Tactic:
rw [isSubwalk_toWalk_iff_mem_darts, isSubwalk_toWalk_iff_mem_darts, edges, List.mem_map]

Premises used: SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_darts, List.mem_map, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
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 ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
⊢ ∃ a ∈ p.darts, a.edge = s(u', v')

Tactic:
grind [Dart.edge]

Premises used: SimpleGraph.Dart.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
refine :
  ∀ (h_1 : ∃ a ∈ p.darts, a.edge = s(u', v')),
    { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
⊢ { fst := u', snd := v', adj := h : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts ↔
    ∃ a ∈ p.darts, a.edge = s(u', v')

Tactic:
refine ⟨fun h ↦ by grind [Dart.edge], fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h : ∃ a ∈ p.darts, a.edge = s(u', v')
have :
  ∀ (d : G.Dart) (hd : d ∈ p.darts) (h : d.edge = s(u', v')),
    { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts

Tactic:
have ⟨d, hd, h⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : d.edge = s(u', v')
⊢ (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap

Tactic:
rw [Dart.edge, Sym2.eq, Sym2.rel_iff'] at h

Premises used: Sym2.eq, Sym2.rel_iff', SimpleGraph.Dart.edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts

Tactic:
h.imp (fun h ↦ ?_) (fun h ↦ ?_)

Premises used: Or.imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
refine_1 : ∀ (h : (d.toProd.1, d.toProd.2) = (u', v')), { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts
refine_2 : ∀ (h : (d.toProd.1, d.toProd.2) = (u', v').swap), { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts

Tactic:
refine h.imp (fun h ↦ ?_) (fun h ↦ ?_)

Premises used: Or.imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ d ∈ p.darts

Tactic:
hd
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
h₁ : (u', v') = d.toProd
⊢ { fst := u', snd := v', adj := h_1 : G.Dart } ∈ p.darts

Tactic:
convert! hd using 2
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ d ∈ p.darts

Tactic:
hd
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
h₁ : (v', u') = d.toProd
⊢ { fst := v', snd := u', adj := ⋯ : G.Dart } ∈ p.darts

Tactic:
convert! hd using 2
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd

Tactic:
h.symm

Premises used: Prod.swap, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h_1 : G.Adj u' v'
h_2 : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h_3 : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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
refine_2 : ∀ (h : s(u', v') ∈ p.edges), [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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
⊢ G.Adj u' v'

Tactic:
have := h.elim adj_of_infix_support (adj_of_infix_support · |>.symm)
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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
this : G.Adj u' v'
⊢ s(u', v') ∈ p.edges

Tactic:
simpa [← isSubwalk_toWalk_iff_mem_edges this, isSubwalk_iff_support_isInfix]

Premises used: SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_edges, 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
h : s(u', v') ∈ p.edges
⊢ ⋯.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p

Tactic:
have := (isSubwalk_toWalk_iff_mem_edges <| p.adj_of_mem_edges h).mpr h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : s(u', v') ∈ p.edges
this : ⋯.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p
⊢ [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support

Tactic:
simpa [isSubwalk_iff_support_isInfix]

Premises used: SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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₁.support <:+: p₂.support

Tactic:
rw [isSubwalk_iff_support_isInfix] at h₁ h₂

Premises used: SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
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₂.support <:+: p₁.support

Tactic:
rw [isSubwalk_iff_support_isInfix] at h₁ h₂

Premises used: SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.support <:+: p₂.support
h₂ : p₂.support <:+: p₁.support
⊢ p₁ = p₂

Tactic:
ext_support <| List.infix_antisymm h₁ h₂

Premises used: SimpleGraph.Walk.ext_support, List.infix_antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v : V
p₁ p₂ : G.Walk u v
h₁ : p₁.support <:+: p₂.support
h₂ : p₂.support <:+: p₁.support
⊢ p₁ = p₂

Tactic:
exact ext_support <| List.infix_antisymm h₁ h₂

Premises used: SimpleGraph.Walk.ext_support, List.infix_antisymm
-- 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'
h : p₂.IsSubwalk p₁
⊢ p₂.support ⊆ p₁.support

Tactic:
(isSubwalk_iff_support_isInfix.mp h).subset

Premises used: List.IsInfix.subset, Iff.mp, 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'
h : p₁.IsSubwalk p₂
⊢ p₁.edges <:+: p₂.edges

Tactic:
grind [edges_append, IsSubwalk]

Premises used: SimpleGraph.Walk.IsSubwalk, SimpleGraph.Walk.edges_append
-- 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'
h : p₂.IsSubwalk p₁
⊢ p₂.edges ⊆ p₁.edges

Tactic:
h.edges_isInfix.subset

Premises used: List.IsInfix.subset, SimpleGraph.Walk.IsSubwalk.edges_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'
h : p₁.IsSubwalk p₂
⊢ p₁.darts <:+: p₂.darts

Tactic:
grind [darts_append, IsSubwalk]

Premises used: SimpleGraph.Walk.IsSubwalk, SimpleGraph.Walk.darts_append
-- 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'
h : p₂.IsSubwalk p₁
⊢ p₂.darts ⊆ p₁.darts

Tactic:
h.darts_isInfix.subset

Premises used: List.IsInfix.subset, SimpleGraph.Walk.IsSubwalk.darts_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G G' : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
h : p₂.IsSubwalk p₁
f : G →g G'
⊢ (Walk.map f p₂).IsSubwalk (Walk.map f p₁)

Tactic:
simp [isSubwalk_iff_support_isInfix, isSubwalk_iff_support_isInfix.mp h, List.IsInfix.map]

Premises used: List.IsInfix.map, Iff.mp, SimpleGraph.Walk.isSubwalk_iff_support_isInfix
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' x y x' y' : V
p : G.Walk x y
q : G.Walk u v
h : p.IsSubwalk q
hx : x = x'
hy : y = y'
hu : u = u'
hv : v = v'
⊢ (p.copy hx hy).IsSubwalk (q.copy hu hv)

Tactic:
simp [isSubwalk_iff_support_isInfix, isSubwalk_iff_support_isInfix.mp h]

Premises used: Iff.mp, 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
q : G.Walk u' v'
hpq : p.IsSubwalk q
⊢ p.dropLast.IsSubwalk q

Tactic:
(isSubwalk_take _ _).trans hpq

Premises used: SimpleGraph.Walk.isSubwalk_take, SimpleGraph.Walk.dropLast, SimpleGraph.Walk.IsSubwalk.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
⊢ p.tail.IsSubwalk q

Tactic:
(isSubwalk_drop _ _).trans hpq

Premises used: SimpleGraph.Walk.isSubwalk_drop, SimpleGraph.Walk.tail, SimpleGraph.Walk.IsSubwalk.trans
-- 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.take n).IsSubwalk (p.take 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.take n).IsSubwalk (p.take k)
succ : (p.take k).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))
⊢ (p.take n).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))

Tactic:
apply ih.trans

Premises used: SimpleGraph.Walk.IsSubwalk.trans
-- 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.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))
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))
⊢ (p.take k).IsSubwalk (v₂ := p.getVert (k + 1)) (p.take (k + 1))

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u : V
n k_1 k : ℕ
h : n ≤ k
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:
isSubwalk_take _ _

Premises used: SimpleGraph.Walk.isSubwalk_take, SimpleGraph.Walk.take, SimpleGraph.Walk.getVert
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
Goal:
V : Type u_1
G : SimpleGraph V
u : V
n k_1 k : ℕ
h : n ≤ k
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:
exact isSubwalk_take _ _

Premises used: SimpleGraph.Walk.isSubwalk_take