split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), List.count u (support (takeUntil p✝ u h)) = 1
a✝ : List.Mem u (support p✝)
⊢ List.count u
      (support
        (if h : u✝ = u then
          Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
            (_ : List.Mem u (u✝ :: support p✝))
        else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))) =
    1
no goals