awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
nil : Eq (α := G.Walk v v) (takeUntil Walk.nil v ⋯) Walk.nil
cons : ∀ {v_1 : V} (h : G.Adj u v_1) (p : G.Walk v_1 v), (Walk.cons h p).takeUntil u ⋯ = Walk.nil
⊢ p.takeUntil u ⋯ = Walk.nil

Tactic:
cases p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v : V
inst : DecidableEq V
⊢ Eq (α := G.Walk v v) (takeUntil nil v ⋯) nil

Tactic:
simp [Walk.takeUntil]

Premises used: SimpleGraph.Walk.takeUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
v_1 : V
h : G.Adj u v_1
p : G.Walk v_1 v
⊢ (cons h p).takeUntil u ⋯ = nil

Tactic:
simp [Walk.takeUntil]

Premises used: SimpleGraph.Walk.takeUntil
-- 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
h₁ :
  (p.takeUntil w h).support =
    (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support
⊢ p.takeUntil w h = Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯

Tactic:
apply ext_support

Premises used: SimpleGraph.Walk.ext_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
u_1 : V
h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w
h₁ : (cast ⋯ nil).support = [u_1]
⊢ (takeUntil nil w h).support =
    (Walk.copy (v := getVert (G := G) (u := u_1) nil (List.idxOf w (support (G := G) (u := u_1) nil)))
        (take nil (List.idxOf w (support (G := G) (u := u_1) nil))) ⋯ ⋯).support

Tactic:
simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.support_nil, SimpleGraph.Walk.take, SimpleGraph.Walk.getVert_nil, SimpleGraph.Walk.takeUntil, eq_mpr_eq_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
u_1 : V
h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w
⊢ (cast ⋯ nil).support = [u_1]

Tactic:
grind [mem_support_nil_iff, support_nil]

Premises used: SimpleGraph.Walk.support_nil, 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
u_1 v_1 w_1 : V
hadj : G.Adj u_1 v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.takeUntil w h).support =
      (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons hadj p).support
⊢ ((cons hadj p).takeUntil w h).support =
    (Walk.copy (v := (cons hadj p).getVert (List.idxOf w (cons hadj p).support))
        ((cons hadj p).take (List.idxOf w (cons hadj p).support)) ⋯ ⋯).support

Tactic:
grind [takeUntil, support, copy_rfl_rfl, take_support_eq_support_take_succ]

Premises used: SimpleGraph.Walk.copy_rfl_rfl, SimpleGraph.Walk.support, SimpleGraph.Walk.takeUntil, SimpleGraph.Walk.take_support_eq_support_take_succ
-- 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
h₁ :
  ∀ {u : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) w),
    (takeUntil nil w h).support =
      (Walk.copy (v := getVert (G := G) (u := u) nil (List.idxOf w (support (G := G) (u := u) nil)))
          (take nil (List.idxOf w (support (G := G) (u := u) nil))) ⋯ ⋯).support
