no goals
ι : Sort ?u.298269
𝕜 : Type ?u.298272
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(commonNeighbors G v w) ≤ degree G w
simp_rw [commonNeighbors_symm _ v w, card_commonNeighbors_le_degree_left]