case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ degree G x = List.countp (fun e => decide (x ∈ e)) (edges p)
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (degree G x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
convert ht.isTrail.even_countp_edges_iff x
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Finset.card (incidenceFinset G x) = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ degree G x = List.countp (fun e => decide (x ∈ e)) (edges p)
rw [← Multiset.coe_countp, Multiset.countp_eq_card_filter, ← card_incidenceFinset_eq_degree]
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ↑Multiset.card (incidenceFinset G x).val = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Finset.card (incidenceFinset G x) = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
change Multiset.card _ = _
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = Multiset.filter (fun e => x ∈ e) ↑(edges p)
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ↑Multiset.card (incidenceFinset G x).val = ↑Multiset.card (Multiset.filter (fun e => x ∈ e) ↑(edges p))
congr 1
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = Multiset.filter (fun e => x ∈ e) ↑(edges p)
convert_to _ = (ht.isTrail.edgesFinset.filter (Membership.mem x)).val
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : Fintype ↑(edgeSet G)
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
have : Fintype G.edgeSet := fintypeEdgeSet ht
no goals
case h.e'_1.h.e'_3.h.e_6.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : Walk G u v
ht : IsEulerian p
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : Fintype ↑(edgeSet G)
⊢ (incidenceFinset G x).val = (Finset.filter (Membership.mem x) (IsTrail.edgesFinset (_ : IsTrail p))).val
rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]