h₂ :
  ∀ {u v w_1 : V} (hadj : G.Adj u v) (p : G.Walk v w_1)
    (ih :
      ∀ (h : w ∈ p.support),
        (p.takeUntil w h).support =
          (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support)
    (h : w ∈ (cons hadj p).support),
    ((cons hadj p).takeUntil w h).support =
      (Walk.copy (v := (cons hadj p).getVert (List.idxOf w (cons hadj p).support))
          ((cons hadj p).take (List.idxOf w (cons hadj p).support)) ⋯ ⋯).support
⊢ (p.takeUntil w h).support =
    (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support

Tactic:
induction p with
  | nil =>
    simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]
    grind [mem_support_nil_iff, support_nil]
  | cons hadj p ih =>
    grind [takeUntil, support, copy_rfl_rfl, take_support_eq_support_take_succ]

Premises used: SimpleGraph.Walk.copy_rfl_rfl, SimpleGraph.Walk.support_copy, SimpleGraph.Walk.support, SimpleGraph.Walk.support_nil, SimpleGraph.Walk.mem_support_nil_iff, SimpleGraph.Walk.cons, SimpleGraph.Walk.take, SimpleGraph.Walk.nil, SimpleGraph.Walk.getVert_nil, SimpleGraph.Walk.takeUntil, eq_mpr_eq_cast, SimpleGraph.Walk.take_support_eq_support_take_succ
-- 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
⊢ (p.takeUntil w h).length = List.idxOf w p.support

Tactic:
simp [takeUntil_eq_take, Nat.le_iff_lt_add_one, ← length_support, List.idxOf_lt_length_of_mem h]

Premises used: List.idxOf_lt_length_of_mem, SimpleGraph.Walk.length_support, SimpleGraph.Walk.takeUntil_eq_take, Nat.le_iff_lt_add_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
v w u : V
h : Membership.mem (γ := List V) (support (G := G) (u := v) nil) u
rw rw₁ : G.Walk v v
⊢ G.Walk u v

Tactic:
rw [mem_support_nil_iff.mp h]

Premises used: SimpleGraph.Walk.mem_support_nil_iff, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u_1 : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
u : V
h : u ∈ (cons r p).support
hx : v = u
subst : (h : v ∈ (cons r p).support) → G.Walk v w
⊢ G.Walk u w

Tactic:
subst u
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v_1 w_1 u : V
inst : DecidableEq V
v w_2 w v_2 : V
r : G.Adj v v_2
p : G.Walk v_2 w
h : v ∈ (cons r p).support
⊢ G.Walk v w

Tactic:
exact cons r p

Premises used: SimpleGraph.Walk.cons
-- 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
nil :
  ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) Walk.nil) u),
    (takeUntil Walk.nil u h).append (dropUntil Walk.nil u h) = Walk.nil
cons :
  ∀ {u_1 v w : V} (h : G.Adj u_1 v) (p : G.Walk v w),
    (∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p) →
      ∀ (h_1 : u ∈ (Walk.cons h p).support),
        ((Walk.cons h p).takeUntil u h_1).append ((Walk.cons h p).dropUntil u h_1) = Walk.cons h p
⊢ (p.takeUntil u h).append (p.dropUntil u h) = p

Tactic:
induction p
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 : V
h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u
⊢ u = u_1

Tactic:
rw [mem_support_nil_iff] at h

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

Tactic:
subst u
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w u : V
h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
⊢ (takeUntil nil u h).append (dropUntil nil u h) = nil

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h_1 : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h : u ∈ (Walk.cons h_1 p).support
cons : ∀ (h : G.Adj u v_1), ((Walk.cons h p).takeUntil u ⋯).append ((Walk.cons h p).dropUntil u ⋯) = Walk.cons h p
cons₁ :
  ∀ (a : List.Mem u p.support),
    ((Walk.cons h_1 p).takeUntil u ⋯).append ((Walk.cons h_1 p).dropUntil u ⋯) = Walk.cons h_1 p
⊢ ((Walk.cons h_1 p).takeUntil u h).append ((Walk.cons h_1 p).dropUntil u h) = Walk.cons h_1 p

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

Tactic:
simp!
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h_1 : List.Mem u p.support
cons :
  append (v := u)
      (if hx : u_1 = u then Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil hx
      else Walk.cons h (p.takeUntil u ⋯))
      (if h_2 : u_1 = u then
        Eq.rec (motive := fun (x : V) (x_1 : u_1 = x) ↦ (h : x ∈ u_1 :: p.support) → G.Walk x w_1)
          (fun (h_3 : u_1 ∈ u_1 :: p.support) ↦ Walk.cons h p) ⋯ ⋯
      else p.dropUntil u ⋯) =
    Walk.cons h p
⊢ ((Walk.cons h p).takeUntil u ⋯).append ((Walk.cons h p).dropUntil u ⋯) = Walk.cons h p

