awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
exact Or.inr hx

Premises used: Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.takeUntil u h).edges ⊆ p.edges

Tactic:
List.map_subset _ (p.darts_takeUntil_subset h)

Premises used: List.map_subset, SimpleGraph.Walk.darts_takeUntil_subset, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ (p.dropUntil u h).edges ⊆ p.edges

Tactic:
List.map_subset _ (p.darts_dropUntil_subset h)

Premises used: List.map_subset, SimpleGraph.Walk.darts_dropUntil_subset, SimpleGraph.Walk.edges
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length

Tactic:
have := congr_arg Walk.length (p.take_spec h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.takeUntil u h).length + (p.dropUntil u h).length = p.length

Tactic:
rw [length_append] at this

Premises used: SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
Nat.le.intro this

Premises used: Nat.le.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.takeUntil u h).length + (p.dropUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ p.length

Tactic:
exact Nat.le.intro this

Premises used: Nat.le.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : ((p.takeUntil u h).append (p.dropUntil u h)).length = p.length
⊢ (p.dropUntil u h).length + (p.takeUntil u h).length = p.length

Tactic:
rw [length_append, add_comm] at this

Premises used: add_comm, SimpleGraph.Walk.length_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.dropUntil u h).length + (p.takeUntil u h).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
Nat.le.intro this

Premises used: Nat.le.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
this : (p.dropUntil u h).length + (p.takeUntil u h).length = p.length
⊢ (p.dropUntil u h).length ≤ p.length

Tactic:
exact Nat.le.intro this

Premises used: Nat.le.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x u_1 : V
q : G.Walk u_1 w
hx : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) x
⊢ x = u_1

Tactic:
rw [mem_support_nil_iff] at hx

Premises used: SimpleGraph.Walk.mem_support_nil_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x u_1 : V
q : G.Walk u_1 w
hx_1 : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) x
hx : x = u_1
nil :
  ∀ (hx : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u_1),
    (append Walk.nil q).takeUntil u_1 ⋯ = takeUntil Walk.nil u_1 hx
⊢ (append Walk.nil q).takeUntil x ⋯ = takeUntil Walk.nil x hx_1

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
u_1 : V
q : G.Walk u_1 w
hx : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1
⊢ (append nil q).takeUntil u_1 ⋯ = takeUntil nil u_1 hx

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (q : G.Walk w_1 w) (hx : x ∈ p.support), (p.append q).takeUntil x ⋯ = p.takeUntil x hx
q : G.Walk w_1 w
hx : x ∈ (cons h p).support
⊢ ((cons h p).append q).takeUntil x ⋯ = (cons h p).takeUntil x hx

Tactic:
grind [cons_append, takeUntil]

Premises used: SimpleGraph.Walk.cons_append, SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
x : V
p : G.Walk u v
q : G.Walk v w
hx : x ∈ p.support
nil :
  ∀ {u : V} (q : G.Walk u w) (hx : Membership.mem (γ := List V) (support (G := G) (u := u) Walk.nil) x),
    (append Walk.nil q).takeUntil x ⋯ = takeUntil Walk.nil x hx
cons :
  ∀ {u v w_1 : V} (h : G.Adj u v) (p : G.Walk v w_1),
    (∀ (q : G.Walk w_1 w) (hx : x ∈ p.support), (p.append q).takeUntil x ⋯ = p.takeUntil x hx) →
      ∀ (q : G.Walk w_1 w) (hx : x ∈ (Walk.cons h p).support),
        ((Walk.cons h p).append q).takeUntil x ⋯ = (Walk.cons h p).takeUntil x hx
⊢ (p.append q).takeUntil x ⋯ = p.takeUntil x hx

Tactic:
induction p with
  | nil => rw [mem_support_nil_iff] at hx; subst_vars; simp
  | cons => grind [cons_append, takeUntil]

Premises used: SimpleGraph.Walk.cons_append, SimpleGraph.Walk.mem_support_nil_iff, SimpleGraph.Walk.cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
rw :
  if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
  else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
| p.getVert n

