-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem count_support_takeUntil_eq_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.takeUntil u h).support.count u = 1

Proof state:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h✝ : G.Adj u v✝
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Tactic:
simp!

Result:
no goals

Proof state:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).support = 1

Tactic:
split_ifs with h' <;> rw [eq_comm] at h' <;> subst_vars <;> simp! [*, List.count_cons]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ nil.support
⊢ List.count u✝ (nil.takeUntil u✝ h).support = 1

Tactic:
simp!

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Tactic:
cases h

Result:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h✝ : G.Adj u v✝
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1

Tactic:
rw [mem_support_nil_iff] at h

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count u (nil.takeUntil u h✝).support = 1

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ nil.support
h : u = u✝
⊢ List.count u (nil.takeUntil u h✝).support = 1

Tactic:
subst u

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ nil.support
⊢ List.count u✝ (nil.takeUntil u✝ h).support = 1

Proof state:
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

Tactic:
induction p

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ nil.support
⊢ List.count u (nil.takeUntil u h).support = 1

case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
h : u ∈ (cons h✝ p✝).support
⊢ List.count u ((cons h✝ p✝).takeUntil u h).support = 1

Proof state:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u ((cons h✝ p✝).takeUntil u ⋯).support = 1

Tactic:
simp! only

Result:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (h : u ∈ p✝.support), List.count u (p✝.takeUntil u h).support = 1
a✝ : List.Mem u p✝.support
⊢ List.count u (if hx : u✝ = u then hx ▸ nil else cons h✝ (p✝.takeUntil u ⋯)).support = 1