-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsTrail.even_countP_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) :
    Even (p.edges.countP fun e => x ∈ e) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Proof state:
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
rw [Nat.even_add_one, ih, ← not_iff_not]

Result:
case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
⊢ ¬¬(x ≠ w✝ → x ≠ x ∧ x ≠ w✝) ↔ ¬(¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝)

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : ¬x = u✝ ∧ ¬x = v✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
simp only [h.1, h.2, not_false_iff, true_and, add_zero, Ne] at ih ⊢

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬x = u✝ ∧ ¬x = v✝
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ ¬v✝ = w✝ → ¬x = w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ ¬u✝ = w✝ → ¬x = w✝

Proof state:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsTrail → (Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : (cons huv p).IsTrail
⊢ Even (List.countP (fun e => decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
rw [cons_isTrail_iff] at ht

Result:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsTrail → (Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e => decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬x = u✝ ∧ ¬x = v✝
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ ¬v✝ = w✝ → ¬x = w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ ¬u✝ = w✝ → ¬x = w✝

Tactic:
rw [ih]

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
h : ¬x = u✝ ∧ ¬x = v✝
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ ¬v✝ = w✝ → ¬x = w✝
⊢ ¬v✝ = w✝ → ¬x = w✝ ↔ ¬u✝ = w✝ → ¬x = w✝

Proof state:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + if decide (x = u✝ ∨ x = v✝) = true then 1 else 0) ↔
    ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
split_ifs with h

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : ¬decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
rw [decide_eq_true_eq, not_or] at h

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : ¬x = u✝ ∧ ¬x = v✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 0) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Proof state:
case nil
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ : V
ht : Walk.nil.IsTrail
⊢ Even (List.countP (fun e => decide (x ∈ e)) Walk.nil.edges) ↔ u✝ ≠ u✝ → x ≠ u✝ ∧ x ≠ u✝

Tactic:
simp

Result:
no goals

Proof state:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.IsTrail → (Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝)
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
⊢ Even (List.countP (fun e => decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
specialize ih ht.1

Result:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Proof state:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) (cons huv p).edges) ↔ u✝ ≠ w✝ → x ≠ u✝ ∧ x ≠ w✝

Tactic:
simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]

Result:
case cons
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + if decide (x = u✝ ∨ x = v✝) = true then 1 else 0) ↔
    ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ v✝ w✝ : V
huv : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ht : p.IsTrail ∧ s(u✝, v✝) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
h : x = u✝ ∨ x = v✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
obtain (rfl | rfl) := h

Result:
case pos.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x v✝ w✝ : V
p : G.Walk v✝ w✝
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝
huv : G.Adj x v✝
ht : p.IsTrail ∧ s(x, v✝) ∉ p.edges
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬x = w✝ → ¬x = x ∧ ¬x = w✝

case pos.inr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v x u✝ w✝ : V
huv : G.Adj u✝ x
p : G.Walk x w✝
ht : p.IsTrail ∧ s(u✝, x) ∉ p.edges
ih : Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ x ≠ w✝ → x ≠ x ∧ x ≠ w✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