awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 = Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯
have h₁ : (p.takeUntil w h).support =
  (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) sorry sorry).support
Tactic: apply ext_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (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
have h₁ : (cast sorry nil).support = [u_1]
Tactic: simp only [takeUntil, eq_mpr_eq_cast, support_nil, getVert_nil, take, support_copy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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).support =
    (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support
have 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))) sorry sorry).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]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.takeUntil w h).support =
    (Walk.copy (v := p.getVert (List.idxOf w p.support)) (p.take (List.idxOf w p.support)) ⋯ ⋯).support
have 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)) sorry sorry).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)) sorry sorry).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]
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ G.Walk u v
have rw : G.Walk v v
Tactic: rw [mem_support_nil_iff.mp h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ G.Walk u w
have subst : (h : v ∈ (cons r p).support) → G.Walk v w
Tactic: subst u
Cleared hypotheses: u, h, hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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) = p
have nil : ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u),
  (takeUntil nil u h).append (dropUntil nil u h) = nil
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.takeUntil u h).append (p.dropUntil u h) = p
have 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 ∈ (cons h p).support), ((cons h p).takeUntil u h_1).append ((cons h p).dropUntil u h_1) = cons h p
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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
⊢ (takeUntil nil u h).append (dropUntil nil u h) = nil
have h₁ : u = u_1
Tactic: rw [mem_support_nil_iff] at h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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) nil) u
h : u = u_1
⊢ (takeUntil nil u h_1).append (dropUntil nil u h_1) = nil
have nil : ∀ (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u_1),
  (takeUntil nil u_1 h).append (dropUntil nil u_1 h) = nil
Tactic: subst u
Cleared hypotheses: u, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 ∈ (cons h_1 p).support
⊢ ((cons h_1 p).takeUntil u h).append ((cons h_1 p).dropUntil u h) = cons h_1 p
have cons : ∀ (h : G.Adj u v_1), ((cons h p).takeUntil u sorry).append ((cons h p).dropUntil u sorry) = cons h p
Tactic: cases h
Cleared hypotheses: u_1, h_1, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ ((Walk.cons h_1 p).takeUntil u h).append ((Walk.cons h_1 p).dropUntil u h) = Walk.cons h_1 p
have cons₁ : ∀ (a : List.Mem u p.support),
  ((Walk.cons h_1 p).takeUntil u sorry).append ((Walk.cons h_1 p).dropUntil u sorry) = Walk.cons h_1 p
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 h p).takeUntil u ⋯).append ((cons h p).dropUntil u ⋯) = cons h p
have 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 cons h (p.takeUntil u sorry))
    (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) sorry sorry
    else p.dropUntil u sorry) =
  cons h p
Tactic: simp! only
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have 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) sorry sorry) =
    cons h p
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have neg : ∀ (h' : ¬u_1 = u), (cons h (p.takeUntil u sorry)).append (p.dropUntil u sorry) = cons h p
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ 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
have 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 sorry)
        (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) sorry sorry) =
      cons h p
Tactic: subst_vars
Cleared hypotheses: u, p_ih, h_1, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
h : u ∈ p.support
⊢ p.dropUntil u h = p
have 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 => sorry.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 sorry) =
  p
Tactic: unfold dropUntil
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
v u : V
inst : DecidableEq V
p : G.Walk u v
h : u ∈ p.support
⊢ (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
have 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), sorry.mpr nil = nil
Tactic: split
Cleared hypotheses: v, p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (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
have 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 sorry) =
        cons r p
Tactic: split
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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 = Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯
have h₁ : (p.dropUntil w h).support =
  (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) sorry sorry).support
Tactic: apply ext_support
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (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
have h₁ : (cast sorry nil).support = [u_1]
Tactic: simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ ((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
have 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)) sorry sorry).support
Tactic: by_cases! h' : w = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ ((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
have 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)) sorry sorry).support
Tactic: by_cases! h' : w = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ ((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
have 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)) sorry sorry).support
Tactic: subst h'
Cleared hypotheses: a, h_1, h, h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ ((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
have 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 sorry) =
  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)) sorry sorry)
Tactic: rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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).support =
    (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
have 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))) sorry sorry).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
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ (p.dropUntil w h).support =
    (Walk.copy (u := p.getVert (List.idxOf w p.support)) (p.drop (List.idxOf w p.support)) ⋯ ⋯).support
have 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)) sorry sorry).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)) sorry sorry).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
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
have mp : w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
have mpr : (∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r) → w ∈ p.support
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
have mp : w ∈ p.support → ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
Tactic: classical
  constructor
  · exact fun h => ⟨_, _, (p.take_spec h).symm⟩
  · rintro ⟨q, r, rfl⟩
    simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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
⊢ w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
have mpr : (∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r) → w ∈ p.support
Tactic: classical
  constructor
  · exact fun h => ⟨_, _, (p.take_spec h).symm⟩
  · rintro ⟨q, r, rfl⟩
    simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
Goal:
V : Type u
G : SimpleGraph V
inst : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
⊢ List.count u (p.takeUntil u h).support = 1
have nil : ∀ {u_1 : V} (h : Membership.mem (γ := List V) (support (G := G) (u := u_1) nil) u),
  List.count u (takeUntil nil u h).support = 1
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (goal)
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),
    List.count u (takeUntil Walk.nil u h).support = 1
⊢ List.count u (p.takeUntil u h).support = 1
have cons : ∀ {u_1 v w : V} (h : G.Adj u_1 v) (p : G.Walk v w),
  (∀ (h : u ∈ p.support), List.count u (p.takeUntil u h).support = 1) →
    ∀ (h_1 : u ∈ (cons h p).support), List.count u ((cons h p).takeUntil u h_1).support = 1
Tactic: induction p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Walk.Decomp (hypothesis)
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
⊢ List.count u (takeUntil nil u h).support = 1
have h₁ : u = u_1
Tactic: rw [mem_support_nil_iff] at h