ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ card (Set.toFinset Set.univ \ Set.toFinset {v, w}) = Fintype.card V - 2
ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ Fintype.card ↑(commonNeighbors ⊤ v w) = Fintype.card V - 2
simp only [commonNeighbors_top_eq, ← Set.toFinset_card, Set.toFinset_diff]
ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ card (Set.toFinset Set.univ) - card (Set.toFinset {v, w}) = Fintype.card V - 2

ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ Set.toFinset {v, w} ⊆ Set.toFinset Set.univ
ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ card (Set.toFinset Set.univ \ Set.toFinset {v, w}) = Fintype.card V - 2
rw [Finset.card_sdiff]
no goals
ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ card (Set.toFinset Set.univ) - card (Set.toFinset {v, w}) = Fintype.card V - 2
simp [Finset.card_univ, h]
no goals
ι : Sort ?u.303485
𝕜 : Type ?u.303488
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✝ : DecidableEq V
v w : V
h : v ≠ w
⊢ Set.toFinset {v, w} ⊆ Set.toFinset Set.univ
simp only [Set.toFinset_subset_toFinset, Set.subset_univ]