Tactic:
rw [← take_spec p hw, getVert_append]

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
conv_rhs :
  (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
⊢ (p.takeUntil w hw).getVert n = p.getVert n

Tactic:
conv_rhs => rw [← take_spec p hw, getVert_append]

Premises used: SimpleGraph.Walk.getVert_append, SimpleGraph.Walk.take_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
inl :
  n < (p.takeUntil w hw).length →
    (p.takeUntil w hw).getVert n =
      if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
      else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
inr :
  n = (p.takeUntil w hw).length →
    (p.takeUntil w hw).getVert n =
      if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
      else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

Tactic:
cases hn.lt_or_eq

Premises used: LE.le.lt_or_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h : n < (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
w : V
inst : DecidableEq V
u v : V
n : ℕ
p : G.Walk u v
hw : w ∈ p.support
hn : n ≤ (p.takeUntil w hw).length
h : n = (p.takeUntil w hw).length
⊢ (p.takeUntil w hw).getVert n =
    if n < (p.takeUntil w hw).length then (p.takeUntil w hw).getVert n
    else (p.dropUntil w hw).getVert (n - (p.takeUntil w hw).length)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
apply : 1 ≤ (p.takeUntil w h).length
⊢ (p.takeUntil w h).snd = p.snd

Tactic:
apply p.getVert_takeUntil h

Premises used: SimpleGraph.Walk.getVert_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
contrapose : ∀ (hsu : ¬1 ≤ (p.takeUntil w h).length), w = u
⊢ 1 ≤ (p.takeUntil w h).length

Tactic:
contrapose hsu
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
symm : u = w
⊢ w = u

Tactic:
symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
hsu : ¬1 ≤ (p.takeUntil w h).length
⊢ u = w

Tactic:
simpa [length_eq_zero_iff] using hsu

Premises used: SimpleGraph.Walk.length_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
⊢ ((p.takeUntil u h).append (p.dropUntil u h)).getVert (p.takeUntil u h).length = p.getVert (p.takeUntil u h).length

Tactic:
have := congr_arg₂ (y := (p.takeUntil _ h).length) getVert (p.take_spec h) rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
p : G.Walk v w
h : u ∈ p.support
this :
  ((p.takeUntil u h).append (p.dropUntil u h)).getVert (p.takeUntil u h).length = p.getVert (p.takeUntil u h).length
⊢ p.getVert (p.takeUntil u h).length = u

Tactic:
grind [getVert_append, getVert_zero]

Premises used: SimpleGraph.Walk.getVert_zero, SimpleGraph.Walk.getVert_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
⊢ n < (p.takeUntil (p.getVert n) h).support.dropLast.length

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
⊢ n < (p.takeUntil (p.getVert n) h).support.dropLast.length

Tactic:
have h₁ : n < (p.takeUntil _ h).support.dropLast.length := by simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
simp_rw :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p.takeUntil (p.getVert n) h).support n ⋯ ∈
    (p.takeUntil (p.getVert n) h).support.dropLast
simp_rw₁ :
  getElem (valid := fun (as : List V) (i : ℕ) ↦ i < as.length) (p.takeUntil (p.getVert n) h).support.dropLast n h₁ ∈
    (p.takeUntil (p.getVert n) h).support.dropLast
⊢ p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast

Tactic:
simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le,
      ← List.getElem_dropLast h₁, List.getElem_mem h₁]

Premises used: List.getElem_dropLast, List.getElem_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
⊢ p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast

Tactic:
have : p.getVert n ∈ (p.takeUntil _ h).support.dropLast := by
    simp_rw [p.getVert_takeUntil h hn.le ▸ getVert_eq_support_getElem _ hn.le,
      ← List.getElem_dropLast h₁, List.getElem_mem h₁]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
⊢ List.count (p.getVert n) ((p.takeUntil (p.getVert n) h).support.dropLast ++ [p.getVert n]) = 1

Tactic:
have := dropLast_support_concat _ ▸ p.count_support_takeUntil_eq_one h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : p.getVert n ∈ p.support
hn : n < (p.takeUntil (p.getVert n) h).length
h₁ : n < (p.takeUntil (p.getVert n) h).support.dropLast.length
this_1 : p.getVert n ∈ (p.takeUntil (p.getVert n) h).support.dropLast
this : List.count (p.getVert n) ((p.takeUntil (p.getVert n) h).support.dropLast ++ [p.getVert n]) = 1
⊢ False

Tactic:
grind [List.not_mem_of_count_eq_zero]

Premises used: List.not_mem_of_count_eq_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
n : ℕ
p : G.Walk v w
h : u ∈ p.support
hn : n ≤ (p.takeUntil u h).length
⊢ p.getVert n = u ↔ n = (p.takeUntil u h).length

Tactic:
grind [getVert_length_takeUntil, getVert_lt_length_takeUntil_ne]

Premises used: SimpleGraph.Walk.getVert_lt_length_takeUntil_ne, SimpleGraph.Walk.getVert_length_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
rw : (p.takeUntil u h).length ≠ p.length
⊢ (p.takeUntil u h).length < p.length

Tactic:
rw [(p.length_takeUntil_le h).lt_iff_ne]

Premises used: SimpleGraph.Walk.length_takeUntil_le, LE.le.lt_iff_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ (p.takeUntil u h).length

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ u = w

