-- 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.inl
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
huv : G.Adj v✝ v✝
p : G.Walk v✝ v✝
ih : Even (List.countP (fun e => decide (v✝ ∈ e)) p.edges) ↔ v✝ ≠ v✝ → v✝ ≠ v✝ ∧ v✝ ≠ v✝
ht : p.IsTrail ∧ s(v✝, v✝) ∉ p.edges
⊢ False

Tactic:
exact G.loopless _ huv

Result:
no goals

Proof state:
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
⊢ x = w✝ → ¬v✝ = w✝

Tactic:
rintro rfl rfl

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

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

Tactic:
exact huv.ne

Result:
no goals

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✝
⊢ ¬¬(x ≠ w✝ → x ≠ x ∧ x ≠ w✝) ↔ ¬(¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝)

Tactic:
simp only [huv.ne.symm, Ne, eq_self_iff_true, not_true, false_and, not_forall,
  not_false_iff, exists_prop, and_true, Classical.not_not, true_and, iff_and_self]

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✝ → ¬u✝ = w✝

Proof state:
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
⊢ ¬(v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝) ↔ ¬x = w✝ → ¬x = x ∧ ¬x = w✝

Tactic:
simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall,
  Classical.not_not, exists_prop, eq_self_iff_true, not_true, false_and,
  and_iff_right_iff_imp]

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
⊢ x = w✝ → ¬v✝ = 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 : decide (x = u✝ ∨ x = v✝) = true
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Tactic:
rw [decide_eq_true_eq] at 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 : x = u✝ ∨ x = v✝
⊢ Even (List.countP (fun e => decide (x ∈ e)) p.edges + 1) ↔ ¬u✝ = w✝ → ¬x = u✝ ∧ ¬x = w✝

Proof state:
case neg.mpr
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✝
⊢ (¬u✝ = w✝ → ¬x = w✝) → ¬v✝ = w✝ → ¬x = w✝

Tactic:
rintro h' h'' rfl

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

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

Tactic:
cases h'

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

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✝
⊢ x = w✝ → ¬u✝ = w✝

Tactic:
rintro rfl

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

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

Tactic:
rw [Nat.even_add_one, ih]

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
⊢ ¬(v✝ ≠ w✝ → x ≠ v✝ ∧ x ≠ w✝) ↔ ¬x = w✝ → ¬x = x ∧ ¬x = w✝

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

Tactic:
simp only [imp_false, eq_self_iff_true, not_true, Classical.not_not] at h'

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

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

Tactic:
simp only [not_true, and_false, false_and] at h

Result:
no goals