-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem count_edges_takeUntil_le_one {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) :
    (p.takeUntil u h).edges.count s(u, x) ≤ 1

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : u✝ = u
⊢ List.count s(u, x) (h' ▸ nil).edges ≤ 1

Tactic:
subst h'

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u✝ ∈ p'.support), List.count s(u✝, x) (p'.takeUntil u✝ h).edges ≤ 1
a✝ : List.Mem u✝ p'.support
⊢ List.count s(u✝, x) (⋯ ▸ nil).edges ≤ 1

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u✝ ∈ p'.support), List.count s(u✝, x) (p'.takeUntil u✝ h).edges ≤ 1
a✝ : List.Mem u✝ p'.support
⊢ List.count s(u✝, x) (⋯ ▸ nil).edges ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u✝, v✝) == s(u, x)) = true then 1 else 0) ≤ 1

Tactic:
split_ifs with h''

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : (s(u✝, v✝) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : ¬(s(u✝, v✝) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 0 ≤ 1

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
h : u ∈ (cons ha p').support
⊢ List.count s(u, x) ((cons ha p').takeUntil u h).edges ≤ 1

Tactic:
cases h

Result:
case cons.head
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x v✝ w✝ : V
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
ha : G.Adj u v✝
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : (u✝, v✝) = (u, x) ∨ (u✝, v✝) = (u, x).swap
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h''

Result:
case pos.inl.refl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬u = u
p' : G.Walk x w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj u x
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

case pos.inr.refl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Proof state:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : (s(u✝, v✝) == s(u, x)) = true
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
simp only [beq_iff_eq, Sym2.eq, Sym2.rel_iff'] at h''

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
h'' : (u✝, v✝) = (u, x) ∨ (u✝, v✝) = (u, x).swap
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

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

Tactic:
simp!

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1

Tactic:
rw [edges_cons, List.count_cons]

Result:
case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ (List.count s(u, x) (p'.takeUntil u ⋯).edges + if (s(u✝, v✝) == s(u, x)) = true then 1 else 0) ≤ 1

Proof state:
case pos.inr.refl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
cases p' <;> simp!

Result:
no goals

Proof state:
case cons.tail
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
⊢ List.count s(u, x) ((cons ha p').takeUntil u ⋯).edges ≤ 1

Tactic:
simp! only

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

Proof state:
case pos.inl.refl
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬u = u
p' : G.Walk x w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj u x
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
exact (h' rfl).elim

Result:
no goals

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

Tactic:
split_ifs with h'

Result:
case pos
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : u✝ = u
⊢ List.count s(u, x) (h' ▸ nil).edges ≤ 1

case neg
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
h' : ¬u✝ = u
⊢ List.count s(u, x) (cons ha (p'.takeUntil u ⋯)).edges ≤ 1