Tactic:
simpa using (hl ▸ getVert_takeUntil h (by rfl) :
    (p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length)

Premises used: SimpleGraph.Walk.getVert_takeUntil, Eq.rec
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length ≠ p.length

Tactic:
exact fun hl ↦ huw (by simpa using (hl ▸ getVert_takeUntil h (by rfl) :
    (p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length))
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
w x : V
p : G.Walk u v
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
simp_rw : ((p.takeUntil w hw).append (p.dropUntil w hw)).takeUntil x ⋯ = p.takeUntil x ⋯
⊢ (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯

Tactic:
simp_rw [← takeUntil_append_of_mem_left _ (p.dropUntil w hw) hx, take_spec]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.takeUntil_append_of_mem_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
rw : w ∉ ((p.takeUntil w hw).takeUntil x hx).support
⊢ w ∉ (p.takeUntil x ⋯).support

Tactic:
rw [← takeUntil_takeUntil p hw hx]

Premises used: SimpleGraph.Walk.takeUntil_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
⊢ (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length

Tactic:
length_takeUntil_lt _ h.symm

Premises used: SimpleGraph.Walk.length_takeUntil_lt, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
⊢ (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length

Tactic:
exact length_takeUntil_lt _ h.symm

Premises used: SimpleGraph.Walk.length_takeUntil_lt, Ne.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
⊢ (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length

Tactic:
have h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length
      < ((p.takeUntil w hw).takeUntil x hx).length := by
    exact length_takeUntil_lt _ h.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length

Tactic:
length_takeUntil_lt _ h

Premises used: SimpleGraph.Walk.length_takeUntil_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length

Tactic:
exact length_takeUntil_lt _ h

Premises used: SimpleGraph.Walk.length_takeUntil_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
⊢ ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length

Tactic:
have h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length := by
    exact length_takeUntil_lt _ h
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
⊢ (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length

Tactic:
simp only [takeUntil_takeUntil] at h1 h2

Premises used: SimpleGraph.Walk.takeUntil_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (((p.takeUntil w hw).takeUntil x hx).takeUntil w hw').length < ((p.takeUntil w hw).takeUntil x hx).length
h2 : ((p.takeUntil w hw).takeUntil x hx).length < (p.takeUntil w hw).length
h1₁ : (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length
⊢ (p.takeUntil x ⋯).length < (p.takeUntil w hw).length

Tactic:
simp only [takeUntil_takeUntil] at h1 h2

Premises used: SimpleGraph.Walk.takeUntil_takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
w x : V
h : x ≠ w
hw : w ∈ p.support
hx : x ∈ (p.takeUntil w hw).support
hw' : w ∈ ((p.takeUntil w hw).takeUntil x hx).support
h1 : (p.takeUntil w ⋯).length < (p.takeUntil x ⋯).length
h2 : (p.takeUntil x ⋯).length < (p.takeUntil w hw).length
⊢ False

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
simp : (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail
⊢ (c.rotate u h).support.tail ~r c.support.tail

Tactic:
simp only [rotate, tail_support_append]

Premises used: SimpleGraph.Walk.rotate, SimpleGraph.Walk.tail_support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
apply : (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail
⊢ (c.dropUntil u h).support.tail ++ (c.takeUntil u h).support.tail ~r c.support.tail

Tactic:
apply List.IsRotated.trans List.isRotated_append

Premises used: List.isRotated_append, List.IsRotated.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
rw : ((c.takeUntil u h).append (c.dropUntil u h)).support.tail ~r c.support.tail
rw₁ rw₂ : c.support.tail ~r c.support.tail
⊢ (c.takeUntil u h).support.tail ++ (c.dropUntil u h).support.tail ~r c.support.tail

Tactic:
rw [← tail_support_append, take_spec]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.tail_support_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ w ∈ (c.rotate u h).support ↔ w ∈ c.support

Tactic:
grind [rotate, take_spec, mem_support_append_iff]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.rotate, SimpleGraph.Walk.mem_support_append_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
simp : (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts
⊢ (c.rotate u h).darts ~r c.darts

Tactic:
simp only [rotate, darts_append]

Premises used: SimpleGraph.Walk.rotate, SimpleGraph.Walk.darts_append
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
apply : (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts
⊢ (c.dropUntil u h).darts ++ (c.takeUntil u h).darts ~r c.darts

Tactic:
apply List.IsRotated.trans List.isRotated_append

Premises used: List.isRotated_append, List.IsRotated.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
rw : ((c.takeUntil u h).append (c.dropUntil u h)).darts ~r c.darts
rw₁ rw₂ : c.darts ~r c.darts
⊢ (c.takeUntil u h).darts ++ (c.dropUntil u h).darts ~r c.darts

Tactic:
rw [← darts_append, take_spec]

Premises used: SimpleGraph.Walk.take_spec, SimpleGraph.Walk.darts_append