Tactic:
simp! only
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h_1 : List.Mem u p.support
pos :
  ∀ (h' : u_1 = u),
    append (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h')
        (Eq.rec (motive := fun (x : V) (x_1 : u_1 = x) ↦ (h : x ∈ u_1 :: p.support) → G.Walk x w_1)
          (fun (h_2 : u_1 ∈ u_1 :: p.support) ↦ cons h p) ⋯ ⋯) =
      cons h p
neg : ∀ (h' : ¬u_1 = u), (cons h (p.takeUntil u ⋯)).append (p.dropUntil u ⋯) = cons h p
⊢ append (v := u)
      (if hx : u_1 = u then Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil hx
      else cons h (p.takeUntil u ⋯))
      (if h_2 : u_1 = u then
        Eq.rec (motive := fun (x : V) (x_1 : u_1 = x) ↦ (h : x ∈ u_1 :: p.support) → G.Walk x w_1)
          (fun (h_3 : u_1 ∈ u_1 :: p.support) ↦ cons h p) ⋯ ⋯
      else p.dropUntil u ⋯) =
    cons h p

Tactic:
split_ifs with h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h_1 : List.Mem u p.support
h' : u_1 = u
pos :
  (∀ (h : u_1 ∈ p.support), (p.takeUntil u_1 h).append (p.dropUntil u_1 h) = p) →
    ∀ (a : List.Mem u_1 p.support),
      append (v := u_1) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil ⋯)
          (Eq.rec (motive := fun (x : V) (x_1 : u_1 = x) ↦ (h : x ∈ u_1 :: p.support) → G.Walk x w_1)
            (fun (h_2 : u_1 ∈ u_1 :: p.support) ↦ cons h p) ⋯ ⋯) =
        cons h p
⊢ append (v := u) (Eq.rec (motive := fun (x : V) (h : u_1 = x) ↦ G.Walk u_1 x) nil h')
      (Eq.rec (motive := fun (x : V) (x_1 : u_1 = x) ↦ (h : x ∈ u_1 :: p.support) → G.Walk x w_1)
        (fun (h_2 : u_1 ∈ u_1 :: p.support) ↦ cons h p) ⋯ ⋯) =
    cons h p

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
v w u v_1 w_1 : V
h : G.Adj u v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h_1 : List.Mem u p.support
⊢ append (v := u) (Eq.rec (motive := fun (x : V) (h : u = x) ↦ G.Walk u x) nil ⋯)
      (Eq.rec (motive := fun (x : V) (x_1 : u = x) ↦ (h : x ∈ u :: p.support) → G.Walk x w_1)
        (fun (h_2 : u ∈ u :: p.support) ↦ cons h p) ⋯ ⋯) =
    cons h p

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w u_1 v_1 w_1 : V
h : G.Adj u_1 v_1
p : G.Walk v_1 w_1
p_ih : ∀ (h : u ∈ p.support), (p.takeUntil u h).append (p.dropUntil u h) = p
h_1 : List.Mem u p.support
h' : ¬u_1 = u
⊢ (cons h (p.takeUntil u ⋯)).append (p.dropUntil u ⋯) = cons h p

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
h : u ∈ p.support
unfold :
  (match (motive := (w : V) → (x : G.Walk u w) → (x_1 : V) → x_1 ∈ x.support → G.Walk x_1 w) v, p, u, h with
    | .(u), nil, u_1, h => ⋯.mpr nil
    | w, cons r p, u_1, h =>
      if hx : u = u_1 then
        Eq.ndrec (motive := fun (u_2 : V) ↦ (h : u_2 ∈ (cons r p).support) → G.Walk u_2 w)
          (fun (h : u ∈ (cons r p).support) ↦ cons r p) hx h
      else p.dropUntil u_1 ⋯) =
    p
⊢ p.dropUntil u h = p

Tactic:
unfold dropUntil

Premises used: SimpleGraph.Walk.dropUntil
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
h : u ∈ p.support
h_1 :
  ∀ (w : V) (x : G.Walk u w),
    ∀ x_1 ∈ x.support, ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u), ⋯.mpr nil = nil
h_2 :
  ∀ (w : V) (x : G.Walk u w),
    ∀ x_1 ∈ x.support,
      ∀ (v_1 : V) (r : G.Adj u v_1) (p : G.Walk v_1 v) (h : u ∈ (cons r p).support),
        (if hx : u = u then
            Eq.ndrec (motive := fun (u_1 : V) ↦ (h : u_1 ∈ (cons r p).support) → G.Walk u_1 v)
              (fun (h : u ∈ (cons r p).support) ↦ cons r p) hx h
          else p.dropUntil u ⋯) =
          cons r p
⊢ (match (motive := (w : V) → (x : G.Walk u w) → (x_1 : V) → x_1 ∈ x.support → G.Walk x_1 w) v, p, u, h with
    | .(u), nil, u_1, h => ⋯.mpr nil
    | w, cons r p, u_1, h =>
      if hx : u = u_1 then
        Eq.ndrec (motive := fun (u_2 : V) ↦ (h : u_2 ∈ (cons r p).support) → G.Walk u_2 w)
          (fun (h : u ∈ (cons r p).support) ↦ cons r p) hx h
      else p.dropUntil u_1 ⋯) =
    p

Tactic:
split
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u : V
inst : DecidableEq V
w : V
x : G.Walk u w
x_1 : V
h_1 : x_1 ∈ x.support
h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) u
⊢ ⋯.mpr nil = nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
w : V
x : G.Walk u w
x_1 : V
h_1 : x_1 ∈ x.support
v_1 : V
r : G.Adj u v_1
p : G.Walk v_1 v
h : u ∈ (cons r p).support
⊢ (if hx : u = u then
      Eq.ndrec (motive := fun (u_1 : V) ↦ (h : u_1 ∈ (cons r p).support) → G.Walk u_1 v)
        (fun (h : u ∈ (cons r p).support) ↦ cons r p) hx h
    else p.dropUntil u ⋯) =
    cons r p

Tactic:
simp
-- 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
h₁ :
  (p.dropUntil w h).support =
    (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
⊢ p.dropUntil w h = Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯

Tactic:
apply ext_support

Premises used: SimpleGraph.Walk.ext_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
u_1 : V
h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) w
h₁ : (cast ⋯ nil).support = [u_1]
⊢ (dropUntil nil w h).support =
    (Walk.copy (u := getVert (G := G) (u := u_1) nil (List.idxOf w (support (G := G) (u := u_1) nil)))
        (drop nil (List.idxOf w (support (G := G) (u := u_1) nil))) ⋯ ⋯).support

Tactic:
simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.support_nil, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.getVert_nil, SimpleGraph.Walk.drop, eq_mpr_eq_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
a v_1 w_1 : V
h_1 : G.Adj a v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons h_1 p).support
pos :
  ∀ (h' : w = a),
    ((cons h_1 p).dropUntil w h).support =
      (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
          ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support
neg :
  ∀ (h' : w ≠ a),
    ((cons h_1 p).dropUntil w h).support =
      (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
          ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support
⊢ ((cons h_1 p).dropUntil w h).support =
    (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
        ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support

Tactic:
by_cases! h' : w = a
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
a v_1 w_1 : V
h_1 : G.Adj a v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons h_1 p).support
h' : w = a
pos :
  ∀ (h : G.Adj w v_1) (h_2 : w ∈ (cons h p).support),
    ((cons h p).dropUntil w h_2).support =
      (Walk.copy (u := (cons h p).getVert (List.idxOf w (cons h p).support))
          ((cons h p).drop (List.idxOf w (cons h p).support)) ⋯ ⋯).support
⊢ ((cons h_1 p).dropUntil w h).support =
    (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
        ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support

Tactic:
subst h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
v_1 w_1 : V
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h_1 : G.Adj w v_1
h : w ∈ (cons h_1 p).support
⊢ ((cons h_1 p).dropUntil w h).support =
    (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
        ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support

Tactic:
simp [dropUntil_first, drop_support_eq_support_drop_min]

Premises used: SimpleGraph.Walk.dropUntil_first, SimpleGraph.Walk.drop_support_eq_support_drop_min
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
a v_1 w_1 : V
h_1 : G.Adj a v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons h_1 p).support
h' : w ≠ a
⊢ List.idxOf w (cons h_1 p).support ≠ 0

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
a v_1 w_1 : V
h_1 : G.Adj a v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons h_1 p).support
h' : w ≠ a
neg :
  support (G := G) (u := w) (v := w_1)
      (if hx : a = w then
        Eq.ndrec (motive := fun (u : V) ↦ (h : u ∈ (cons h_1 p).support) → G.Walk u w_1)
          (fun (h : a ∈ (cons h_1 p).support) ↦ cons h_1 p) hx h
      else p.dropUntil w ⋯) =
    support (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
      (Walk.copy (p.drop (List.idxOf w (cons h_1 p).support - 1)) ⋯ ⋯)
⊢ ((cons h_1 p).dropUntil w h).support =
    (Walk.copy (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
        ((cons h_1 p).drop (List.idxOf w (cons h_1 p).support)) ⋯ ⋯).support

Tactic:
rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.drop_cons_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
v w u : V
inst : DecidableEq V
a v_1 w_1 : V
h_1 : G.Adj a v_1
p : G.Walk v_1 w_1
ih :
  ∀ (h : w ∈ p.support),
    (p.dropUntil w h).support =
      (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
h : w ∈ (cons h_1 p).support
h' : w ≠ a
⊢ support (G := G) (u := w) (v := w_1)
      (if hx : a = w then
        Eq.ndrec (motive := fun (u : V) ↦ (h : u ∈ (cons h_1 p).support) → G.Walk u w_1)
          (fun (h : a ∈ (cons h_1 p).support) ↦ cons h_1 p) hx h
      else p.dropUntil w ⋯) =
    support (u := (cons h_1 p).getVert (List.idxOf w (cons h_1 p).support))
      (Walk.copy (p.drop (List.idxOf w (cons h_1 p).support - 1)) ⋯ ⋯)

Tactic:
grind
-- 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
h₁ :
  ∀ {u : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u) nil) w),
    (dropUntil nil w h).support =
      (Walk.copy (u := getVert (G := G) (u := u) nil (List.idxOf w (support (G := G) (u := u) nil)))
          (drop nil (List.idxOf w (support (G := G) (u := u) nil))) ⋯ ⋯).support
h₂ :
  ∀ {a v w_1 : V} (h : G.Adj a v) (p : G.Walk v w_1)
    (ih :
      ∀ (h : w ∈ p.support),
        (p.dropUntil w h).support =
          (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support)
    (h_1 : w ∈ (cons h p).support),
    ((cons h p).dropUntil w h_1).support =
      (Walk.copy (u := (cons h p).getVert (List.idxOf w (cons h p).support))
          ((cons h p).drop (List.idxOf w (cons h p).support)) ⋯ ⋯).support
⊢ (p.dropUntil w h).support =
    (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support

Tactic:
induction p with
  | nil =>
    simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]
    grind [mem_support_nil_iff, support_nil]
  | @cons a _ _ _ p ih =>
    by_cases! h' : w = a
    · subst h'
      simp [dropUntil_first, drop_support_eq_support_drop_min]
    · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
      grind

Premises used: SimpleGraph.Walk.support_copy, SimpleGraph.Walk.support_nil, SimpleGraph.Walk.mem_support_nil_iff, SimpleGraph.Walk.cons, SimpleGraph.Walk.dropUntil, SimpleGraph.Walk.nil, SimpleGraph.Walk.getVert_nil, SimpleGraph.Walk.drop, eq_mpr_eq_cast, SimpleGraph.Walk.dropUntil_first, SimpleGraph.Walk.drop_cons_eq, SimpleGraph.Walk.drop_support_eq_support_drop_min
-- 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
⊢ (p.dropUntil w h).length = p.length - List.idxOf w p.support

Tactic:
simp [dropUntil_eq_drop]

Premises used: SimpleGraph.Walk.dropUntil_eq_drop
-- 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
⊢ p = (append nil (p.takeUntil w h)).append (p.dropUntil w h)

Tactic:
simp
-- 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
⊢ p = ((p.takeUntil w h).append (p.dropUntil w h)).append nil

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
mp : w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
mpr : (∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r) → w ∈ p.support
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

Tactic:
constructor